[SCL] Proposed additions to the SCL draft standard

[Tanel Tammet]

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.

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

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

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


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.

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

     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.

   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.

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

   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.


Regards,
      Tanel Tammet

-------------- next part --------------
A non-text attachment was scrubbed...
Name: sclmodif25may.zip
Type: application/x-zip-compressed
Size: 9856 bytes
Desc: not available
Url : http://philebus.tamu.edu/pipermail/scl/attachments/20030525/f62672b2/sclmodif25may.bin