[SCL] Proposed additions to the SCL draft standard

[pat hayes]

>Hi,
>
>Before additional work on the XML concrete syntax I thought
>that it would be more important to put some new features
>into SCL proper. These "new" features have been discussed a lot
>on the SCL list, but they are not present in Chris's
>minimalistic SCL draft.
>
>If we do not have these features in SCL proper (the
>abstract syntax and semantics), it would not be suitable
>to put them into the XML concrete syntax: the latter
>has to reflect the SCL abstract syntax, not extend it.
>
>I took Chris Menzel's SCL draft from
>http://cl.tamu.edu/docs/scl-latest.html at 24 May
>and added a number of PROPOSED modifications directly
>to it.
>
>Attached please find the modified SCL draft, as
>a zip file (sent a message with unzipped html before,
>but this was too big for the list program).
>
>The additions introduced are proposals. I have colored
>the background of all the additions green, so that it
>would be easier to follow (tested the Amaya editor
>while writing the additions).
>
>Please have a look at the additions and decide whether
>some of them or all of them are in principle worth
>keeping. Once the list of OK additions is decided,
>further modifications to the presentation would
>be suitable.

I am rather unhappy with these multiple 'levels' being in the core. 
They make the presentation much too complex. Let us decide what the 
language is, define it, and then restrict it in various ways to give 
the levels. They will be sublanguages of SCL, in fact, which was 
always the preferred design.  But this is purely a matter of 
presentation; the substantive aspects of your changes I largely agree 
with.

I would prefer to allow arbitrary expressions (including legal SCL) 
as annotations, rather than requiring them to be strings. Strings are 
one option, but I would suggest that we handle this option by 
allowing strings as a syntactic form in the entire language, along 
with numerals, with a distinctive 'recognizing' predicate in a 
special family scl:string, scl:number, so that
|=  scl:string("any character string").


>Found a few parts of the SCL draft which contained
>errors or were in obvious need for further details.
>More about this after the list of proposed additions.
>
>The following is a list of the additions in the
>SCL draft html file along with motivations:
>
>
>- SCL standard is split into four levels or layers.
>
>   Motivation: it is easier to implement a smaller standard
>   than a larger standard. Fancier parts of SCL might
>   be hard to implement/understand for users. It would
>   be good to indicate that even partial implementations
>   may correspond to an identified subset of a standard,
>   if done properly. Othwerwise we stand the serious risk of
>   partial implementations claiming to be SCL, while
>   nobody really knows which parts are implemented and which
>   not (or we stand the risk that very few people take up courage
>   to implement and use SCL at all).

Agreed.

>
>- Annotations (might be called also comments or documentation
>   strings). Free text (strings) may be attached to terms
>   and formulas.
>
>   Motivations:
>    - Obvious need for documentation. Most probably will
>      be implemented in concrete syntaxes. Hence it would be
>      good to define in the abstract syntax, so that different
>      concrete syntaxes would be intertranslatable.
>    - Possibility to encode additional (nonlogical) information
>      for specialised systems in annotation strings.
>      For example, in the automated
>      theorem proving (ATP) context it is really crucial to identify
>      that some parts of the formula stem from general axioms
>      while some parts stem from a specification of a system
>      explored while yet others stem from a query asked.
>      This is absolutely unavoidable for practical ATP needs.
>      And we DO NOT want to go into serius metalogic in the SCL
>      context in order to attack this everyday necessity.
>
>- Integers and bounded existential quantifications (a possibility
>   to say that there exist exactly N objects with some property P).
>   By 'integers' I mean the use of numerals with a predefined
>   property that all lexically different numerals map to
>   different elements of the domain. Ie, not(id(4,7)) holds,
>   no need for a user to define this.
>
>   I have NOT defined the semantics of integer-bounded
>   existential quantifier in the text, since the predicate-bounded
>   existential quantifier was not defined either (see later in
>   the 'omissions' section).

Hmm, I think we need to do both of these. We can show that they are 
eliminable, but that is a separate issue.

There is a general issue here, in fact. There are several cases where 
some sublanguage of SCL is equi-expressive with the whole language, 
in that there is a systematic translation of SCL into a theory of the 
sublanguage which preserves entailment; examples include the 
sublanguages without restricted quantifiers, numerical quantifiers, 
and the conventional FOL syntax (using the holds/app translation). 
There are also others, of course, which eliminate connectives or one 
of the quantifiers in the usual ways. Maybe it would be discussing 
these all together and giving a general account of this kind of 
'expressing in a sublanguage' idea. It occurs to me that taking a 
very simple SCL expression and showing what it looks like in, say, 
the holds/app translation using only and, not and exists, might be an 
instructive exercise for some readers.

>
>   Motivations:
>     - OWL Full contains bounded existential quantification.
>       While this can be encoded in plain FOL (or SCL), it is
>       pretty cumbersome. Would be more convenient to use integers
>       in the language.
>       Once we do allow to use bounded existential quantification,
>       it would be a bit weird not to allow integers in general.

Agreed. Integers (well, numerals) were always on the table.

>     - Integers and integer arithmetic is, not surprisingly, very
>       important in many practical ATP fields, like verification.
>       Essentially, you have to build in integers and arithmetic
>       for doing practical verification of hardware (electronics,
>       railroads, etc). You have to build in integers for creating
>       e-commerce system rules, etc (think prices, quantities of goods,
>       etc).
>     - Integers are not just syntactic sugar. It is not enough to
>       decide that, say, let us use 0 to denote 0, s(0) to denote
>       1, s(s(0)) to denote 2, etc.
>       The crucial issue is that you need to define that 1 is not equal
>       to 2, 3 is not equal to 7, etc for all pairs of integers.

I think you need the ordering and we also need a built-in connection 
with the length of a sequence. This actually gives the language 
considerable expressive power, since it effectively builds-in 
numerical induction.

>       As we know, this CANNOT BE DONE IN FOL.

Its not clear if it can be done in SCL with seqvars, however.

>This can be done
>       only using induction. However, it is easy to PREDEFINE that
>       different numerals map to different integers in the domain,
>       essentially building in the infinite list of disequalities
>       (similar to the equality predicate, which also cannot be defined
>        in pure FOL).

Right.

>     - Once we have integers in the language, we could in principle
>       (if we want to) encode strings and string equalities as
>       integers (for example, by using ascii or utf) along with
>       the ascii or utf string type constuctor taking an integer as
>       an argument. Strictly speaking we would not need to extend
>       the core language to encode strings (or any other datatypes,
>       for that matter: integers suffice, at least theoretically).

Yes, but the same convenience arguments apply. After all, we could 
axiomatize arithmetic if we really wanted to. Strings are extremely 
useful in a number of application areas.

>Small errors and omissions found:
>
>- In the early part of text the name of the identity function
>   used was Ind, not Id as later.
>- The semantics of quantifiers bounded by predicates was IMHO
>   not defined. This needs to be done. Once it is defined, the
>   definition can be extended to the existential quantifier bound by an
>   integer (not done in the proposed additions).
>- XML DTD was IMHO not complete: again, the possibility for
>   bounded quantifiers was not there in the DTD. Hence I have not
>   put in the integer-bounded quantifier into the DTD either.
>
>
>Some serious extension possibilities worth considering (not introduced
>as proposals in the attached text):
>
>- Identity (equality) on the object level.
>
>   Chris mentioned that once we encode predicates using the App/Pred
>   functions, the formula (forall x. P(x) & -Q(x)) & (forall x,y. x=y) is
>   NOT valid, while it IS valid in the standard, non-app/pred semantics
>   of FOL.
>
>   This means that it is very hard to use SCL for encoding
>   standard logical problems, including a large part of the
>   thousands of problems in TPTP, used extensively in the
>   ATP community. People cannot use Id in these contexts:
>   they'd have to define their own equality not present
>   in SCL and not axiomatisable in pure SCL alone.

All we need to do is to restrict the quantifiers to the subuniverse 
of non-relations, by adding scl:relation(?x) to every clause for each 
variable in the clause. The same equality predicate works.

>
>   This might be survivable, but is really
>   unpleasant, since it unnecessarily limits
>   or confuses our audience.
>
>   We could use the App/Pred-based SCL for standard FOL problems
>   IF:
>    - we explicitly identify a "simple" subclass of SCL where any first
>      arguments of App and Pred are constants. This subclass
>      can be trivially mapped to non-App/Pred, classical
>      semantics (just drop the App and Pred and lift the first
>      argument to the function/predicate symbol position: validity
>      of formulas is not changed by this transformation).

Yes, we intend to do that: that is one of the primary SCL 
sublanguages and it has a 'special' model theory in which the 
extension mappings are all identity mappings.

>
>     The "simple" subclass can be extended, of course, allowing
>     cases where a variable is used in the first argument: the
>     mapping will be harder, though.
>
>   - We do provide an equality predicate on the individual
>     constants only: ie, not usable on predicate/function name
>     constants.

In this sublanguage, the restriction to non-relations can be limited 
to the identity. This can be viewed as a different identity, but I 
think it is actually clearer and simpler to keep this understood as a 
quantifier restriction.

>
>   Observe that the current Id predicate is NOT such an
>   individual-constants only predicate.
>
>   Also, the current
>   SCL does explicitly differentiate between object constants
>   and function/predicate constants, simplifying the introduction
>   of the second equality predicate.

Yes, that was the primary purpose of that change.

>
>   Hence I suggest to:
>   - write a chapter identifying the "simple" subclass of SCL
>     and properties of its semantics,
>    - introduce the second equality predicate, different from
>      Id, defined only on the object constants.
>
>
>- Including other text.
>
>   Both in the semantic web context and "ordinary" ATP it is
>   important to import other files or parts of other files into
>   the formula.
>
>   If we want to put this into SCL (and why shouldn't we?) we
>   do need an "include" operation. Include should IMHO take an
>   URI as an argument and return the text at the URI.

Hmm..text?? What if the text found there is, say, OWL-DL rendered in 
RDF written in XML. It would be a lot more use to use for the URL to 
dereference to a standard SCL translation of the 'logical form' of 
this, than to the raw text.

Suggestion: (ambitious?) : have a 'web SCL ontology' which has 
special built-in vocabulary which maps between forms of ontologies, 
eg at(..) is a function from a URL to the text found there, as you 
suggest (though see later), Is-RDF(..) is true of a string which is a 
legal XML encoding of RDF, XML-to-RDF is a function from such strings 
to RDF  graphs (ie a parsing function), similarly RDF-to-OWL parses 
an RDF graph into OWL, and so on. Then we can write things like
Is-RDF(at(?x)) and Is-OWL(RDF-to-OWL(XML-to-RDF(at(?x)))
implies
trans(?x) = OWL-to-SCL(RDF-to-OWL(to-RDF(at(?x))))

and subsequently use trans to 'import' an ontology.

>In case
>   namespaces or any external links are used in the text referred
>   by our URI, these namespaces and/or links should be resolved
>   before including the text (a simple recursive process).
>
>   If we do NOT put "include" into SCL, then inevitably people using
>   SCL would have to construct their own inclusion constructions,
>   different for different concrete syntaxes and users.

Yes, but on the other hand, take a look at the OWL mess to see how 
complicated this gets, with 'deprecated symbols' and so on.

>
>   Observe that the XML concrete syntax would not automatically
>   introduce the linking possibility. Pure XML provides us with
>   namespaces, but does not provide including text. We could
>   try to use additional XML-based languages like XLINK, but
>   these are highly complex. IMHO it would be better to put
>   text inclusion into SCL directly, as an additional layer.

I basically agree. The key point is that we need to provide some 
syntactic way of distinguishing a URIref used simply as a logical 
constant, and a URI (maybe also a URI ref) used as a Web identifier 
of a page of hypertext. The use of 'at' above kind of glosses over 
this by making that function use the latter sense by magic, but it 
would be better to have a more principled way to make the distinction.

I think we are unlikely to have time to get this finally right; it 
isn't even clear what it means to quote hypertext, in fact. The best 
we will be able to do is to provide a useful 'hook' for a more 
ambitious later project.  BUt that would be well worth trying to do.

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