[SCL] Proposed additions to the SCL draft standard

[Tanel Tammet]

Chris Menzel wrote:

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

Not necessarily. See below. We do not have to give any 
meta-interpretations to the annotation items in our language.

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

I agree to that "in a classical semantics all terms must have a semantic 
value.". The suggested way of including annotations does, IMHO, do
it, once we add the domain of annotation strings to the semantics (I did
not add this: a correctable mistake).

What about this:

- What I had suggested:

   Use the function symbol Annot and a connective Annot (might be two
   different names) for annotating terms and formulas.
   Annot may take an arbitrary number of arguments:
     - the first argument is the annotated term (or formula)
     - all the other arguments are annotation entities (strings do fine)
   Then define in the SCL semantics:
   - for terms: Annot(trm, a1,...,an) = trm
   - for formulas: Annot(frm, a1,...,an) <=> frm

- What needs to be added:

   Let us take a new set of objects ANNOT as a domain of
   annotation entities (strings in concrete syntax).
   Let us say that each annotation entity is mapped to ANNOT.

   This is no different from the way we treat ordinary constants.
   If we so wish, we could IMHO even use ordinary constants or integers
   as annotations (the definition of the Annot function and connective
   is all that matters), but this might get confusing: I guess it would
   be better to have a separate domain of annotations, ie keep ANNOT
   (domain elements, not lexical entities) disjoint from other domain
   sets.

It looks to me that in this case we do have an ordinary first order
semantics for everything about annotations.

BTW, such an Annot looks very much like a K combinator: it keeps the 
first argument, unchanged, and throws away the rest.

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

Sorry, I misread that paragraph before. You have the semantics
for the restricted quantifiers described.

This part of your text looks a bit complex though: wonder if it
would be possible to present this part in simpler terms or
more details. The rest of the SCL draft is easier to read than
the particular part about the meaning of the restricted quantifiers.

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

I have written the paragraph up here real badly.
Literally taken, it is a wrong claim.

One could take the definition of plus and then say something like
forall x,y . ((exists n . (x=y+n or x+n=y)& (n!=0)) => x!=y)

What I guess would be right, though, is that:

- If we have numerals explicitly in SCL, it would be
   easier to use ordinary, decimal integer representations
   during actual usage of SCL.

   Otherwise some people would
   have a tendency to use the successor notation, some
   would come with a binary (bitwise) encoding scheme,
   while some would use numerals. The actual formulas
   in concrete syntaxes would probably represent integers
   in different ways.

- When we consider actual implementations proving theorems,
   then it is badly inefficient to use axioms like the one
   above for basic integer functions and predicates (equality
   of two integers is a good example). It is normally a good
   idea to build in some basic operations while using
   axiomatisations for all the rest.

   It seems to me (though I may be mistaken) that it would
   be advantageous for implementors to think like "ok, these
   basic operations like equality of two integers should perhaps be
   built in, since we have a special domain for integers and
   special numerals in the language anyway".

   I know: what I said here is vague. One could build in parts
   of arithmetic without any special support from SCL or like (have
   done that myself). Strictly speaking, we would not
   need "help" from SCL for that. However, as I said, IMHO it will
   be a nice guide for implementors to have integers in the
   SCL.


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

I am not suggesting to put in strings and other kinds of
types into SCL.

I was trying to say that it would be easier for users to define
their types (strings, for example) - all doable in FOL -
once they have integers in the language.

You are of course right in that this is not really the SCL
business (and "ease" is a very vague notion anyway), but
since I am thinking about the implementation aspects all
the time, I do have a tendency to stress the implementation
aspects. Hence I also think that we should pay some attention
to implementation issues: not the critical point for
SCL, but not irrelevant either.

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

OK! That was very nice you actually had the mechanism for writing
the standard "object" equality. No real need to have a second equality
once we have the Ind predicate.

> I don't think the semantics for predicate-bounded quantifiers will be
> genearalizable to a semantics for numerical quantifiers.  

I did not think really generalising the existing semantics:
just adding the feature.

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

Again, my mistake. Meant "satisfiable". The formula above
is not satisfiable in SCL, while it is satisfiable in FOL
(a domain with just one object suffices for satisfiability).


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

Another way to look at it is the following question:
which kind of these two kinds of quantifiers:
- (forall (?x Ind) ...
- (forall (?x) ...
should be the DEFAULT (ie, shorter to express)?

One could perhaps take an approach that
- (forall (?x) ... means what you meant by (forall (?x Ind) ...
    before,
- we use something like (forallwithpredicates (?x) ...) for a
   "free" case,  where we quantify over predicates.
Just a matter of defining the meaning of a quantifer.

The possible advantage of the latter is that it would be less confusing
for "ordinary FOL" people. Just writing a quantifier with no
special modifications would mean a standard FOL quantifer, while
a non-traditional, RDF-ish quantifier would require extra writing
and be clearly identifiable as something unordinary.


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

Indeed, I am getting into the metalinguistic issue with the "include"
construction (I was not realy getting into metalinguistics with
the annotations).


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

Right. I have currently no idea about what would be the
proper place, hence I did not try to put it into the
suggested additions to SCL draft: just wanted to turn
attention to the issue.

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

I have no idea about how could we have a logical
status for the include (differently from the annotations,
where we can have a trivial logical status).

Hence I guess - seems you do as well - that the "include",
in case it would be added to SCL, should be outside logic.

This does not mean, however, that we cannot put it into
SCL (for example, by putting it into yet another layer
and saying that the "include" mechanism is not a part
of the logical meaning of SCL at all: just markup
with a procedural meaning.)

Thanks for the most detailed answer and clearing up a lot of
issues!

Regards,
         Tanel Tammet