[SCL] Proposed additions to the SCL draft standard

[Chris Menzel]

On Sun, May 25, 2003 at 02:38:24PM +0300, Tanel Tammet wrote:
> 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.

This is the right thing to do!

> These "new" features have been discussed a lot on the SCL list, but
> they are not present in Chris's minimalistic SCL draft.

Yes, there are several things missing, and I'm sure I omitted other
things in my haste to get a first-cut document up -- your msg is exactly
the sort of thing I was hoping to see!

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

Yes.

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

I've upped the limit to 500k.  Sorry I didn't think of that when I set
up the list.  To help with organization, I have created a "mods"
directory under the scl 1.0 dir and have renamed the file to
scl-1.0-mod1.html.  So the complete URL for this document is:

http://cl.tamu.edu/docs/scl/1.0/mods/scl-1.0-mod1.html

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

Very good idea.

> 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.
> 
> Found a few parts of the SCL draft which contained errors or were in
> obvious need for further details.  

Thanks.

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

I have no problem with this sort of split.  I do have questions about
the contents of the levels.

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

I think this falls under the notion of conformance.  I was going to
propose adding the notion of a conformant sublanguage of SCL, similar to
the notion in the full CL document.  Would you mind having a look at
that to see if you think it does the job?

> - Annotations (might be called also comments or documentation
>   strings). Free text (strings) may be attached to terms
>   and formulas.

I see the need for annotations in SCL implementations, but the suggested
approach won't work.  You propose including them as terms.  But the
underlying logic/semantics of SCL is classical, and in a classical
semantics all terms must have a semantic value.

If some sort of annotating facility is going to be added, it must be
thought of as some sort metalinguistic device.  Hence, if we agree some
notion of annotation is important, then we need to have a section of SCL
that describes such a device, and offers counsel about how to implement
it.

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

Yes, we talked about this at some length at the last telecon.  There
seemed to be general agreement that such quantifiers are necessary and
useful.

>   I have NOT defined the semantics of integer-bounded existential
>   quantifier in the text, since the predicate-bounded existential
>   quantifier was not defined either...

Not sure what you mean.  As noted in the document, the syntax permits
things like (in a KIFish language):

(forall ((?x Boy))
        (exists ((?y Girl))
                (Kissed ?x ?y)))

and the semantics for this is captured explicitly in the notion of a
[X_1,...,X_n]-variant of a variable assignment; see the second full
paragraph in the section Denotations and Truth, especially the first
of the two bullets that end that paragraph.

>   Motivations:
>     - 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.
>       As we know, this CANNOT BE DONE IN FOL. 

I'm not sure what you mean.  There is a very simple theory of
first-order arithmetic that has as consequences "m =/= n" for any
distinct numerals m and n.

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

You're losing me.  I believe you are talking much closer to the level of
implementation than is any of SCL's business.

> Small errors and omissions found:
> 
> - In the early part of text the name of the identity function
>   used was Ind, not Id as later.

No, Ind was supposed to indicate a distinguished predicate that applies
to the non-relations of the domain; it should have been listed as a
distinct distinguished predicate.  In the semantics, I see now I
neglected to give the proper semantics to Ind and neglected Id
altogether...ugh!  I'll fix this ASAP.

> - The semantics of quantifiers bounded by predicates was IMHO
>   not defined. 

Not so, as noted above.

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

I don't think the semantics for predicate-bounded quantifiers will be
genearalizable to a semantics for numerical quantifiers.  But it will be
easy enough to implement an appropriate semantics.

> - XML DTD was IMHO not complete: again, the possibility for
>   bounded quantifiers was not there in the DTD. 

Yes, that was an oversight, thanks.

> Some serious extension possibilities worth considering (not introduced
> as proposals in the attached text):
> 
> - Identity (equality) on the object level.

Already supposed to be there, as noted, just poorly defined!

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

No it isn't.  It's false, e.g., in any interpretation whose domain
contains more than one thing, and in which everything is P and nothing
is Q.  It's not valid in SCL either.  Perhaps you are thinking of
something like the following:  

     (implies
        (forall (?x) (iff (P ?x) (not (Q ?x))))
        (not (forall (?x ?y) (= ?x ?y))))

which is invalid in standard FOL but valid in SCL.  ("P" and "Q" both
denote something in SCL, but since those denotations have different
extensions, they must denote distinct things.)  I agree we need to think
carefully about these issues.  The purpose of the "Ind" predicate was
basically to restrict quantifiers to non-relations to get the right
sorts of correlations with standard FOL.  Thus, the result of so
restricting the quantifiers in the formula above:

     (implies
        (forall (?x Ind) (iff (P ?x) (not (Q ?x))))
        (not (forall (?x ?y Ind) (= ?x ?y))))

is NOT valid in SCL.  But again, this is worth a lot of thought.  We
need in particular to convince ourselves of the advantages of allowing a
"free" syntax in which predicates can occur as arguments to other
predicates.

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

No, the properties of identity would be not change.

>   This might be survivable, but is really unpleasant, since it
>   unnecessarily limits or confuses our audience.

That is to be determined.

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

I don't think this will do that job, but I'm not positive I understand
you.  I suspect what we'll have to do if this is a genuine concern is to
generalize the semantics to allow for classes of interpretations in
which predicates are interpreted in the usual way, and do not take
denotations in the domain.  I'll try to work something up like this in
the coming week.

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

Again, I believe you are getting into metalinguistic issues and issues
of implementation -- very important, of course, but we need to remain
clear about where all the pieces fit.

>   If we want to put this into SCL (and why shouldn't we?) 

We may well want to put it in, but in the proper place!

>   we do need an "include" operation.  Include should IMHO take an URI
>   as an argument and return the text at the URI. 

You are confusing object language and metalanguage here.

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

So that argues for describing mechanisms for SCL language
implementation.  I agree this is important.  It is also important that
we are clear where it belongs and what it's logical status is.

These are really fine observations, comments, and suggestions!  Thanks
for all your efforts.

Pat, can we set up a telecon for Tue morning??

-chris