[SCL] weekend update

[Tanel Tammet]

Hi Chris,

Chris Menzel wrote:
> Sorry to have been out of the loop the last week, I've had to put in
> some heavy hours on a project that actually pays real money.  I have
> several papers to review, a Master's thesis and a PhD dissertation to
> read by Friday, so the rest of the week is pretty well spoken for, but I
> should be back to incorporate Pat's suggestions over the weekend.

When you posted your last spec I went through it and then spent
some time meditating about how I feel about it. I do not know if
this is of any help, but I'll summarize my feelings here.

Please do not read these notes as a criticism: I am really
writing about motivations and goals, and these are IMHO
not subject to criticism. There is nothing I'd complain about
in the SCL draft as an object in its own rights: you have done a lot
of really good work.

The main problem for me is that what I'd want to get from the SCL
seems to be somewhat different from what you have been
concentrating on.

1. Simplicity: introduction with semantics based on FOL

An easy-to-understand spec. The current spec is fine as
a special chapter for fans of semantics, but not as a spec
of SCL for the public aimed at using it in real programs.

Hackers are highly impatient. Anything which cannot be
understood in half an hour is not OK as a spec.
The main body of the spec should be MUCH easier and
less fancy than it is right now.

Frankly, after reading the SCL spec several times I am
still unsure that I understand it correctly. I remember
that the same has happened to both me and Pat before, reading
earlier versions of the spec: not understanding something
correctly, finding it out only after asking Chris.

I have a feeling that the SCL draft has reached a point
in complexity (despite the intuitive simplicity of the
task we have had) that it hinders progress even in the small
SCL group. People are not commenting much any more.

As for semantics, I can assure you that the people we are
targeting all have good understanding of FOL, and very
different views on everything else. Hence I see the real
point of SCL ideally being a set of normative syntactic
mappings from different FOL-based or FOL-extending languages,
with SCL itself being seen as a subset of FOL.


2. Trivial-to-read, NORMATIVE, SCL<->FOL mappings

The current discussion in the spec about SCL and FOL relations
is very hard to understand. It is what is says to be - a discussion.

We need a straightforward NORMATIVE syntactic mapping
from SCL to FOL and vice versa.

Not discussion in its place. No fancy language.
Obviously, phrases like  "indirectly SCL conformant",
"total recursive function", "TFO-agreeable relative to arity"
"a logical individual",  "Tarski correlate" etc have no
place in this normative syntactic mapping chapter.


3. Integers and annotations in the language.

We have talked about that a lot and presented several
ways to do this. We really need to put them into the
language.

4. Normative concrete syntaxes.

Some concrete syntaxes with their own name and position,
intended to be used exactly as presented. Not "just examples".

5. RDF(S)<-> SCL mappings

Obviously we need to put these in if  we want the
Semantic Web people to have any interest in the whole
enterprise.


Finally, I have a few questions about the parts in
the "Traditional first order languages" which I did
not understand.

You write:

"Let L*1 be the TFO sublanguage of L* based on arity"
and proceed giving a translation scheme from
L to L*1.

Why do you translate into L*1 as opposed to traditional
FOL? Is L*1 traditional FOL or not? If not, then we
do not have a translation to traditional FOL. If yes,
then the usage of L*1 seems to complicate matters
unnecessarily.

As I understood (maybe incorrectly), L*1 is NOT
traditional FOL. Ie, we do not have a translation
from SCL->traditional FOL here at all, but rather
a translation from a specific sublanguage of
SCL to another specific sublanguage of SCL.
This should not be the real goal of the chapter.

You write:

"The idea here, first, is to purge ? of its type-free elements, viz., 
those predicate constants and function symbols that double as individual 
constants. To accomplish this, we first separate off the "pure" 
predicates of ?, those that are not also individual constants. So let 
PurePred = PredCon – IndCon."

But how on earth are we going to do this?

For example, suppose we have a typical axiom

Raxiom: forall x,y,z. R(z) -> (z(x,y) <-> z(y,x)).

If we then want to prove (Raxiom & Otherstuff) -> Query
where "Otherstuff" is a large amount of very different
formulas, then EVERY PREDICATE (at least with arity 2)
is potentially "not pure", ie you cannot algorithmically
decide whether a predicate is pure or not.

Sure, sometimes you can decide such things, but in the
general case you cannot.

Also, the idea of splitting predicate symbols in such
a manner (while STILL wanting them to interact with
Raxiom above) does not work once we think about storing
partial formulas and working with these. The property
of being a "pure" predicate should never change!
As far I understand the situation, we do not want
to have any such predicates which could NEVER be
impure.

You write:

"Suppose also 'f' and 'foo' have also been designated individual constants".

How do you "designate" something as an individual constant?

And, what about the Horrock formulas? I did not see how that
problem disappears in the current spec.

IMHO the SCL<->FOL translation issue is still left open in
the current draft. Since the very same issue is in my understanding
absolutely critical for the wider usability of SCL, I'd propose
dropping all the other SCL developments until the
commonly agreeable mapping is worked out :-)


Regards,
          Tanel Tammet