[SCL] Re: (SCL): Seqvars revisited
pat hayes
phayes at ai.uwf.edu
Thu Dec 19 22:53:12 CST 2002
>On Wed, Dec 18, 2002 at 10:05:50AM -0600, Pat Hayes wrote:
>> I think that we can get the benefits [of seqvars] 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.
>
>I'd hate to see them go cuz the semantics is so damn cool *sniff* but I
>suspect you are right.
Hey, remember this is SCL, not CL.
>And actually, I think some of the nice features
>of the semantics can be retained (see below).
>
>As for your model theory: Unfortunately, I am in the throes of grading
>graduate student papers and cannot comment at length or with the clarity
>I would otherwise want. But let me just throw a couple of things out
>there. First, I wasn't quite clear on your discussion about recursion
>and finitude. Aren't you simply saying that the domain of an
>interpretation for the language is just the union of a set A of
>individuals and the set A* of all finite sequences over A?
Yes, but there really is a problem with that 'finite' , which isn't
first-order defineable, and since we are getting kind of deliberately
sloppy about the syntax/semantics boundary here, I think we have to
approach the metatheory with slightly more formalist glasses on, so
to speak.
> That is,
>aren't we just making the range of the seqvars from the original SKIF
>(simple KIF) model theory first class citizens and welcoming them into
>the domain of the quantifiers?
I think it will come out that way, but if we take it more carefully
we will be less confused about where exactly we are standing. And
maybe more important, I think that a similar route can be used to
introduce other useful domains apart from the sequences....so there
might be more goodies in the jar.
> Your discussion seems more complicated
>than is necessary.
Well, maybe. If it turns out to be needlessly complex, after all,
then we can scrap it.
>
>Second, the syntactic problem that arises -- and which you wrestle
>valiantly with -- when you put sequences in the domain is how to manage
>the potential syntactic ambiguities that arise when you have seqvars --
>do you want to be talking about the sequences or their elements?
Proposal: the variables range OVER *syntactic* sequences. The atomic
assertions USE the sequences. In this view of the machinery, these
are essentially substitutional quantifiers. This means that if you
instantiate with a sequence containing a variable, then that variable
is *free* , not quantified. So you only get 'schemas' by using these
- let me call them - list variables. The quantifiers basically say
'for all schemas...' and 'for some schema....', but I don't expect
the latter to be of much utility.
Our current use of the universal seq. quantifier now looks like a
two-stage quantification: it is the normal-universal *closure* of the
substitution-universal-list quantification of a list variable. Ie it
says, for all expressions got by substituting a (recursively defined)
sequence of terms for ?x, the result of universally quantifying that
expression is true. No wonder its a bitch for a proof theory, right?
But look, we shouldnt try to get this done by email, its late and
tomorrow I have to go Xmas-travelling. I promise I will get these
ideas written up and web-accessible by the first week in January, in
several versions if they come out that way.
> I have
>not been able to consider your proposal in detail, but let me just
>mention an approach I worked out a while back that appears to be an
>alternative to yours. The idea is simply to use exactly the current CL
>semantics for sequence variables (modulo pushing sequences directly into
>the domain), so that a seqvar @x is always used to predicate things of
>the *elements* in the value of @x. To talk about sequences explicitly
>the idea is simply to add a sequence-forming operator "seq" (or, more
>conveniently, perhaps, simple brackets "[...]"). Thus, in particular,
>(seq a b) (or [a b]) forms a term for the sequence <a,b> (seq @x) (or
>[@x]) yields a term explicitly denoting the sequence that @x takes as a
>value.
>
>Back in the days when the SUO list had a reasonable signal to noise
>ratio, I worked out a theory of sequences along these lines. I include
>it below for what it's worth (perhaps only general disapprobation, but
>even showing what's wrong with the approach is useful). Three things
>about it. It is stronger than the theory of sequences you are
>suggesting (I think, from the quick read) as it allows nested sequences.
That is a mixed blessing, though. We need to look at this carefully.
If sequence quantifiers distinguished subsequences from sequence
elements they wouldnt work properly.
>Second, because it is convenient to talk about the length of sequences,
>it comes with a a simply theory of the integers, so I include that as
>well. Finally, There is also a simple theory of classes and relations
>in the background, but I'll leave that out.
>
>-chris
>
>ps: An SCL list has been set up and should be operational later today.
>
>--
>
> /\ ASCII ribbon | Chris Menzel -- http://philebus.tamu.edu/~cmenzel
> \/ campaign | Philosophy Dept, Texas A&M University
> /\ against | College Station, TX 77843-4237
>/ \ HTML email | voice: 979.845-5660 fax: 979.845.0458
(Purely procedural point, but I think we ought to operate as far as
possible by putting things like this on a website somewhere and
emailing the uri, rather than by email inclusions, or else the emails
are going to explode.)
>*****
>
>
>;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
>;; SEQUENCES ;;
>;; (Requires Integers) ;;
>;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
<snip>
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
More information about the Scl
mailing list