[SCL] Re: Update to SCL-related work

[Pat Hayes]

>Hi,

Hi Tanel, good to hear from you.

>During the last few days I have significantly
>updated the ECL language (SCL branch).
>
>Have a look at
>http://www.ttu.ee/it/elm/ecl.html

Most impressive. It reads very well, for sure. I like your way of 
handling the abstract syntax as in-line constructors, and how it 
trivializes the CL-FOL translation.

>Main changes:
>
>   - Principal changes in the data type
>     (numbers, strings, etc)  handling.
>   - Chapters for two concrete syntaxes
>   - Adoption of the KIF-like syntax in
>     most examples and axioms
>   - Restructuring the chapters
>
>As said before, it would be great if we
>could ever merge SCL and ECL.

I agree, we should look at this seriously. I'm in the throes of 
making SCL be more XML-based, so that XML is both the interchange 
syntax and also the abstract syntax, and things like your ECL 
notation and the SCL core (and others) are 'dialects' which can be 
seen as ways of rendering the XML. Most of them could literally be 
that, defined by a CSS style document. However on reflection, it 
would be neater to adopt your abstract syntax style, and then have an 
XML encoding of it as a separate matter. That could be the basis for 
a merge, maybe?

>From my viewpoint (other people might have
>very different considerations) the
>following things should be done with
>the SCL draft Pat has been writing:
>
>- Clarification of the basic semantics.
>
>   As it stands now, I cannot really understand
>   all the details there, and this leaves
>   two main possibilities:
>
>    - perhaps the SCL semantics is
>      objectively much more complex
>      than FOL semantics

What it boils down to is that an SCL interpretation is like a number 
of classical FOL interpretations all combined (folded) together.

>    - perhaps it is written down in
>      a far too complex way.

Yes, Im sure it is.  The text is partly the result of my trying to 
explain the (evolving) ideas to myself, and has some legacy from this 
process.

>  IMHO: an easy-to-understand FOL-based
>  semantics is crucial for a language
>  like SCL.

The semantics as it stands is FOL-based. It can't be exactly a 
conventional FOL model theory because we don't have fixed signatures.

It would be considerably simpler if we were to just assume that all 
relations and functions are in the universe. This is what we used to 
do, of course, and (I think) it is what ECL does.  However, the proof 
theory does get strange when we do that, and we lose the 
correspondence to classical FOL (ie, SCL that looks like GOFOL isn't 
in fact what it seems to be. The current semantics preserves GOFOL 
SCL as being indeed classical FOL.)

In terms of your Trad translation, what the current SCL does, in 
effect, is to translate

Trad(Atom_n(e1,...,en)) ==> Atom_n(Trad(e1)....Trad(en))

when  e1 occurs in a referential position, but as

Trad(Atom_n(e1,...,en)) ==> e1(Trad(e2)....Trad(en))

when it does not; and similarly for terms. (More exactly, it ALLOWS 
both such translations in the latter case.) That of course preserves 
SCL-gofol syntax, so if you start with SCL that happens to be 
classical FOL, it stays being classical FOL. Now, to head off your 
objection, this sounds like a very bad idea when described in terms 
of translations, since it means that the translation varies with the 
textual context. And I agree, that would be a bad translation 
strategy for processing SCL in any kind of interoperation setting 
when new information could be arriving later.  However, that isn't 
how its described: and as a model theory, it has the merit of 
supporting a uniform translation (along the lines you describe, but 
paying attention to the need to restrict quantifiers in some cases) 
but also preserving the meaning of classical FO syntax precisely by 
allowing the uniform null 'translation' of classical FO text into 
itself. So how Id describe the SCL==>GOFOL translation is as follows.

1. GOFOL is a subset of SCL syntax, and is FO-satisfiable just when 
it is SCL-satisfiable and with the same interpretations. So SCL 
'contains' GOFOL exactly.

2. In addition, one can translate any piece of SCL syntax uniformly 
into GOFOL using a particular vocabulary based on the abstract 
syntax. This can be done in two ways:
2a (as above) preserves GOFOL syntax and embeds non-GOFOL syntax and 
preserves GOFOL interpretations exactly, but is 
text-context-sensitive (translation of an atom varies depending on 
surrounding text) so unsuitable for some applications
2b (as in your document) is simpler to describe, embeds all syntax 
uniformly and is context-free, but does not preserve GOFOL meanings 
exactly because in some cases it enlarges the universe. There are 
several ways to handle this, of which the one you prefer is to 
distinguish two kinds of equality and the one I prefer is to 
introduce a type of 'real things' to delineate the original FO 
universe, and restrict the translated quantifiers to that domain.

However, whatever we do, I would like it to be that the SCL standard 
*allows* the expression of classical FO syntax without requiring it 
to be re-understood as having an enforced non-FO semantics, or to be 
uniformly translated into a relation-embedded form. Right now, as I 
understand it, that option isn't available in ECL.

>- Equality confusion solved.

I really don't think there is any equality confusion. Equality means 
what it usually means, i.e. I('x=y') = true when I(x)=I(y). The issue 
you have always raised is not two kinds of equality, but two notions 
of what is in the universe (GOFOL individuals only, or also including 
relations). This can be expressed in terms of equality since (x 
exists) is the same as (x=x) , but that is misleading. Equality is 
the same on both universes: there aren't two notions of equality.

>As it stands
>   now, many of the complexities in the
>   semantics seem to be motivated by the
>   desire to fight the Horrocks sentences,
>   which is purely a problem with equality
>   axiomatisation.

It runs deeper than this. Its a problem with the size of the 
universe. Its true that without equality there is no way to 
axiomatically enforce a finite universe, so the examples all use 
equality, but the meta-theoretic point they illustrate holds true 
even for the logic without equality. What we want is that if some SCL 
text is GOFOL, then its FO models are among its SCL models. The 
Horrocks sentences illustrate the objection that with the former SCL 
semantics, this is not the case (because the relations had to be in 
the universe).  It would still be a valid objection in the logic 
without equality. That is what was unacceptable (and is now fixed), 
not a specific equality issue.

>The current SCL
>   approach seems to be the requirement
>   to declare some predicates and functions
>   in a special header,

I will abandon the header idea in the first draft, as it will take 
too long to get the wrinkles sorted out.  For a truly viable Web 
logic I think something like that will be needed, however.

>which I think is
>   a very bad idea (unless the declaration
>   is optional, in which case it is fine).

It always was intended to be optional.

>- Annotations (at least comments) added.

We have those in the SCL core. In the XML they come for free in any case.

>- Crucial data types fully axiomatised,
>   at least numbers, strings and lists.

Right, this needs to be done. It is straightforward, however. There 
is a general scheme for any such axiomatization: it can be infinite, 
remember :-).

Pat


>
>Regards,
>              Tanel Tammet


-- 
---------------------------------------------------------------------
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 ihmc.us       http://www.ihmc.us/users/phayes