[SCL] translating RDF, RDFS and OWL into SCL

[Pat Hayes]

>On Nov 8, 2004, at 4:57 PM, Pat Hayes wrote:
>
>>>On Nov 8, 2004, at 4:07 PM, Pat Hayes wrote:
>>>
>>>>>Hi, Pat...
>>>>>
>>>>>Didn't know you were working on this.  And, since we just built 
>>>>>a translator to take OWL into our KFL (an SCL concrete syntax) 
>>>>>I'm anxious to give it a read.  By when do you want comments?
>>>>
>>>>Im debugging the axioms right now, will update and signal you 
>>>>later today. Can your engine handle the SCL tail recursions (=~= 
>>>>KIF sequence variables, or RDF lists) ?
>>>
>>>Yup, at least I think so.  We do use sequence variables in the 
>>>current engine but it's not up to the SCL spec you wrote.  We did 
>>>it 4 years ago.
>>
>>Then its probably up to it. SCL is a step backwards from KIF, since 
>>we don't allow explicit quantifier binding to the seqvars: in 
>>effect, they are always universal at the top syntactic level.
>
>That's what we have.  No existential quant over seqvars.  I have to 
>check what the syntax rules are we have.  All of the axioms that use 
>seqvars are part of our top-level ontology and don't get revisited 
>very often so I've forgotten how that works.
>
>>BTW, I now think that this entire detour into seqvars was kind of 
>>beside the point, in spite of their elegance. Lists are just more 
>>convenient, truth be told. In particular, since they are real 
>>entities, not just syntactic tricks, you can quantify over them 
>>directly; and the obvious list axioms mean that a list of n items 
>>exists just when the items do; so in effect you get 
>>sequence-variable quantification for free whether you want it or 
>>not. Ah well, one is always learning,
>
>From a purely mathematical standpoint you're right.  But when I 
>write something like:
>
>     (forall (F G) (=> (subsumes G F) (forall (...x) (=> (F ...x) (G ...x)))))
>
>I really do mean to say something only about the substitutions for F 
>and G and ...x.  The fact that the length of the substitutions for 
>...x can vary depending on the choice of F and G doesn't alter the 
>fact that I want to say something *ontologically* about relations 
>and their relata, not about lists.

Right, I understand, and that was always the intuition that drove the 
CL/SCL model theory. BUt what Im coming to see (amazing how slow the 
mind is to work) is that there really isn't any essential difference 
between lists and sequences (= tuples); and the very idea of a 
relation involves sequences. So right now in SCL we have a special 
syntax for sequences but not for lists, but it is trivial to 
axiomatize lists in terms of sequences; and then explicitly 
quantifying over those lists (using normal quantification, now) gives 
us MORE expressive power than we had from the fancy syntax directly, 
because now we can quantify over them in general position. So the 
only real function of the sequence quantifier is to slip lists in 
under the syntactic hood, so to speak. And since (it seems to me :-) 
no reasonable person could object to the logical universe containing 
finite lists, we might have well have just used them in the first 
place.

On this view, the ONLY real requirement for the seqvar construction 
is to allow the statement of the axiom:

(forall (r) (iff (r (list ...)) (r ...) ))

which amounts to a syntactic convention for 'hiding' the explicit 
list constructor, analogous to our convention (as one might think of 
it as being) for 'hiding' the explicit holds/app relation/function 
constructions. And in fact, this analogy works even better than it 
seems, since the contentious issue in both cases is that this 
'hiding' lets things into the logical universe that some people feel 
shouldnt be there (relations, functions and now lists) and the 
solution should, I now think, be the same in all cases: allow the 
language to be explicit about whether things are in the universe or 
not. If you don't want lists/sequences in your universe, you 
shouldn't need to have them there, but you should still be able to 
USE them as a syntactic device. Right now, the seqvars don't denote 
things in the universe but the lists do. BUt they appear very 
differently in the syntax. Maybe we could do this better. Hmmmm.

Consider vanilla FOL syntax of an atom:

R(a b c)

The conventional view of this is that a, b and c are in the universe 
but R isn't, and neither is the sequence <a b c>. SCL currently 
allows you put R in the universe or not, by a syntactic switch:
R(a b c)
vs.
(R a b c)
but it doesn't offer a similar trick for deciding whether or not the 
argument sequence  (= list = tuple) <a b c> is in the universe. Maybe 
it should, is my point. Not sure how to do it neatly, though. Seems 
hard to beat the distinction
(R a b c)
vs.
(R (list a b c))

>If anything, I wouldn't mind if the ...x were just a shorthand for 
>lists underneath the surface syntax or in the semantics, but for 
>clarity's sake, I like ...x better.

OK, we can leave that there as surface syntax, I agree its neat. But 
wouldnt it be nice if we could write lists that easily as well. After 
all, the tail of a list is a list, and what is ...x in "(R ...x)" 
other than the tail of the list encoding the atom?

Hmmm, am I just re-inventing KIF all over again? Horrible thought :-)

More later.

Pat

PS. Chris M., are you reading this stuff?


-- 
---------------------------------------------------------------------
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 ihmc.us       http://www.ihmc.us/users/phayes