[SCL] Issues and proposals

[John F. Sowa]

Pat, Chris, Jim, et al.,

I have been going through the documentation for the ISO Z standard,
which was formally approved in May 2002.  I believe that the ISO Z
standard would make an excellent starting point for defining the
Simplified Common Logic (SCL) standard.  (For more info about Z
and the ISO standard, see the references at the end of this note.
I recommend the first chapter of the Z reference manual, zrm.pdf,
as an excellent tutorial on Z.)

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.  Although that metalanguage
is not presented as a standardized language in the Z document, a
similar approach could be formalized as part of the more ambitious
goals we have envisioned for the full Common Logic standard.

Therefore, as one, admittedly rather large issue, I would like to make
the following proposal:

  1. We start with the final draft of the ISO Z standard (which Frank F.
     had suggested that we review) as an outline for the June 2003 draft
     of the SCL standard.  That draft would adopt the same model theory
     that is developed for Z:  first-order logic plus equality with ZF
     set theory used to define the denotation of every SCL expression.

  2. Instead of using Z notation as the metalanguage for defining SCL,
     we could use a version of KIF syntax with each of the Z symbols
     replaced by a plain ASCII string; e.g., the fancy letter P used
     in the Z standard would be written as "powerset".

  3. 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.

  4. Given a formal definition of sequences, it should be a relatively
     straightforward exercise to define a syntax that would use sequences
     as a replacement for the row variables that people have been using
     in KIF.  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.  For the
     KIF users, there should be no noticeable difference.

  5. As concrete syntaxes for the object languages, the SCL standard
     would include the grammars for a KIF-like language that is
     upward compatible with current KIF and for a CG-like language
     that is upward compatible with CGIF (Conceptual Graph Interchange
     Format).  Since the model theory would be indentical to the Z
     standard, that would make all three concrete notations semantically
     equivalent and computationally interoperable:  KIF, CGs, and Z.

Since most of the above work can be accomplished merely by copying the
relevant parts of the Z standard and replacing the Z syntax and symbols
with KIF syntax and symbols, I believe that we can finish the complete
committe draft by June 2003.  At that point, we can submit it to both
ISO and W3C.  If everybody likes it, then it would become an ANSI, ISO,
and W3C standard.

The next step after June 2003 would be to work on the more ambitious
CL standard, which would formalize the metalanguage as well as the
object language and which would replace the Z semantics with a more
general, but upward compatible typeless model theory along the lines
that Pat and Chris have been developing.  I would hope that the full
CL effort could be completed by summer 2004, but that is another issue
to be discussed.

Following are some comments on earlier notes.  First a comment on
Jim Hendler's recent note:

JH> In particular, I am very interested both in the expression of rules
 > on the web (connected to the sorts of ontologies provided by OWL) and
 > even more so in the exchange of proofs on the web - which, if done
 > right, could really prove an amazingly strong case for the deployment
 > of logics on web resources.

That shouldn't be difficult.  There are quite a few theorem provers
that use KIF, CG, and Z notations.  Defining a common semantics for
all three notations together with formal mappings from any of the
notations to any of the others should make it even easier to exchange
rules, proofs, ontologies, etc.

JH> For example, my favorite is an e-business contract in which your
 > system could send to my bank a proof that I had made a purchase at an
 > agreed upon price, and my bank would transfer the money assuming all
 > was appropriately signed and assured.  Tim BL's favorite is web site
 > access - his example is that you can access the W3C member site if you
 > can prove you work for one of the members - and that proof probably
 > includes some sort of signed statement from some database that you
 > work for X, coupled with the W3C's assertion that X is a member.

Again, a lot of work on such topics has been done with all three
notations.  You might take a look at the examples in Spivey's
reference manual for Z (see the reference below for zrm.pdf).

I would also like to mention the RoZ project (see reference below),
which translates an annotated version of UML diagrams to Z.  The
RoZ tools can be used in conjunction with Rational Rose for generating
formal specifications as part of the UML design process.  The RoZ
tools also generate the UML Object Constraint Language (OCL) from Z.

And Gerard Ellis (email above) had been teaching a course in
software engineering, in which he used both Z notation and CG
notation for software specification.  He gave the students their
choice of using either notation for their course projects, and
most of them preferred to use the CG notation.  But both notations
were used in semanticaly equivalent ways.

Another language I would recommend for the SCL family of notations
is a version of controlled English.   See my note on how similar
rules can be stated in an English-like notation that could be
translated to or from any of the three proposed notations for SCL:

    http://www.jfsowa.com/logic/ace.htm

In a previous note, Pat Hayes mentioned a couple of issues that were
raised by Tanel Tammet:

PH> 1. SCL needs a way to attach comments to expressions which are
 > logically transparent but can be used to attach extra-logical
 > information.

All three notations -- KIF, CGs, and Z -- already have a syntax for
representing comments, and the translations from one notation to
another could simply carry the comments along while changing the
delimiters to suit the particular concrete syntax.

PH> 2. SCL needs an explicit XML syntax. Choosing an XML syntax style
 > may have consequences for the rest of the language.

Everyone recognizes that it is necessary to demonstrate that any of
the concrete notations should be translatable to an XML form.  But that
would impose no constraints on the languages themselves.  As a matter
of fact, back in the 1980s, two of the CG implementers, Alex Hurwitz and
Bill Rich, had designed a represenation for CGs in GML -- the parent
of SGML, which is the parent of XML.  That representation didn't require
any changes to either the syntax or the semantics of conceptual graphs.

Furthermore, Appendix A of the ISO Z standard is devoted to the LaTeX
mark-up for formatting and printing Z notation.  The reason why they
used LaTeX instead of XML is that XML was not available when they began
working on their project and all the Z formatting tools used LaTeX.
In any case, it would be an easy exercise to modify or extend MathML
to format Z.

John Sowa

------------------ References ------------------

The Z Reference Manual, which is a more readable
introduction to Z than the official ISO standard:

    http://spivey.oriel.ox.ac.uk/~mike/zrm/

If that link is unavailable, the book can also be found
at the following URL:

    http://www.cs.clemson.edu/~fmgroup/Materials/Zed/zrm.pdf

The Z user's web site with the FAQ list and pointers to
various resources:

     http://www.zuser.org/z/

Copies of the draft standards and other proceedings
leading up to the official ISO standard:

     http://www.zuser.org/z/#standards

The draft of August 1999 is almost identical to the
official ISO standard.

Web site for tools that map annotated UML diagrams
to Z specifications:

     http://www-lsr.imag.fr/Les.Groupes/pfl/RoZ/

The name RoZ is pronounced "Rosette" to suggest
that it is a Rosetta stone for relating UML to logic.