[SCL] Re: The second draft for XML syntax for CL

[geoff at cs.miami.edu]

Hi Murray,

> > It's not black and white. The more verbose your syntax gets, the more
> > people who may be alienated. So it's not just "use XML or don't", it
> > can affect decisions in designing the XML syntax (i.e., avoid verbose
> > XML).
> 
> First, we were discussing XML in general as a verbose notation, not
> specifically the design of a specific syntax. But as regards markup
> design, I'm not sure on what your opinion is based. There are a great
> number of factors involved in designing a suitable syntax, and these
> must be taken into account more than any measure of verbosity, which
> is really irrelevant after the other, more important, factors are
> taken into account.
> 
> For example, it seems "simple" to put content in attribute values.
> Well, if one wants to add attributes to that content, it's apparent
> that the content should be element content. This is a recursive
> issue. Also, there are matters of simplicity that are in direct
> conflict with verbosity -- sometimes a more verbose syntax is in
> actuality a lot simpler, such as having one element that is typed
> by another rather than a myriad of "simple" elements, if you need
> extensible typing.
> 
> Put it this way: XML was designed by some of the industry's experts,
> people with decades of experience in SGML. What does one of the
> requirements on XML say? "Terseness in XML markup is of minimal
> importance." I've now been doing markup work for over a decade,
> and honestly, the last thing to consider is verbosity. If people believe
> an XML concrete syntax for SCL is going to be commonly hand-authored
> rather than the product of a transformation, I think they need to
> have their heads examined. HTML is one thing, but logic? Think of
> the potential for syntax or human interpretation errors. ugh.

OK. If we agree that this stuff is never going to be seen by people, then
verbosity is no issue. Then, going back to a previous item in one of the
emails, I suggest that using long words for tags (<quantifier> rather
than <quant> or <q>). It'll make parser code easier to write and understand,
and there's no loss to the user (who'll never see it).

> >>>   TPTP will support is 
> >>>         ? [1:X,2:Y] : p(X,Y)
> >>>   meaning there are exactly one X and two Ys such that p(X,Y).
> >>>   
> >>>   Comment by Tanel: no clear need to introduce this into minimal core
> >>>   (we want to keep the core minimal!). Could be introduced in extensions.
> >>>   Easy to give an extra parameter to quantifier tag, like this:
> >>>   <quantifier name="exists" variable="x" count="2">
> >>>   indicating that we say that there are exactly TWO instances.
> >>>   However, bringing this into core creates unnecessary complications.
> >>>   Let us see whether it will be in the SCL core - if yes, we can put
> >>>   it into the XML concrete syntax.
> >>
> >>This could be introduced as a PSI rather than as new syntax. As in my
> >>last comment.
> > 
> > Help, what's PSI? Anyway, I support Tanel with a minimalist approach in
> > the core. So, as I suggested in my response to the first draft, I would
> > say the typing is not core - you open any text on mathematical logic and
> > read the definition of FOL ... not a word about types. I suggest you can
> > take types out of the core.
> 
> What I'm referring to as "types" are inherently in the core, just a
> very specific set, essentially anything that can be typed. If you
> look at the current SCL draft, in the content of <formula> you see
> types. There are two quantifier types, <forall> and <exists>; there
> are five connective types, <and>, <or>, <implies>, <iff>, and <not>.

I think we are talking about different things. I am referring to types
for the logic variables, as in Tanel's example:
    exists x:r forall y . p(x,f(1,a)) & ...
Here the logic variable x is constrained to be of type "r" (real?). Maybe
I'm really missing something, but aren't those different from the types you
(Murray) are referring to? If they are different, it's those logic variable
types I suggest are non-core. Please put me right if I'm all wrong.

Cheers,

Geoff

Geoff Sutcliffe                           http://www.cs.miami.edu/~geoff
Department of Computer Science            Email : geoff at cs.miami.edu
University of Miami                       Phone : +1 305 2842158/2842268
(Director of Undergraduate Studies)       FAX   : +1 305 2842264