[SCL] DTD for XML/SCL

[John F. Sowa]

Bill and Chris,

I think we all agree on the fundamental issues regarding how SCL should
relate to XML.  To clarify, and in some respects broaden, the issues,
I would like to suggest the following approach:

  1. Write an XML DTD to relate the abstract syntax of SCL to XML along
     the lines that Chris has been doing.

  2. Include other concrete syntaxes in the SCL standards document,
     such as KIF and CGIF.

  3. Provide an escape tag, which would allow the embedding of various
     SCL concrete notations within an XML document.  For example,

        <logic language=kif>
            (exists ((?x Cat) (?y Mat)) (on ?x ?y))
        </logic>

        <logic language=cgif>
             (on [Cat] [Mat])
        </logic>

  4. Include Z as a first-class member of the SCL family, with the same
     status as KIF and CGIF.  The SCL standard document should relate
     the SCL abstract syntax to the concrete syntax of core Z (which is
     Z without the mathematic toolkit) in the same way that it relates
     the abstract SCL syntax to the concrete syntaxes of KIF and CGIF.

Points #1 and #2 seem to be well accepted by everybody who is working
on the SCL project.  Point #3 is one that I raised in my earlier note,
to which Bill and Chris replied.  I would have no objections to the
verbosity of the XML DTD along the lines of #1 provided that we also
have an escape along the lines of #3, which would allow KIF, CGIF, and
other compatible SCL languages in an XML document without the overhead
of the encoding proposed for point #1.

The major new point I believe we should add is the adoption of Z as
a member of the SCL family of concrete notations.  There are several
reasons, which I discussed in my earlier note and which I would like
to summarize here:

  1. The model-theoretic foundations for Z, as presented in the ISO Z
     standard, are logically equivalent to the simplified SCL semantics
     that Pat Hayes proposed.

  2. Z has been developed and used by well-qualified computer scientists
     who have a long history of applying logic to formal specifications
     of programming languages and other kinds of software.  It was first
     published as a PhD dissertation by Mike Spivey at Oxford, but it
     incorporates the approach developed by Hoare, Abrial, and others,
     including distinguished visitors to Oxford, such as Dana Scott.

  3. Z has been officially adopted as an ISO standard.  An SCL standard
     that builds on the Z standard would be very easy to sell to the
     ANSI and ISO standards bodies as well as to any country, company,
     or computer scientist who respects ANSI and ISO (which includes
     nearly everybody in the world except Bill Gates).

  4. Finally, we have been proposing CL and SCL as a way of unifying
     the diverse logic-based notations that have been developed.
     If we adopt the Z standard as a foundation for SCL, we will set
     a good example for other people to follow.  But if we ignore Z and
     go our own way independently of Z, we will lose any credibility
     we may have had.  The first question anybody would ask is why
     they should accept our proposal instead of adopting an official
     ISO standard that has the same semantics.

As I said in my earlier note, the adoption of Z semantics as a
foundation for SCL would allow us to develop an upward compatible
semantics that would satisfy the more ambitious goals of our
earlier CL efforts.  We could write a solid SCL standard document
with an outline similar to the Z document by June 2003.  After that,
we could turn to the more ambitious metalanguage project for CL,
which would go beyond what has been done in the Z standard.

Bottom line:  Adopting the Z standard for the SCL foundations would
enable us to finish an SCL standard document quickly, and let us begin
work on the much more interesting metalanguage project.

John