[SCL] weekend update

[Chris Menzel]

Hi Tanel, thanks for the detailed and very useful comments/criticisms.  

> 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.

Yes, that is of course true, and that is by design.  The intention all
along that *this* spec not be for public consumption -- not that the
public shouldn't see it, but rather that it is simply not intended to be
the one most people will *want* to see.  The current document has one
and only one purpose: to get the formal foundations right, in
excruciating detail.  Once we agree we've got them right, the idea is
then to use the document to generate a spec for public consumption.  Too
often specs of the latter sort are written without the former sort, with
the consequence that deatils are not nailed down, and it remains unclear
at important points exactly what does and what does not satisfy the
spec.  That said, it is clearly a pressing task to begin work quickly on
a friendlier spec as soon as we are agreed on the contents of the
current document.

> 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.

Ask again.  :-)  There are sections that are admittedly compressed, as
time has been an issue, and I felt it was important to get the thing out
there.

> 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 ...

Well, surely that should be a part of what it provides; and maybe it
should even be its "real point".  But to do it *right*, we need to get
the formal foundations right.

> ... from different FOL-based or FOL-extending languages, with SCL
> itself being seen as a subset of FOL.

Should be a superset, but we can talk about that.  (I'm not even sure
what you have in mind by thinking of it as a subset -- what do you
propose leaving OUT??)
 
> 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.

I am in complete agreement with everything you say here.

> 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.

But, again, they an important place in the formal foundations.  What you
call fancy language are just names for clear definitions.

> 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.

Agreed.

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

Important, but these seem to me to be tasks for separate documents.

> 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.

Again, of course.
 
> 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? 

FOL is not the name of a definite object.  L*1 is an instance of a
first-order language.

> Is L*1 traditional FOL or not? 

It is a first-order language, yes.

> 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.

Well, I'd be happy to see a way to draw the connection with first-order
languages more simply.  If you could point out the unnecessary
complications, I'd be grateful! :-)

> As I understood (maybe incorrectly), L*1 is NOT traditional FOL. 

But it is; it is what I call a TFO (traditional first-order) language,
and it is pure as the driven snow: predicates, function symbols, and
individual constants form separate lexical categories, the arity
function assigns definite arities to all predicates and function
symbols, terms and atomic formulas are formed in the the usual way.

> 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.

Good thing it isn't!

> You write:
> 
> "The idea here, first, is to purge ? 

I use an ascii-based mail client, though I think it is good practics in
general to use an ascii substitute for lambdas and such, e.g., "lambda". :-)

> > 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 lambda, those
> > that are not also individual constants. So let PurePred = PredCon U
> > IndCon."
> 
> But how on earth are we going to do this?

Well, we just do it.  It's a formal definition.  I think the problem
here is that you are viewing the formal procedure here as a practical
methodology.  It isn't.  We'll have to think about how this plays out in
an implementation.

> 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.

Well, again, we are now moving to the issue of implementation, but how
about this:  you assume a predicate is pure unless something in
Otherstuff + Query forces to assume otherwise, e.g., a sentence in which
R occurs as an argument to another predicate.

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

I'm not convinced that is true.

> 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.

The force of "could" here is not clear.  It could be understood to mean
that you want all predicates to be thought of as impure, i.e., you want
a full CL sort of language.

> You write:
> 
> "Suppose also 'f' and 'foo' have also been designated individual
> constants".
> 
> How do you "designate" something as an individual constant?

Once again, designation only has a formal meaning here; we considering a
language in which 'f' and 'foo' are also in the set of individual
constants for a language.  How this plays out in an implementation is
not being addressed -- yet.

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

Well, you'll have to tell me exactly what you think the problem is and
show that it doesn't disappear.

> IMHO the SCL<->FOL translation issue is still left open in the current
> draft. 

At the implementation level, yes.  We have only abstractly expressed the
idea, but it will be important to lay it out with specific languages.

> 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 :-)

I'd be happy to make this our current focus.

Thanks again.  We've got lots to talk about!

-chris