[SCL] Headers and bodies

[pat hayes]

>Pat,
>
>I am very much in sympathy with your basic goal of producing
>a single document with a single model theory for a single
>language, and I am still hopeful that it can be achieved
>by Dec. 12th.  Following are some comments:
>
>>  First, our primary goal should be to define a single language.
>>  We can *present* it in a 'core+modules' way purely for exposition,
>>  but it should *be*  a single coherent system with a single model
>>  theory. Somewhere in the spec, there should be a single, ideally
>>  quite compact, statement of what SCL as a whole) *is*, one that
>>  a developer can take and run with.
>
>I agree.
>
>>  Second, it should be possible (and we should explain how) to
>>  implement a conforming SCL reasoner largely by translating SCL
>>  into a FOL theory in a certain way, and then applying traditional
>>  FOL reasoners to it. But this translation need not be central or
>>  particularly simple (though it would be nice if it were not
>>  hopelessly inefficient).
>
>I believe that is possible, but probably not by Dec 12.

Well then it will be done later than Dec 12. :-)

>
>>  Third, we can identify subcases of SCL that have useful properties,
>>  including 'traditional FOL'; so that traditional FOL is indeed a
>>  sublanguage of SCL.
>
>I agree.  I also believe that we can define Z as a sublanguage of SCL,
>since Z is basically a typed version of infix FOL with a lot of special
>symbols.  I don't believe it's a firm requirement to specify Z

It is not even on the agenda. I propose to completely ignore Z.

>, but
>I think it is possible to do so without too much trouble, and it
>would answer a lot of questions, such as "Why aren't you using Z?"

That is not a question that deserves a rational answer, IMO.

>
>>  Fourth, all of the above exposition - of SCL syntax, model theory
>>  and translation into FOL - can be stated in terms of an abstract
>>  syntax, and hence projected into any conforming concrete syntax.
>
>I agree.
>
>>  ...  Chris' style of language description treats these as completely
>>  distinct: a language is defined by its syntax, and a model theory is
>>  attached to the syntax: and 'syntax' here includes a lexical
>>  classification of the primitive lexical terms. This distinction is
>>  wired into Chris' way of describing abstract syntax by starting with
>>  a lexicon and building up from there.  This means that matters like
>>  the arity of a relation are part of the basic syntactic structure
>>  of the particular SCL language, and hence must be taken account of
>>  throughout the subsequent metatheoretic development; hence much of
>>  the complexity, I suggest. And hence also the fact that 'an SCL
>>  language' must as it were come clean on what its syntactic/lexical
>>  assumptions are; whereas, in contrast, Tanel and I both think of SCL
>>  (and FOL) as a *single* language, rather than a family of languages.
>
>That is a very good way of summarizing the differences.  I would vote
>for an approach along the lines that you and Tanel are recommending:
>
>  1. Define the abstract syntax of one very simple SCL language.
>
>  2. Define the MT for that language.
>
>  3. Defer most syntactic issues to the specification of each concrete
>     syntax for each SCL-conformant language.

Not sure what you mean here by 'language'. Eg consider SCL-KIF as one 
concrete syntax. Is that *one* language, in your view? Because for 
Chris its *infinitely many* languages, each one of them defined by a 
particular set of constant names. If you mean the latter sense of 
"language", specifying a concrete syntax doesn't define a single 
language. So how do we specify the lexical rules for a *single 
language* in this sense? .

>  The concrete syntax of
>     a KIF-like SCL language might be much simpler, for example, than
>     the syntax of Z.  That would make the spec for Z longer than
>     the spec for KIF, but the SCL core would be the same for both.
>
>>  I think that the basic MT that we have worked out is right. It works,
>>  it has been stable now for quite a while, and we understand it fully.
>  > When we started, SCL was pretty damn simple: all names (except
>>  functions) were the same syntactic category and we didnt need anything
>>  like the complexity that we are now saddled with. Looking back, it
>>  seems to be that all of our problems have been to do, one way or
>>  another, with syntax.
>
>I agree.  I would prefer to have a very simple SCL core, which I could
>use as a base for defining CGIF (or Z, if I have the time).
>
>In fact, I would prefer to have only three operators in the core
>language:  the existential quantifier, conjunction, and negation.
>All other operators could be defined as syntactic combinations of
>those three.
>
>The current SCL 1.1 contains 2 quantifiers and 5 Boolean operators.
>But why include 5?  Why not 1? or 2? or 16?

That was a design decision, and we could debate its merits one way or 
another. The syntax we have right now seems to be a reasonable 
compromise between useability and complexity.

>One (either Nand or Nor)
>is sufficient, but since those are uncommon operators, I would prefer
>to have 2: And and Not.

So, would users be obliged then to write (P or Q) in the form (not 
((not P) and (not Q))) ? That seems unfriendly, to say the least. Or 
do you want us to specify an abbreviation convention which allows 
users to say that Or is an abbreviation for the deMorgan form? We 
would need a notation to use to specify the abbreviations that were 
allowed, which would allow for example schematic variables for 
arbitrary sentences, which we don't have right now in the language, 
so we would need to do some completely new material. (I know its all 
familiar stuff, but it takes the SCL project in a completely 
different direction.) . I don't think it is part of the SCL goal to 
be a *minimal* language; and in any case, a minimal language plus a 
set of abbreviation conventions is actually more complicated than the 
language we have at present.

>  > First, define basic SCL as the language which has a single category
>>  of names, and the MT is defined so that terms which occur in a
>>  relation position must denote relations, and in object position must
>>  denote something in the universe of discourse (and function symbols
>>  denote functions, of course), and no other constraints.
>
>Question:  What if I write (x y z w) in a KIF-like syntax, and x is not
>a relation?  Is that false?

In my proposal, assuming that is that the header declares x to be a 
non-relation, this will in fact be false, but its truthvalue in such 
interpretations is kind of irrelevant since they will be 
inappropriate for the header.

>  Or is it syntactically incorrect?

In the current version, it is syntactically ill-formed: but that begs 
the question of how exactly x is declared to be a relation symbol.

>Is there
>a distinction between simple falsity and syntax errors?

Whether to regard this a a syntactic or a semantic matter is where 
Chris and I have been taking different roads. The 'header' idea was 
an attempt to find a mutually acceptable compromise, or perhaps 
better a way of doing it both ways at once, by subsuming syntactic 
issues (in the body ) to semantic ones (in the header).

>  If there is no
>such distinction, what happens if I write (not (x y z w))?  Is it true?

In the header proposal, if x is stated to be a non-relation in the 
header, then this sentence in the body is considered to be 
semantically ill-formed: it can be satisfied only by interpretations 
which are inappropriate for the header,a nd they are not allowed to 
be satisfying interpretations of the body even if they would satisfy 
it in isolation (as here.)

>Rather than comment in detail about the header issue, let me ask
>a more basic question:  Why should we define the document format
>in the SCL standard?

We have to define it some way, and there are many pragmatic 
advantages to using SCL to define itself as far as possible. Chiefly, 
it greatly increases the chances of having SCL be a basis for 
interoperability using different notations.

>That should only be necessary if we required
>a single parser that would parse all SCL-conformant languages.

That would obviously be highly desireable, but I agree is not 
absolutely required. However I think it is not unreasonable to 
suggest that for each concrete syntax, there could be a universal SCL 
parser for all SCL documents  written *in that concrete syntax*. In 
fact I think this is close to being a requirement: if we can't do 
this there is little point in defining SCL at all.

>I don't think that's a requirement.
>
>Those people who prefer XML formats can use their existing XML tools.
>People who have been developing CGs can use CG tools -- and the
>same goes for Z, UML, etc.  They all have their own tools.

Sure, that is the choice of concrete syntax. But that is an 
orthogonal issue, and  the header idea wasn't meant to handle that: 
more, questions like, is 'Frooble' a relation or an individual name? 
Does it have a fixed arity or not? Call this 'micro-syntax' or 
'lexical' questions: that is what the header is supposed to be able 
to specify.

Pat

>   I don't
>believe that we should require or even bother to specify a single
>document format for every SCL-conformant language.
>
>John


-- 
---------------------------------------------------------------------
IHMC	(850)434 8903 or (650)494 3973   home
40 South Alcaniz St.	(850)202 4416   office
Pensacola			(850)202 4440   fax
FL 32501			(850)291 0667    cell
phayes at ihmc.us       http://www.ihmc.us/users/phayes