[SCL] REQUEST FOR FEDBACK: core syntax

[John F. Sowa]

Pat, Jay, Tanel, and Murray,

We should give a clear statement of who or what
is expected to read or write the SCL core syntax.

  1. If it's intended for people to read and write,
     then human readability is essential.

  2. If it is intended as an intermediate language
     for programs to read and write then simplicity
     in the grammar is more important than human
     readability.

I have been assuming that SCL core syntax is primarily
intended for computational purposes, and people would
prefer to use many other notations, such as controlled
English (or French, or Estonian, or whatever) or some
other previously designed language, such as infix
predicate calculus, CGs, TMs, UML, or whatever.

Assuming that human readability is not a primary design
requirement for SCL core syntax, then I would recommend
the following design decisions:

  1. A preference for a LISP-like (or KIF-like) syntax
     for expressions.  But this is only a mild preference,
     since it is not too difficult to interchange the name
     of the relation with the opening parenthesis.

  2. Programs are easier to write when there are no
     exceptions.  Therefore, if we have an explicit
     symbol for "or" and "exists", it would be easier
     to handle "and" and "forall" in the same way
     than to treat them as exceptions.

  3. Logically, a constant is simply a name that is
     existentially quantified with a global scope
     rather than sentence or parenthetical block scope.
     Therefore, the presence or absence of a distinction
     in the spelling of constants and variables is
     irrelevant, because a parser would need to maintain
     a symbol table to keep track of the scope of names
     (and types with a sorted or restricted notation).

  4. Much more important is the question of whether we
     want to adopt a unique-name convention:  if "abc" and
     "def" are two constants with different names, can we
     assume that they are distinct, or must we assume
     that they could be equal?  For theorem provers,
     that is a far more significant issue than whether
     they are local or global.  If we do want to have
     a unique-name convention, then we would need some
     marker to indicate such names.

John