[SCL] telecon elaborations

[Tanel Tammet]

Chris Menzel wrote:

> Tanel and I were the only participants, but we had a productive 45
> minute talk.  I have to run to a lunch mtg, but, briefly, there were two
> major topics (Tanel, pls confirm/correct/elaborate as necessary):
> 
> * The importance of developing clear rules for translating an
> arbitary SCL language into traditional first-order form.  The most
> obvious approach here is just to use the Pred_n and App_n predicates.
> Pat and I already worked this out in a currently dormant paper on CL.
> I'll extract it and put it into the SCL doc.  Tenel also suggested it
> would be good to see the precise mapping from RDFS to a fully conformant
> first-order SCL language using Pred_n and App_n.
> 
> * The choice and development of intrinsic SCL datatypes.  Tanel sent out
> a msg earlier today about this, following up on yesterday's discussion
> between Pat and John on the introduction of a very basic theory of the
> integers I will try to distill Pat's proposal into something concrete as
> well.

I'll attempt to make these points more concrete, starting with
the first one.

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

For a moment, let us forget the namespace issues and the
like: suppose all four sites use the same default namespace.

Obviously the FOLPROVE people will create a file F
by appending the utilities-converted files
t1(AX1)+t2(AX2)+t3(AX3)+t4(Q1)
and then feed the resulting file to FOLPROVE.

What they will expect, of course, is that, say, a predicate
P present in all initial files AX1, AX2, AX3, Q will be
converted to the same predicate in F. Otherwise FOLPROVE
is unable to prove the expected things.

What may happen in a negative scenario, though, is that from
SCL concrete syntax 1 predicate P is converted to Pred(P...
while from SCL concrete syntax 2 P is converted to Holds(P...
while from RDF/RDF it is converted to Triple(...,P,...)
while from a concrete traditional FOL syntax it is converted to just P.

If that happens, the whole point (at least for me) of SCL is lost.

Observe that ABSTRACT SYNTAX alone does not help to avoid the
negative scenario. It seems to me that we need to provide
actual rules for converting SCL formulas to traditional FOL.

The rules will then be used by people writing the converter
programs, with the end result that all these four input files get 
converted so that the P present in the original files gets converted to 
ONE CONCRETE form, not four different forms.

I am not too optimistic that the converter writers "will do the
right thing" if they have not been given clear translation
rules before. Without clear rules they might even refrain
from writing the translators in the first place, arguing
that the end results would be incompatible anyway.
Abstract syntax and semantics alone (if it cannot be read
directly as conversion rules) is IMHO not sufficient.

Why I am a bit worried about the "simple" approach of quantifying
always over BOTH I (objects) and R (relations): in case you
want to read in a "traditional FOL" file like Q above, the
quantifiers themselves, not just predicate symbols will
have different original meanings in
t1(AX1),t(AX2),t(AX3),t(Q1). This will be hard to detect
and hard to understand.

Take the example we had before:

(forall x. P(x) & -Q(x)) & (forall x,y. x=y) & R(P) & R(Q).

Suppose that the first two pieces:

(forall x. P(x) & -Q(x)) & (forall x,y. x=y)

come as a translation from a traditional FOL language.

Suppose R(P) & R(Q) comes from a fancier, RDFS-ish language
(could be SCL).

Then, if FOLPROVE operates on the weird principle I
suggested as an example before, that it notices R(P) & R(Q)
and determines that ALL quantifiers now iterate over both
ordinary objects and relations, the formula is not
satisfiable. However, most probably this was NOT what
the authors of the first two pieces - who had perhaps
never heard of SCL or RDFS - intended. They had always
assumed that their part IS satisfiable.

This consideration makes the typed quantifiers to seem
a bit more attractive, in my viewpoint. We could in principle
survive a situation where we have TWO general quantifiers:
one ranging over objects (I), one over relations (R), and
why not even the third, running over I+R. I guess that
the "traditional", I-covering general quantifier will be
used mostly, and the users of that might be even happily
unaware that there are other people, other languages  who
have their quantifiers range over relations as well!

I am not completely sure that this works out as nicely
as I imagine: have to look more into what might happen
with the R-ranging quantifier usage. But I do hope that
there are no lousy complexities.

To finish this letter I'd - again - stress the importance
of some common, basic datatypes. Again, imagine that
the AX1 people use a decimal notation of integers, while
the AX2 people use a successor notation, while Q people
use a binary notation. Then, obviously, the end result of
translating-and-appending, the file F, will contain several
different representations of integers, all incompatible:
2 in AX1 will not be equal to 2 in AX2 will not be equal
to 2 in Q.

Hence it seems that we will need to TELL the converter-writers
that in SCL there is this specific way of encoding integers and
these specific pre-defined predicates and functions. Then
the converter utility program will be able to detect and
properly understand the integers in the SCL file, and if
it so wishes, convert them into a successor notation or
decimal notation or whatever in FOLPROVESYNTAX.

In case the FOLPROVE people did not have a nice syntax
and built-in functions and predicates (built-in for
efficiency reasons) before, they may well opt to
use the SCL conventions and program these into the
FOLPROVE+, a new version of FOLPROVE. After that they
will take care to convert the successor syntax, etc,
- if noticed to be integer syntax (!) - to SCL integer
syntax, not vice versa (since their FOLPROVE uses
the SCL integer syntax). This, if it happens, will
stengthen the position of SCL and will possibly push
towards its use as a defacto standard to be read
in by FOLPROVER++ and similar programs.

Regards,
          Tanel Tammet