[SCL] (SCL) Seqvars revisited

[pat hayes]

I'm more and more coming to think that KIF bit off more than anyone 
could chew, and a lot more than Mike Genesereth thought he was biting 
off, when it just threw seqvars into the syntax. You say you need 
them, Bill, but they were always slated for demolition in CL, if you 
recall, on the grounds that nobody really knew what they meant. Mike 
G insisted that without them you couldn't possibly quantify over 
variadic relations, which seemed right, and then Chris and I figured 
out that you could see them as abbreviations for infinitary 
expressions, and since then we theoreticians have been happy as pigs 
in s**t but the implementers have been depressed and wishing they had 
never come to the party.

I think that we can get the benefits without the unworkable bad side 
of them if we take a little more trouble and treat them explicitly as 
sequences with a fixedpoint semantics a la LISP, which is after all 
what the old KIF obviously had in mind, since it used LISP *as* its 
syntax. This is what the implementers are asking for, and its what 
the RDF/OWL axis has done (in a horribly ugly way, but leave that 
aside for now.) I seem to see a convergence here between the demands 
of theory and those of practice, which is very encouraging.

What everyone wants, I think, is the freedom to have variadic 
relations and to quantify into them in neat ways and so on, PLUS the 
ability to use recursion and to assume that intuitively recursive 
constructions do in fact define what any sane LISP hacker would take 
them to be defining. Right now, neither KIF nor CL actually has that 
latter property, in fact - it requires a kind of induction principle 
in CL which goes beyond the FO MT and needs a genuinely infinitary 
axiom to state in the language - but if we were to look these things 
in the face honestly, then I think we could get that in a clean way 
which would also provide a clean semantics and a better metatheory 
with a closer link between MT and proof theory. And we can always 
leave CL infinitary-ivory-tower clean and have SCL be a worldly 
recursive special case of it, if y'all prefer.

Heres a sketch. A relational atom is treated in CL basically as a 
predication on tuples, right now, if you check the semantics, and 
seqvars are actually a kind of schema for talking about tuples of 
arbitrary length by implicitly quantifying over all finite tuples at 
once. The key point here is that 'finite' which we kind of cheat 
with, since we say its finite since its all in the syntax; but the 
seqvars are using this to define a range of a *quantifier*. Hence all 
the non-FO complexity. OK, so lets stop cheating and get explicit 
about where that 'finite' comes from, which is a recursion on the 
length of the tuples: you can add another widget to a finite tuple 
and it stays finite, and we take the standard fixedpoint of the 
obvious recursion. We don't even use the concept of 'finite' in the 
metatheory anywhere. Tuples are then something awfully like LISP 
lists (cf. KIF) and RDF collections (cf. OWL).

OK, now go back to relational atoms.  Lets be up-front about what the 
MT is saying: we have tuples now as explicit things, and a relation 
is just a set of tuples, and relational atom syntax says this: its a 
*unary* predication applied to a *single* argument which is a 
sequence, or list if you prefer. Seqvars quantify over the lists, 
normal vars are used to quantify over the things in the lists. They 
are both perfectly normal quantifiers now, but they contribute to the 
truthconditions of the relational atom in different ways. The seqvar 
domain is defined recursively and is indeed not FO, but the normal 
vars quantify over FO domains in the usual way. Key point: those 
lists are NOT definable in any finite ontology, so any SCL *theory* 
of lists isn't going to be able to eliminate them (you can describe 
them in SCL but only by using them in the description in some way.)

Here's a way to put this into an 'honest' syntax. A relational atom 
consists of two things: a term denoting the relation and a list of 
terms indicating the arguments. Lists are indicated by writing their 
elements inside parentheses. You can quantify over the lists :

R ?y

or over the things in the lists:

R(?y)

The first corresponds to CL syntax (R @y), the second to (R ?y). 
Obviously the first only makes sense if ?y is instantiated by a list, 
so you can think of it as a sorted quantifier if you like, but its 
still just a quantifier.

To write something corresponding to, say, (R ?y @z ?x) in CL, you 
need to get explicit about the list structures, and we can introduce 
an implicit concatenation-by-adjacency into the syntax, so that this 
might look like

R(?y) ?z (?x)

in this 'honest' version. The tail-sequence case is where you only 
allow a single list variable in the tail position, obviously, so the 
difference only amounts to
(R ..... @x)
R(..... ) ?x

But I don't mean to suggest this syntax seriously, its only to 
illustrate the point.

All this is close to being a re-stating of the current CL MT, in 
fact, and it could be applied directly to CL as it stands; but in 
addition it makes sense of the KIF idea that syntax is LISP-like (and 
of the KIF way of slipping the seqvars in by the back door, with an 
implicit tail-recusion which doesnt get mentioned anywhere) and of 
the RDF/OWL idea that N-ary things are unary (well, binary in RDF, 
but never mind) things applied to lists of arguments; and instead of 
forcing the metatheory into infinitary languages, it forces us only 
into FO + recursion, which I think is where we should always have 
been in any case.

Comments??

Pat

PS, BTW it occurs to me that the above syntax allows things like this:
R(?x) ?x
which at first I thought was crazy but in fact makes perfect sense: 
it says that the first argument of R is the list of the remaining 
arguments, and it does this magically without using recursion :-).
-- 
---------------------------------------------------------------------
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