[SCL] A few questions about the new SCL version
pat hayes
phayes at ai.uwf.edu
Tue May 27 11:31:15 CDT 2003
>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.
Oh dear, Thats not good. SCL must be able to support things like
reflexive(?r) iff (forall (?x ?y)(?r(?X ?y) iff ?r(?y ?x))
Seemed to me that your semantic tweak should be able to handle that OK.
In order to be a suitable target language for RDFS, SCL needs to be
able to at least do the following;
1. Allow nonwellfounded applications, like R(R,A) and R(P) & P(R)
2. Allow axioms of the form P(?r) iff (forall (?x ?y)(foo ?r ?x ?y))
Anything that we do that breaks this isn't acceptable. If we can also
keep native GOFOL as unchanged as possible that is obviously good,
but we need to keep at least this much of the CL wild west syntax
intact. I am optimistic that we can do all of this, however. Chris'
latest semantic idea seems to still have some room for exploration.
>
>>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.
Then I misunderstood. I don't think this is acceptable, then.
>
>>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,
Can predicate variables occur in individual position?
>which wouldn't have the right semantics, since they range over
>everything. We would want variables that only range over relations.
This just seems to amount then to a sorted version of SCL in which
relations are a sort and the relation position is restricted to
things of that sort. That is fine with me, I guess, provided that we
can quantify freely. It kinda smells of type theory to me, though. I
would prefer to have SCL be kept relatively pure of such clutter even
at the cost of slightly complicating the GOFOL-SCL translation
mapping.
>
>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.
Whoa: scaling back on that kind of quantificational freedom was never
a design goal of SCL.
> 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.
Not acceptable. Anything that prevents us asserting properties of
predicates isnt acceptable. Use the 'reflexive' example as a test
case.
>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
I do. Fatal limitations, in fact.
Whats wrong with saying that *if* it occurs as an individual in an
expression, *then* it must denote something in I ? Then there is no
syntactic restriction and no 'sorting'. This does have some
consequences that a traditional GOFOLer might find odd, such as that
while
(forall x. P(x) & -Q(x)) & (forall x,y. x=y)
is satisfiable,
(forall x. P(x) & -Q(x)) & (forall x,y. x=y) & R(P, Q)
is not satisfiable. But then a traditional GOFOLer isn't going to
write things like this second one in any case.
The only case that this fails to handle properly is one where a
variable occurs ONLY in relation positions, since in this case the
quantifier could be vacuous. However, I think that we could simply
rule out such expressions, as they cannot be used to say anything
useful in any case; or else treat them as though they were indeed
vacuous quantifiers where the variable doesnt occur in the body. What
this means is that such a variable - one which occurs only in
relation positions and is never predicated on - is essentially
unbindable by a quantifier. In that respect it is rather similar to a
sequence variable and maybe can be treated the same way, ie
essentially as a schematic symbol rather than a true variable.
>, 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?
Unfortunately, yes.
>
>>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.
I agree with Tamel here. I would prefer to have the sorting (because
that is what we are talking about) done implicitly by the syntax,
rather than explicitly. The trouble with being explicit is that one
has to say what it means when the explicit 'declaration' is missing,
and then we are back where we started; or else make it syntactically
illegal to omit it, and then we have 'structured' ontologies with
compulsory prefixes and so on. I would rather not even go there. The
'header information' is the thin end of that wedge.
>
>>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.
I like the approach outlined in the above example.
Pat
--
---------------------------------------------------------------------
IHMC (850)434 8903 or (650)494 3973 home
40 South Alcaniz St. (850)202 4416 office
Pensacola (850)202 4440 fax
FL 32501 (850)291 0667 cell
phayes at ai.uwf.edu http://www.coginst.uwf.edu/~phayes
s.pam at ai.uwf.edu for spam
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://philebus.tamu.edu/pipermail/scl/attachments/20030527/b03182a2/attachment.htm
More information about the Scl
mailing list