[SCL] Representing constraints that go beyond EBNF

[John F. Sowa]

Pat,

EBNF can be defined as a subset of Horn-clause logic, which is
a subset of FOL.  The constraints that go beyond EBNF can be
defined in any version of FOL, including SCL.  That would give
a complete specification of SCL in SCL.

JS> In mathematics, a common representation for a graph consists
 > of a set of nodes and a set of arcs.  Since sets are by definition
 > unordered, no further comment is needed.

PH> That kind of an answer isn't going to be acceptable to the Perl
 > hackers, though. They want a machine-readable syntax for specifying
 > it, which is what I was also looking for.

There are machine executable implementations of Z.  So it would be
possible to specify everything in Z (assuming that EBNF was first
translated to Z).  But I doubt that Z is what the average Perl hacker
would like to see.

PH> A grammar written in ISO EBNF *with some additions* is not written
 > in ISO EBNF.

People who use ISO EBNF typically go beyond EBNF in order to specify
the context-sensitive constraints.  They usually do so by adding
English comments, which are about as far from being machine readable
as one could imagine.  They avoid the problem you are worrying about
by not mentioning it:  they say that the EBNF spec is "the grammar"
and that the English is a "normative part" of the standard, but they
don't call it part of the grammar.

PH> [Re MathML] ... That seems mostly concerned with issues which arise
 > from using XML to identify display properties which are totally
 > orthogonal to the logical form. That is a real issue in the XML world
 > where XML serves both as textual markup and as a structural
 > description (we met this issue in a small form in the RDF spec), but
 > I think this is a slightly different issue to ours.

I agree that the MathML goals are different, but they are struggling
with the same problem:  defining the constraints on bound variables
that go beyond the context-free capabilities of XSLT.

Re Schematron:  I followed the pointer to the Schematron tutorial, which
led me to other pointers to XMLCL (XML Constraint Language).  Both of
those languages seem to be hacked up subsets of Horn clauses written
by people whose knowledge of logic is questionable.

My major concern about Schematron or XMLCL is that I have no confidence
in their logical foundations, and I seriously doubt that their rule
languages support the kind of recursion one would like to use for
checking arbitrary nests of quantifiers.

I would much rather state the non-EBNF rules in well-written English
supplemented by formal statements written in a subset of SCL.  I believe
that SCL rules should be at least as readable as rules in Schematron
or XMLCL -- and we know that SCL has a solid semantics.

Recommendation:  I suggest that we state all formal definitions of
SCL in some SCL concrete syntax (either the KIF-like dialect or the
infix dialect of SCL).  We have already discussed the idea of stating
the spec's in English and putting the more formal notation in a
normative appendix.  Let's just use SCL itself to write the appendix
instead of using any other notation.

And by the way, that is how the ISO standard for Z is written.
They use Z statements supplemented with English comments to define Z.
We can do the same with SCL instead of Z -- and include a translation
of EBNF to SCL as a normative specification that also serves as an
example of the use of SCL.

John