[SCL] Re: [KIF] (SCL) Seqvars revisited

[Adam Pease]

Folks,
   Apologies for a somewhat repeated comment, but I think it's relevant.  I 
haven't followed all of this, but we're using a version of sequence vars 
daily in a first order theorem prover.  We simply treat them as macros 
which expand to a fixed number of variables.  I think that gets you all the 
practical utility without the theoretical problems.


(=>
    (and
       (subrelation ?REL1 ?REL2)
       (holds ?REL1 @ROW))
    (holds ?REL2 @ROW))

would become

(=>
    (and
       (subrelation ?REL1 ?REL2)
       (holds ?REL1 ?ARG1))
    (holds ?REL2 ?ARG1))

(=>
    (and
       (subrelation ?REL1 ?REL2)
       (holds ?REL1 ?ARG1 ?ARG2))
    (holds ?REL2 ?ARG1 ?ARG2))

etc.

Adam


At 10:05 AM 12/18/2002 -0600, pat hayes wrote:
>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
>
>_______________________________________________
>KIF mailing list
>KIF at philebus.tamu.edu
>http://philebus.tamu.edu/mailman/listinfo/kif