[SCL] Issues and proposals

[pat hayes]

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

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

>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:

This is too much to swallow as a single proposal, particularly as the 
declared aims of Z are somewhat different from ours.

Let me modify this to a slightly weaker initial proposal, which is 
that we examine the Z standard carefully, all agree to at least read 
it, and discuss it carefully.

------

Having (re)read it, I would vote against basing SCL on Z.  The 
languages seem quite different both in aims and in overall structure, 
and Z has many aspects, most notably a very strong type system, which 
make it unsuitable as a first-order description language. Other 
aspects which are contraindicative include its strictly extensional 
semantics, and its emphasis on matters to do with computation, such 
as whether or not some operations preserve 'state', and the rather 
complex and fussy business of having named 'schemas'.

What does make sense is to think about providing as clear a statement 
as we can manage of any useful mappings between Z and SCL. Z for 
example seems to have a very idiosyncratic syntax for specifying 
quantifiers, but I think it can all be mapped into SCL without any 
real harm being done to the meanings.


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

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.

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.

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

I agree it can be done but not that it is exactly straightforward. In 
particular it is not enough to simply have an SCL ontology for 
sequence. We know there are tarpits in this area, eg ANSI-KIF was 
thought (wrongly) to be first-order for many years. I  will send more 
on this topic soon.

>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

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.

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

I think this (apart from the new introduction of Z) already part of 
our overall plan. If Z can be smoothly incorporated, then by all 
means let us do so, but I am not sanguine about that.

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

Getting it through the W3C would take a considerable effort and the 
initiative would have to come from them. One step at a time.

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

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.

>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 caution all logicians that the notion of 'proof' being used 
here is rather different from the standard logical notion, eg 
consider carefully that idea of a 'signature' that Jim refers to 
above. This needs genuine research, which I don't think we have time 
for.

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

I know it is trivial to do, but getting such trivialities actually 
done,a nd locked down and documented is what is going to take up all 
our time. We need to get these all documented in a list so that we 
don;t just forget about them.

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

No, we need to actually *define* an XML syntax as part of the spec., 
in detail. It is not enough to just make observations about a proof 
of concept.  There are many ways to translate a syntax into XML: for 
our sins, we are obliged to actually choose one.  For many users, 
"XML DTD" and "language" are almost synonymous.

>  But that
>would impose no constraints on the languages themselves.

I agree it shouldnt be a constraint on the sematnics and probably not 
on the syntax. But there are issues to be considered. for example, 
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.

Pat

-- 
---------------------------------------------------------------------
IHMC					(850)434 8903 or (650)494 3973   home
40 South Alcaniz St.			(850)202 4416   office
Pensacola              			(850)202 4440   fax
FL 32501           				(850)291 0667    cell
phayes at ai.uwf.edu	          http://www.coginst.uwf.edu/~phayes
s.pam at ai.uwf.edu   for spam