[SCL] Re: (SCL) Getting a move on

[pat hayes]

>On Wed, Dec 18, 2002 at 10:05:30AM -0600, Pat Hayes wrote:
>>  Lets argue about sequence vars. I bet your company doesnt need full
>>  CL seqvars, equivalent to an infinitary logic, right? Do you ever
>>  need to write something like
>>
>>  (forall (?x) (exists (@y)....))
>>
>>  What do you do with it when you've written it??
>
>Pat,
>
>Granted, the full semantics and proof theory of CL seqvars is
>infinitary, but one may not need all of that power and still find a need
>for seqvars just in virtue of using a variably polyadic predicate.

I agree, but I think we should try to capture this useful kind of use 
more accurately. Just saying to everyone who wants to do this that 
they have to use seqvars, is like using the waste heat from a nuclear 
power plant to warm your living room. (Analogy invented by Peter 
Patel-Schneider)

We have to think about implementors as well as writers of axioms. If 
the spec requires full seqvars, then a conforming implementation has 
to be able handle *all* seqvar constructions, which is probably never 
going to happen. Just tossing seqvars into the language says, in 
effect, you have the full power or nothing. We need to define more 
useful compromises.

I now think that the observations about infinitaryness really should 
be taken seriously as showing that seqvars *in their present form* 
aren't a useful construct to have in a deployed language. This is 
supposed to be a formalism for actual use on machines, and if it 
comes with a completeness result that says theoremhood is not even 
semidecideable, then we just look silly. (Bill wants them, but he 
also wants the entire logic to have a well-founded semantics, which 
entirely changes the semantic rules so its not even first-order any 
longer. We can take a look at that, but its not going to be widely 
acceptable and makes the whole system even less like FOL.)

>   Your
>question seems to run roughshod over that possibility.

I want to get that possibility made precise and made the central 
aspect of the language, not an afterthought. The result will not be 
seqvars as we now have them, though it might be closer to what they 
were in original KIF.  (However, we might be able to retain the 
current seqvar *syntax*, if that is felt desireable.)

>  For example,
>suppose you are using a variably polyadic "eats" predicate, and you have
>a constraint that there is always someone eating but you don't
>necessarily have or care about the information about what is eaten when,
>where, etc.  Thus, in your database at any given time, you might have
>any of the following:
>
>(eats pat)
>(eats bill eggs)
>(eats chris tofu noon)
>
>but all you need to verify is that someone eats.  (exists (?x) (eats ?x)
>won't do the job except in the first case.  (exists (@x) (eats @x))
>expresses what we want in all cases.

There is something very odd about that example, since it has the 
consequence that one says the same thing to express 'someone is 
eating', 'something is being eaten', 'an eating is happening at some 
time' and so on. Yet it seems that these ought to be conceptually 
distinct; for example, one can ask when an event is happening without 
knowing anything about the kinds of things that are involved in 
events of that type. It assumes that *events* are going to be 
described as variadic relations; but that seems to me to be only one 
possible option for event descriptions, and indeed not a very 
sophisticated or useful one, since it requires everyone to know where 
in the argument-sequence the various attributes are located, vital 
information which is not made explicit in this way of describing 
things. I wouldn't lose any sleep if SCL were unable to support this 
style of representation for event descriptions.

I think we should take a hard look at what variadic relations are 
supposed to actually be used *for*. The KIF uses are all about 
incorporating LISP into the syntax.  Adam is quite happy to just 
treat them as abbreviations for lists of similar patterns of FO 
axioms; and for examples like yours, he is probably right (how many 
attributes of an action typically get described? Five, maybe?) In 
many parts of the intellectual world they are forthrightly declared 
to be properties on lists rather than variadic relations, and the 
more I think about it that more that makes sense, on just about every 
dimension. It even makes the CL MT come out more precisely and 
cleanly, since it separates three issues that we have munged together 
right now:

1. quantifying over sequences
2. sequences as syntax (recursion not description, sneaks finiteness 
in by the back door and wrecks FO compactness, hence the Lw1w stuff)
3. quantifying over individuals by using sequences

We do 2 and 3 mixed together, in effect; what we ought to be doing, I 
think, is 1 and 2, but being honest about the recursion in 2. That 
way, we get the connection to the list-style approaches 
automatically; we get a genuinely FO language which is kind of wedded 
to a recursive language, which gives us a clean connection to other 
uses which mix recursion and assertion, like well-founded semantics 
in LP and XML datatype domains.

I'll expand on this stuff later and CC the CL mailing list. Maybe we 
could talk about this at Santa Fe? I will need to fly there, but it 
seems worth doing.

>  > We havn't begun to think seriously about the meta-extension.
>
>I have. :-)

I have, too, but *we* havn't, as a group. I speak now of course as a 
member of the CL group, not SCL. SCL really does not have time to get 
involved with the meta-stuff, and I don't see any use cases or demand 
for it from anywhere.

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