[SCL] A few questions about the new SCL version

[Christopher Menzel]

On Monday, May 26, 2003, at 03:16  AM, Tanel Tammet wrote:

> ...
> Great! Looked through the new version, and it seems to be significantly
> clearer and - for several parts - easier to understand. The new feature
> that the traditional FOL is an OK SCL language - semantics preserved -
> is extremely nice, IMHO.

I agree!

> However, in the light of the goals of SCL, the previous versions of SCL
> and all the discussions, I am unsure whether I understand some 
> important
> parts of
> the paper correctly though. So I'll simply ask for clarifications for
> two questions in the rest of this email, without trying to say
> what would be IMHO good or bad.
>
> The first question: variables at the predicate position allowed
> or not?

In full CL, yes; not in SCL.

> You write in the paper:
>
> "For this we simply require that there be a one-to-one function
> Pred on (PredCon × Trm*) ∪ (Con × Trm* × SeqVar); that is,
> given a constant, n terms, and ― optionally ― a sequence variable,
> Pred returns a unique formula."
>
> Does this mean that a formula like
> forall x,y. x(y)
> where a quantified variable x is used in the predicate position
> is not legal in SCL, or have I misunderstood the paper?

You have not misunderstood.

> It seems to me that unless one can use a quantified variable in the
> predicate position, there is no point in allowing I and R
> domains to overlap: cannot use the statements like "Commutative(P)"
> for anything useful unless we can axiomatise
> forall x,y,z. (Commutative(z) => (z(x,y) <=> z(y,x))).

Well, I disagree that there is no reason to allow overlap.  It is very 
useful to be able to ascribe properties to particular relations in 
one's ontology.  That said, I think I agree with you.  Being able to 
quantify directly over relations is very useful, and it would be 
trivial to add this functionality to SCL without altering its 
fundamental formal properties; notably, SCL languages with such 
"higher-order" quantifiers and no seq variables would still be 
semantically fully first-order.  We'd have to implement things a bit 
differently than you suggest, though.  Since we have a class of 
predicates, we would simply add predicate variables rather than allow 
individual variables to occur in predicate position, which wouldn't 
have the right semantics, since they range over everything.  We would 
want variables that only range over relations.

One of the design goals of SCL was to scale back on some of the more 
foreign features of full CL, and quantification into predicate position 
was among those.  But it is not really quantification into predicate 
position that is foreign in CL, but the fact that there is only one 
type of variable for quantifying into any position.  Given that we have 
reinstated the distinction between predicate constants and individual 
constants, it is a pretty easy conceptual step to introduce predicate 
variables.

Here's the proposal then:

1. Introduce predicate variables.  The range of such variables is the 
set R of relations.

2. Predicate variables can *only* occur in predicate position.  The 
reason for this is that not all relations need be considered 
individuals; in fact, in some interpretations, none of them are.  I 
don't think this will lead to expressive limitations, but I feel 
vaguely uneasy about this, a sense that we haven't quite yet hit on 
exactly the right middle ground between FOL and full CL.

> The second question: different SCL languages in practice.
>
> How does one in practice say whether we use a traditional FOL semantics
> or free semantics. Ie, if we take the same example
>
> (***)  (forall x. P(x) & -Q(x)) & (forall x,y. x=y)
>
> and now want to interpret it in the nonstandard way that P and Q
> are in the set I of ordinary objects, quantified over (as it seems
> to be the natural way for RDF).

This is a good question that I'm not sure I'm qualified to answer.  
Presumably there is header information of some ilk that identifies the 
signature of a language?  Is that too much to expect?

> We should then say that the predicate
> domain R is a subset of the domain I of individual constants. But
> how exactly do we say that in some particular concrete syntax?
>
> Perhaps the seqvars have to be used to get the App/Pred
> semantics?
>
> If we could get the nontraditional semantics without seqvars,
> then the question remains:
>
> It seems that we could define different concrete languages with
> concrete syntaxes on top of SCL. One language, say, "traditional"
> would have a traditional semantics, while another language,
> say, "RDFSplus" would have the I=R semantics.

Remember I=R is just a special case.  That aside, this seems plausible 
to me (but again I'm not the guy to ask).

> Did you have something like this in mind?

Now I do! ;-)

> Alternatively, one could imagine that we assume that
> an implementation looks at the actual formulas it gets.
> It can easily detect whether some lexical entity is
> used both in a predicate position and as argument
> to some predicate/function, or a quantified variable
> is used in the predicate/function position.

Yes, but a lexical entity might be intended to be *usable* in argument 
position without actually being used in the given piece of whatever 
ontology we are looking at.  A more reliable mechanism seems to be 
needed.

> If it notices this nonstandard use of the lexicon, it
> will use either I=R (or a partial overlap between I and R),
> otherwise it will assume that I is distinct from R.

Hm, maybe that will be good enough in practice.  But I'm uneasy.

> Let me bring some examples to make my question
> about the implementation-detected semantics option clearer:
>
> Given
> (***)  (forall x. P(x) & -Q(x)) & (forall x,y. x=y)
> the implementation would determine that traditional semantics
> is used and (***) is satisfiable.
>
> Given
> (****)  R(P) & R(Q) & (forall x. P(x) & -Q(x)) & (forall x,y. x=y)
> it will detect that nontraditional semantics is used
> and (****) is NOT satisfiable.
>
> Again, which approach did you have in mind?

The best one! :-)  This is an issue for group discussion/decision.

-chris