[SCL] further telecon elaborations

[Tanel Tammet]

Hi,

After Bill commented on my previous elaborations, I gave the
clarifications he  asked for, but then thought a few further elaborations
might be useful.

In the following I'll not propose or add anything new, just  explain
further how I'd understand the process of writing converters and
what help the converter-writers could expect from SCL papers.

Everything what follows is written purely from the viewpoint
of an implementor: no "real logic" involved.

First I repeat the introduction from the recent message:
------------------
Let us consider a very obvious, realistic scenario where we
have an implementation of a FOL prover, called, say, FOLPROVE.
FOLPROVE is able to read input files in its own syntax FOLPROVESYNTAX.

We will want to use FOLPROVE in a situation where we get various
bits of knowledge from various sites, each providing one
file. Say we have four sites:

S1: provides a file AX1 in SCL concrete syntax 1.
S2: provides a file AX2 in SCL concrete syntax 2.
S3: provides a file AX3 containing RDF and RDFS.
S4: provides a file Q1 containing FOL in some traditional,
    concrete FOL language.

Now we want FOLPROVE to check whether (AX1 & AX2 & AX3) => Q1.
Certainly the FOLPROVE people will have to write utility
programs for translating the languages to FOLPROVESYNTAX.
So they will have four translators:

t1: SCL concrete syntax 1 -> FOLPROVESYNTAX
t2: SCL concrete syntax 2 -> FOLPROVESYNTAX
t3: RDF, RDFS -> FOLPROVESYNTAX
t4: "some traditional, concrete FOL language" -> FOLPROVESYNTAX
---------------

Further (trivial, on purpose) details about how I'd see the 
converter-writing
process follow:

A) The writers have:
    - a limited knowledge of some concrete logical syntax X
      (just based on reading the description: for example, present
       in SCL papers if X is one of  the SCL concrete syntaxes)
    - good knowledge of "traditional FOL"
    - specific knowledge about FOLPROVESYNTAX and
      its relations to "traditional FOL".

B) Our aim is to help the writers to write X->FOLPROVESYNTAX in a manner
     that the translations from different X-s would be compatible.

One way to do this would be to provide following chapters in the
SCL papers:

1) SCL abstract syntax and semantics as we have (observe these are currently
    "abstract": I understand "abstract" here in the sense that the 
lexicon (and even
     some structures) used when defining these two items are NOT 
obligatorily to
    be used by the converter writers).

   I'll call these two items (abstract syntax and semantics) SCLSYNSEM 
in the
   following. It will be used as a central "glue" between several languages.

2) What we do not have yet: a conversion algorithm from SCLSYNSEM
    to "traditional fol". The level of abstraction in our usage of 
"traditional fol"
    in this place should  be low. In particular, the lexicon (concrete
    predicate and function names, names for App/Holds (if used), names
    for datatype constructors (if used)) and the exact meaning of 
quantifiers
   (over which lexicon they are going to range over) have to be fixed!
   
   Probably the names of  connectives (whether to use "and" or "&" etc)
   and the placement of parentheses may be left "abstract", since no
   confusions are likely to happen there.

3) What we do not yet have: several concrete syntaxes X1,X2,X3 for SCL
    along with their mapping to abstract syntax and semantics.

4) What we do not yet have: a concrete mapping of "traditional FOL" to
     SCLSYNSEM.

5) What we do not yet have: a concrete mapping of RDF/RDFS
    (which syntax should be used?) to SCLSYNSEM. Of course,
    this mapping is almost there in Pat's semantics of RDF/RDFS,
    but not given exactly for SCLSYNSEM. I have always assumed that a 
part of Pat's
   aims for SCL stem from a wish for such a SCLSYNSEM.

6) What we do not yet have: a special guide chapter for converter writers,
    giving an overview of the process as described above.

If we have all this, then any converter writer can proceed as
follows:

X1 -> SCLSYNSEM -> "traditional fol" -> FOLPROVESYNTAX
X2 -> SCLSYNSEM -> "traditional fol" -> FOLPROVESYNTAX
X3 -> SCLSYNSEM -> "traditional fol" -> FOLPROVESYNTAX

where:
  - the last arrow is implemented by one single program used
    during the translation of any X
 -  the arrow between SCLSYNSEM and "traditional FOL" is
    probably a mental process of the converter writer, not
    a real program converting two different data structures
 - the main task of the converter writer is to write
    a program X -> "traditional fol" using the methods
    prescribed in the SCL papers.
 - the people working on FOLPROVER will eventually
    write specific optimisations for the kinds of  files they
   expect to get from the translation: this is not really
   our business any more.

In such case we will have compatible translations for various X-s (assuming
everything is done right).

Observe that one possibility would be to avoid having
an abstract SCL semantics part in the SCL papers and
use a conversion algorithm from SCL abstract syntax to
"traditional FOL" (with a fixed lexicon and defined meanings
for the elements of this lexicon) instead. Since the semantics
of the latter is a de facto standard, we will have SCL
semantics described (not directly, but via FOL).

This approach might simplify writing the rules for
the various translations as indicated above, since
the converter writer could proceed in fewer steps
(no need for the mental arrow SCLSYNSEM -> "traditional fol"),
as follows:

X -> "traditional fol" -> FOLPROVESYNTAX

which will make it easier to write the converters.

I am not actually advocating dropping the current
abstract semantics (it is a very nice tool to have). Just
turning attention to that we could use a slightly different
(perhaps  additional) approach as well.

To summarise, I tried to stress that we should also
think about writing the concrete mapping between the
current SCL and ordinary FOL, possibly with some
predefined/prescribed lexical items. Abstract syntax
and semantics, although necessary, are IMHO not sufficient
for actual usage.

Regards,
           Tanel Tammet