[SCL] Issues and proposals (details)

[John F. Sowa]

Pat,

Following are some further comments on the details of your comments,
which I did not address in my earlier note:

JS> Interestingly, the Z standard uses a version of the same Z notation
 > (supplemented with the syntactic categories of Z as types) as the
 > metalanguage for defining Z itself.

PH> Well, to be fair, that makes sense for Z since it was intended from
 > the start as a software specification language.

Actually, the Z metalanguage is not an official part of standard Z.
It is not intended to be used outside the scope of the Z document
itself.  In some of our earlier discussions of metalanguage issues,
I recommended the Goedel language, which is an elegant logic
programming language with a cleaner semantics than Prolog and with
a great deal of attention to metalanguage issues.  The Goedel approach
is similar to the way Z is used as a metalanguage, and I recommend it
as a basis for the CL metalanguage.  The similarity of Goedel to the Z
metalanguage is "interesting" as an example of how different groups
naturally converge on similar solutions.  But for the June-July SCL
document, I believe that we can skip the metalanguage issues,
if that will speed up agreement on the SCL core language.

PH> Having (re)read it, I would vote against basing SCL on Z...

I agree, in the sense that we shouldn't adopt all of Z.  What I think
we can do is to adopt a logically equivalent model theory (translated
into KIF notation instead of Z notation).  Then we can say that both
standards are "based on" the same semantics, but differ in the choice
of features and notations are included in the standard.  With this
approach, any well-formed statement in either Z or SCL could be
translated to a logically statement in the other.  However, it would
not be necessary for us to define the translation in the SCL document,
since the Z developers have done all that work in their document.

JS> Annex B of the Z standard defines a "mathemtical toolkit" in Z,
 > which includes sets, relations, functions, integers, sequences,
 > and bags.  All of those entities, which we have been calling a
 > mathematical ontology, would be useful for most applications of KIF
 > and conceptual graphs.  Therefore, I suggest that we include the same
 > definitions (but in the KIF-like notation) as an annex to the SCL
 > standard.

PH> I am happy to have such an annex, although I think that for the
 > purposes and applications I myself am interested in supporting that it
 > will be of little practical use.

Fair enough.  Those features are available in so many systems, including
SQL, that if we didn't have them people would ask for them.  Since it
wouldn't take much effort to include them, we might as well put them in.

PH> A far more useful toolkit would include means of referring to times
 > and dates, a name-context mechanism and a general-purpose theory of
 > alternative syntaxes. I do not expect to get this done by July. But I
 > think what we DO need to get done is to specify a connection between
 > SCL and XML schema datatypes; and moreover, that this will need to be
 > done in the SCL syntax rather than simply be an SCL ontology. The
 > reason for the last point is that many of the XSD domains cannot be
 > axiomatized in FOL, but instead require recursion.

Fine.  I'm happy with that.

JS> In fact, I believe that it would be possible to define a syntax
 > that is identical to what the KIF users are familiar with.  The only
 > difference is that the sequences in the SCL version of KIF would be
 > defined in an annex rather than the core logic.

PH> I do not think that this can be done coherently, but would welcome
 > any exact proposal. The main problems are (1) the set of *finite*
 > sequences cannot be defined using FOL but requires recursion, and (2)
 > defining sequences does not of itself give one the power to quantify
 > over the members of sequences. There is a big difference between
 > quantifying over sequences and quantifying *with* sequences, ie using
 > sequences in the syntax to quantify over an arbitrary sequence of
 > things. That first step requires us to go a squeak beyond FOL, but the
 > second step takes us right into infinitary logic, which I think is
 > where we definitely do not want to go.

I agree that there is a need to go beyond FOL, and the Z developers have
done that with the English phrase "the smallest set such that", which
occurs repeatedly throughout their standard.    That escape clause is
the minimum necessary for most mathematics, and I believe that we can do
the same thing that the Z people have done.  After using that clause to
define sequences, they quite happily allow quantification over them.

PH> The issue here is that 'rules' is often taken to mean something
 > *less* expressive than FO implications, or even Horn clauses, and also
 > often assumed to include nonmonotonic constructions such as
 > negation-by-failure which violate most standard model theories.

I agree that the nonmonotonic constructions create problems.  They can't
be represented by in pure FOL or even the extensions used for Z.  I
suggest that we leave them for CL, not for the June-July version of SCL.

PH> RDF has an XML syntax already defined. It is hideous and irrational,
 > but it is now a standard. There is also an obvious translation of RDF
 > into SCL (positive binary existential conjunctions) . Should we try to
 > produce an XML syntax for SCL which preservers the XML syntax of the
 > RDF-definable fragment? It would not look at all like the DTD that
 > Chris suggested.

I agree that we need an XML representation at the level that Chris
suggested, but there is no reason why it has to have any syntactic
resemblance to RDF.   As long as we provide a definition of how the RDF
subset version can be translated to and from the more rational syntax
that we propose, that should be sufficient.

Our claim is that we can provide a common semantics that can support
interoperability with any notation for any subset of classical FOL that
conforms to the semantics.  If someone wants to invent a truly ugly
syntax, as the RDFers have done, they have to live with it.  We can
support it semantically and show how to translate to and from it,
but we don't have to adopt it.

John