[SCL] Headers and bodies

[John F. Sowa]

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.

 > 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, 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?"

 > 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.  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?  One (either Nand or Nor)
is sufficient, but since those are uncommon operators, I would prefer
to have 2: And and Not.

 > 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?  Or is it syntactically incorrect?  Is there
a distinction between simple falsity and syntax errors?  If there is no
such distinction, what happens if I write (not (x y z w))?  Is it true?

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?  That should only be necessary if we required
a single parser that would parse all SCL-conformant languages.
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.  I don't
believe that we should require or even bother to specify a single
document format for every SCL-conformant language.

John