[SCL] Re: Folding unnecessary [was: Re: Update to SCL-related work]

[Tanel Tammet]

Hi,

After all this fruitful folding-thread I have got the impression
that there is a really simple solution that should satisfy all the
requirements or objectives we have.

This is basically your header idea, but formulated in a
lexical context, not syntactical. I'll give the details
in the following (there is nothing really new, just
(important) nuances).

In particular, I see no need for folding: although I thought
for a while that folding would be nice, we can achieve
everything we need by much simpler means.

Coming back to roots, what do we want to achieve?

1) Possibility to give properties to functions/predicates,
    which requires that functions/predicates have
    associated constants. The non-contested way to
   do this is via  app/hold encoding.

2) Possibility to express traditional FOL sentences in
     SCL, with EXACTLY the traditional semantics.
     In particular, I should be able to say in some
     concrete syntax (say, SCL-KIF) that
    (forall (x) (and (P x) (not (Q x)))
    and this should be satisfiable on a domain with
    only one element, which would be impossible
    if we translated the formula with  app/holds
    encoding. This would automatically take care
    of the horrocks sentences as well.

3) Keeping the SCL concrete syntaxes simple
     and traditional, with no weird/complex
     constructions.


All these things are - fundamentally - questions
about SCL concrete syntaxes, not the underlying
MT, where we can use conventional FOL with
no tricks.

The suggested way to  go is the following.

We have one unstructured set of domain elements,
and the goals above are achievable using lexical
conventions plus a number of axiom schemas.

In any concrete SCL syntax we split the names,
i.e lexical items for constants/predicates/functions
into several sets:

- ordinary constants (like a, c1, bbx)
- numeric constants (like 0, -2, 10)
- string constants (like "aab", "1")
- possibly date and time constants (like 01.02.2004)
- special function and predicate names: any name
  prefixed by ! is a special name (like !f, !P)

These sets are strictly different lexical categories:
a numeric constant is not a string constant, is not
a special function, etc. We have to give the lexical
definitions in EBNF for all these names, preferrably
keeping them the same for all SCL concrete
syntaxes.

So far this has nothing to do with model theory.

Next, we will give a syntactical restriction, saying
that special function/predicate names can NOT
occur in argument positions: they are only allowed
in function/predicate positions. This is an ordinary
restriction used in many conventional FOL presentations.

All the other constants (except, perhaps, numeric/string/date
constants) may appear in any position, including the
predicate/function position.

For example, it is syntactically OK to say in SCL/KIF that
(p a), (p p), (!r 1), (!p a)
but it is not OK to say
(p !r), (!r !r)

The semantics of SCL/KIF and other concrete languages
are given by their translation to SCL abstract syntax.
Abstract syntax is exactly conventional FOL with no extra
machinery added. Translation uses app/holds if the predicate/function
symbol is not a special predicate/function. If the
predicate/function symbol is special, no app/holds
is added.

For example:

(p a)   -->  holds_2(p,a)
(p p)   -->  holds_2(p,p)
(!r 1)   --> !r(1)
(!p a)  --> !p(a)
((f p) 1) --> holds_2(app_2(f,p),1)
((!r p) 1) --> holds_2(!r(p),1)


What we have now is that any conventional FOL formula
can be written in any SCL concrete language: one should only
use the predicate/function symbols prefixed with the exclamation
character !

In case you do not use the exclamation character, the functions/terms
are converted to app/holds. In particular:

- atoms/functions led by variables are converted using app/holds
- atoms/functions led by function applications are converted using app/holds

This schema satisfies all the three requirements we had in the beginning.
We can give properties to functions/predicates, we can write conventional
FOL, there are no special syntactic constructions in SCL concrete syntaxes,
the model theory is a purely conventional FOL model theory with no
modifications.

The lexical differences are present in any conventional formal
language anyway. You have numbers, strings, functions, all with
defined lexical differences and restrictions for their use in
syntax. Prefixing something with a special characer like !
is a conventional approach.

Observe that:

- There is really no need for folding any more: the function/predicate names
   with conventional FOL meaning are always different from the other names.
   It cannot happen that in one text (p a) means app_2(p,a), while in
   another it means p(a). You'd have to write (!p a) to get !p(a) in
   abstract syntax. !p is different from p.

- There is really no need for two equalities any more: the ordinary
   (strong) equality is fine, since the horrocks sentence should be
   written with exclamation marks, and then it is FOL with no
   app/holds encoding.

- SCL has the conventional FOL MT, with zero
   changes. This is pretty important! You might
   perhaps personally love to invent some clever
   modifications or additions, but this will inevitably
   doom any widespread use of  SCL.

   Observe that once the weird/complex constructions
    are present in MT, all the lemmas we know about
    FOL go out of the window and have to be proved
    again. This would be a nightmare for implementors:
    I'd have to think whether, say, resolution method
    is still correct and complete and what changes
    are necessary, and I'd have to think all the
    search strategies over again, proving their
    completeness: a horrific task people will simply
    not undertake. They'll rather avoid SCL.

   Simply saying that "all the conventional FOL
   stuff still holds" would be just empty speech
   unless proofs are given, and you cannot give
   all the necessary proofs: there are far too many
   of them. Even if you give the proofs, people
    will still be suspicious, but will lack the time
   or initiative to read or check the proofs. Again,
    they'll rather avoid SCL.

Why is the lexical approach better than the header approach:

- The meaning of terms is not dependent on context (except
  for the variables, where the bounding quantifiers give the
  meaning).

  With the header approach the meaning is dependent on the
  header context. Whenever you copy/paste a formula
  into another formula, you'd have to check that contexts match.

  This may be fine in RDF, XML and namespaces, but I find
  it intolerable if we assume that SCL may be used outside
  the semantic web context as well, or in a situation where
  namespaces are really not used or cared for.

- It is much easier to understand the SCL description
  if there are no headers.

- Headers can still be used in concrete SCL syntaxes, but
   for conventional purposes:

  a)  giving abbreviations to namespaces (like we do in XML),
      so that we can write (foo:p 1), with foo being a header-defined
     namespace.

     Observe that this is different from the exclamation thing:

    (foo:p 1) and (foo:!p) would still have two different
    translations, regardless of which URI "foo" stands for.

  c) indicating character sets (various UTF-s and ISO-s)
 
  d) including other SCL files: this amounts to including
      theories/knowledgebases/data, formed of SCL axioms
      (different files may contain different data)

   e) possibly giving some metainformation out of SCL
       scope.
 
   All these applications of headers would be in the
   conventional lexical or meta-level, not changing the underlying
   semantics of SCL formulas a bit.


Finally I have some notes on data types: numbers, strings,
etc. The XML schema datatypes are a complex structure
and the W3C documents contain no axioms we would need.

I will describe why the approach taken in ECL is a necessary
approach.

We have to axiomatise ourselves that numbers are
different from strings and two different numbers are
different, etc. We cannot simply point to the W3C documents
for datatypes, since they contain no such axioms (they
cannot, since they do not use any logic, in particular they
do not use SCL, which does not even exist before we publish
the SCL description).

Fortunately, the axiomatisation is not hard: I wrote it
down in the ECL paper, in a conventional way.

In order to make datatypes easy to use and understand,
we have to define and axiomatise a few basic datatypes
with all details. We have no time or initiative to do this
for all XML schema types. Instead, we should then
give a detailed description of how to add new datatypes
as modules to SCL.

The basic datatypes like integers and strings should
be defined lexically.

All the new datatypes should be created by constructor
functions, like boolean(0), analogously to lists,
where cons(0,nil) creates a list from a number and a list.

Regards,
           Tanel