[SCL] Issues and proposals

[John F. Sowa]

Pat,

I agree with your concerns about the vast differences between Z
and CL/SCL in motivation, application, notation, and type theory.

However, their model theoretic semantics, which is presented in
Section 15, called "Semantic Relations", takes just 7 pages in their
admittedly "rebarbative" notation.   My suggestion is to define the
semantics of SCL in a similar fashion, but with KIF-like notation
and without the rather heavy-handed type system of Z.

That would give us a version of FOL that would be, in effect,
an untyped subset of Z.  There would be no need for us to go
through all the definition of Z syntax, types, schemas, etc.,
since the Z standard already does that.  As a replacement for
the Z types, we could just adopt the old KIF strategy of
calling them "types", but defining them by restricted
quantification.   Every KIF or CGIF statement that used
restricted quantification would then be logically equivalent
to some untyped Z statement, but there might not exist a
strongly typed Z equivalent.

I haven't gone through the details of Z type theory, but I
suspect that any correctly typed Z statement could be translated
to an untyped Z statement, which could be then translated to KIF/CG
notation.  I'm sure that people in the Z community would be happy
to confirm or correct that conjecture and to provide approved Z
terminology on that point, which we could insert into the SCL
standard document.

I would like to say a bit more about some of the other points you
mentioned in your note, but I'll do that in a separate note.
For now, I would like to bring up an important procedural issue:

I plan to fly to Santa Fe, NM, on Jan 22 for the metadata forum
and stay until Tuesday, Jan 28, for the ISO committee meeting.
Is there anyone else in the SCL group who would also be able
to go there for some or all of that time?  If so, we could have
a one or two-day meeting on SCL during the weekend of Jan 25 & 26
and possibly some informal meetings before or after those dates.

John