[SCL] (SCL): Seqvars revisited
Chris Menzel
cmenzel at tamu.edu
Thu Dec 19 06:41:13 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. 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? 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? Your discussion seems more complicated
than is necessary.
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? 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.
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
*****
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; SEQUENCES ;;
;; (Requires Integers) ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(documentation "AXIOM: Sequence is a class.")
(Class Sequence)
(documentation Sequence "A sequence is an ordered n-tuple of objects,
for some non-negative integer n. Formally, a sequence is understood
to be a 2-place functional relation that that holds between each
positive integer [and only the positive integers] less than some
positive integer and a unique object in the domain. Intuitively,
then, `(S N X)' indicates that X is the Nth element of the sequence S.
Any objects in the universe of discourse -- including other sequences
-- may be elements of a sequence. Thus, we say that X is an element
of the sequence S -- (element-of X S) -- just in case (S N X) holds,
for some positive integer N. [This is captured formally in the next
axiom.] Note that we do not use a biconditional here, as we want
sequences, qua sequences, to be extensional, but we also want them to
be functions, and hence a type of relation. But we do not wish to
build the extensionality of relations into our logical foundations,
and so we have to treat sequences as a special *type* of relation
where extensionality holds.")
(=>
(Sequence ?s)
(and
(BinaryRelation ?s)
(Functional ?s)
(subclass-of (DomainFn ?s) PositiveInteger)
(exists (?n)
(and
(PositiveInteger ?n)
(not
(element-of ?n ?s))
(forall (?m)
(=>
(and
(PositiveInteger ?m)
(< ?m ?n))
(element-of ?m ?s)))))))
(documentation element-of "DEFINITION: The element-of relation holds
between an object in a sequence and the seqence. It is the analog of
the membership relation for sets.")
(<=>
(element-of ?x ?seq)
(and
(Sequence ?seq)
(exists (?n)
(?seq ?n ?x))))
(documentation "AXIOM: Sequences are extensional, i.e., sequences with
the same elements in the same order are identical.")
(=>
(and
(Sequence ?seq1)
(Sequence ?seq2))
(=>
(forall (?n ?x)
(<=>
(?seq1 ?n ?x)
(?seq2 ?n ?x)))
(= ?seq1 ?seq2)))
(documentation "AXIOM: There is a null sequence.")
(exists (?seq)
(and
(Sequence ?seq)
(not
(exists (?n ?x)
(?seq ?n ?x)))))
(documentation nil "DEFINITION: nil is the null sequence. The
uniqueness of the null sequence follows from the extensionality of
sequences.")
(and
(Sequence nil)
(not
(exists (?n ?x)
(nil ?n ?x))))
(documentation length "DEFINITION: The length of a sequence SEQ is the
largest nonnegative integer n such that SEQ is `defined' on every
positive integer less or equal to n, that is, the largest nonnegative
integer n such that, for every positive m =< n, there is an object X
such that (SEQ m X).")
(<=>
(length ?seq ?n)
(and
(Sequence ?seq)
(NonNegativeInteger ?n)
(forall (?m)
(=>
(and
(PositiveInteger ?m)
(=< ?m ?n))
(and
(exists (?x)
(?seq ?m ?x))
(not
(exists (?y)
(?seq (+1 ?n) ?y))))))))
(documentation "AXIOM: length is functional.")
(Functional length)
(documentation "THEOREM: The length of nil is 0. This follows chiefly
from the fact that nil is defined [vacuously] on every positive
integer less than 1.")
(= (length nil) 0)
(documentation initseg "DEFINITION: One sequence S1 is an initial
segment of another S2 if they agree on every number on which S1 is
defined.")
(<=>
(initseg ?s1 ?s2)
(and
(Sequence ?s1)
(Sequence ?s2)
(=< (length ?s1) (length ?s2))
(forall (?i)
(=>
(and
(PositiveInteger ?i)
(=< ?i (length ?s1)))
(= (?s1 ?i) (?s2 ?i))))))
(documentation "AXIOM: Any sequence can be extended by any object.")
(=>
(and
(Sequence ?s1)
(= (length ?s1) ?n))
(exists (?s2)
(and
(Sequence ?s2)
(initseg ?s1 ?s2)
(= (length ?s2) (+1 ?n))
(= (?s2 (+1 ?n)) ?x))))
(documentation max "DEFINITION: The max of a non-null sequence of
integers is the largest integer in the sequence. [That the elements
of the argument to max must be a sequence of integers is ensured by
the axiom for >=, which can only hold between integers.]")
(<=>
(= ?n (max ?seq))
(and
(element-of ?n ?seq)
(forall (?m)
(=>
(element-of ?m ?seq)
(>= ?n ?m)))))
(documentation one-one "DEFINITION: A sequence SEQ is one-one if the
same object does not occur twice as an element, i.e., if there are no
distinct numbers m and n such that, for some object X, we have both
(SEQ m X) and (SEQ n X).")
(<=> (one-one ?seq)
(not
(exists (?m ?n)
(and
(/= ?m ?n)
(= (?seq ?m) (?seq ?n))))))
(documentation cc "DEFINITION: The concatenation of two sequences S1
and S2, `(cc S1 S2)', is the unique sequence SEQ consisting of the
elements of S1 followed by the elements of S2. More formally, (SEQ m)
is (S1 m), for positive integers less than or equal to the length i of
S1, and (SEQ (+ i n)) is (S1 n) for positive integers n less than or
equal to the length of S2.")
(<=>
(= ?s1s2 (cc ?s1 ?s2))
(and
(Sequence ?s1)
(Sequence ?s2)
(Sequence ?s1s2)
(= (length ?s1s2) (+ (length ?s1) (length ?s2)))
(forall (?m ?n)
(=>
(and
(PositiveInteger ?m)
(PositiveInteger ?n)
(=< ?m (length ?s1))
(=< ?n (length ?s2)))
(and
(= (?s1s2 ?m) (?s1 ?m))
(= (?s1s2 (+ (length ?s1) ?n)) (?s2 ?n)))))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; THE SEQ FUNCTION ;;
;; (Row variables essential) ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(documentation "REMARK: The seq function enables us to form names of
sequences by listing their elements. Thus, for exmample, `(seq a b
c)' is the sequence [a,b,c]. The seq function also enables us to move
seamlessly between the values of row variables [which lie outside the
domain of the object quantifiers] and the sequences within the domain
of the object quantifiers given by a theory of sequences.")
(documentation seq "AXIOM: The seq function applied to some objects is
a sequence.")
(Sequence (seq @args))
(documentation "AXIOM: seq with no arguments yields nil.")
(= nil (seq))
(documentation "THEOREM: The length of (seq) is 0. This follows from
the previous axiom and the theorem that the length of nil is 0.")
(= (length (seq)) 0)
(documentation "AXIOM: The length of the seq of some arguments
together with a further argument is one greater than the length of the
seq of those arguments alone. From this and the previous theorem
[together with our simple theory of the integers] it follows that,
e.g., the length of (seq a) is 1, that of (seq a b) is 2, and so on.")
(= (length (seq @args ?x)) (+1 (seq @args)))
(documentation "AXIOM: The seq of some arguments is an initial segment
of the seq of those same arguments together with an additional
argument, and, moreover, the value of the latter sequence applied its
length is that additional argument. This axiom enables us to prove
such facts as: (= ((seq a b c) 2) b), i.e., the second element of the
sequence [a,b,c] is b.")
(and (initseg (seq @args) (seq @args ?x))
(= ((seq @args ?x) (length (seq @args ?x))) ?x))
(documentation "NOTATION: The `seq' operator is a bit awkward. We
therefore introduce a simpler bracket notation to indicate the seq of
some arguments. COMMENT: The BNF needs to be revised a bit for this
notation to be kosher.")
(= [@args] (seq @args))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; INTEGERS ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; The following is a simple theory of the integers with addition and
;; subtraction. It is all the arithmetic that is needed for this
;; ontology.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Basic Axioms for the Integer class ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(documentation "AXIOM: Integer is a class.")
(Class Integer)
(documentation "AXIOM: 0 is an Integer.")
(Integer 0)
(documentation "AXIOM: The successor and predecessor of any integer is
an integer.")
(=> (Integer ?i)
(and
(Integer (+1 ?i))
(Integer (-1 ?i))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Axioms for the Less-than Relation ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(documentation "AXIOM: The less-than relation only applies to integers.")
(Signature < Integer Integer)
(documentation "AXIOM: The less-than relation is transitive on the
integers.")
(TransitiveRelation <)
(documentation "AXIOM: The less-than relation is irreflexive on the
integers.")
(IrreflexiveRelationOn < Integer)
(documentation "AXIOM: The less-than relation is a total ordering on
the integers.")
(TotalOrderingRelationOn < Integer)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Axioms for the Successor and Predecessor Functions ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(documentation "AXIOM: The successor and predecessor functions are
one-to-one on the integers.")
(=> (and
(Integer ?i)
(Integer ?j))
(and
(=>
(= (+1 ?i) (+1 ?j))
(= ?i ?j))
(=>
(= (-1 ?i) (-1 ?j))
(= ?i ?j))))
(documentation "AXIOM: An integer is less than its successor and
greater than its predecessor.")
(=> (Integer ?i)
(and
(< ?i (+1 ?i))
(< (-1 ?i) ?i)))
(documentation "AXIOM: No integer is between a given integer and its
successor or predecessor.")
(=> (and
(Integer ?i)
(Integer ?j))
(not
(or
(and
(< ?i ?j)
(< ?j (+1 ?i)))
(and
(< ?j ?i)
(< (-1 ?i) ?j)))))
(documentation "REMARK: This axiom -- the `Cancellation Axiom' --
entails that every numeric term containing both +1 and -1 can be
replaced by a numeric term containing only +1 or -1.")
(=> (Integer ?i)
(and
(= (+1 (-1 ?i)) ?i)
(= (-1 (+1 ?i)) ?i)))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Axioms for Addition and Subtraction ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(documentation "AXIOM: Recursive definition of Addition.")
(=>
(and
(Integer ?i)
(Integer ?j))
(and
(= (AddFn ?i 0) i)
(= (AddFn ?i (+1 ?j)) (+1 (AddFn ?i ?j)))
(= (AddFn ?i (-1 ?j)) (-1 (AddFn ?i ?j))))))
(documentation "AXIOM: Recursive definition of Subtraction.")
(=>
(and
(Integer ?i)
(Integer ?j))
(and
(= (SubFn ?i 0) 0)
(= (SubFn ?i (+1 ?j)) (-1 (SubFn ?i ?j)))
(= (SubFn ?i (-1 ?j)) (+1 (SubFn ?i ?j)))))
;;;;;;;;;;;;;;;;;;;;
;; Basic numerals ;;
;;;;;;;;;;;;;;;;;;;;
(documentation "It is convenient to introduce definitions for some of
the traditional numerals.")
(= 1 (+1 0))
(= 2 (+1 1))
(= 3 (+1 2))
(= 4 (+1 3))
(= 5 (+1 4))
(= 6 (+1 5))
(= 7 (+1 6))
(= 8 (+1 7))
(= 9 (+1 8))
(= 10 (+1 9))
;;;;;;;;;;;;;;;;;;;;;;;;;
;; Definitional Axioms ;;
;;;;;;;;;;;;;;;;;;;;;;;;;
(documentation PositiveInteger "DEFINITION: A positive integer is an
integer that is greater than 0.")
(<=> (PositiveInteger ?i)
(< 0 ?i))
(documentation NegativeInteger "DEFINITION: A negative integer is an
integer that is less than 0.")
(<=>
(NegativeInteger ?i)
(< ?i 0))
(documentation NonNegativeInteger "DEFINITION: A non-negative integer
is an integer that either 0 or positive.")
(<=> (NonNegativeInteger ?i)
(or
(PositiveInteger ?i)
(= ?i 0)))
(documentation EvenInteger "DEFINITION: An even integer is either 0 or the
result of adding or subtracting 2 from an even integer.")
(<=>
(EvenInteger ?i)
(and
(Integer ?i)
(or
(= ?i 0)
(exists (?j)
(and
(EvenInteger ?j)
(or
(= ?i (AddFn 2 ?j))
(= ?i (SubFn 2 ?j))))))))
(documentation OddInteger "DEFINITION: An integer is odd iff it is not
even.")
(<=>
(OddInteger ?i)
(and
(Integer ?i)
(not
(EvenInteger ?i))))
(documentation "THEOREM: The OddInteger class is the complement of the
EvenInteger class relative to the integers.")
(= OddInteger (RelativeComplementFn EvenInteger Integer))
(documentation AddInverseFn "AXIOM: The additive inverse of a number N
is the result of subtracting N from 0.")
(=> (Integer ?i)
(= (AddInverseFn ?i) (Sub 0 ?i)))
(documentation AbsValueFn "DEFINITION: The absolute value of an
integer INT is INT if INT is positive, otherwise it is its additive
inverse.")
(<=>
(= (AbsValueFn ?i) ?j)
(or
(and
(PositiveInteger ?i)
(= ?i ?j))
(and
(NegativeInteger ?i)
(= ?j (AddInverseFn ?i)))))
(documentation > "DEFINITION: The greater-than relation.")
(<=>
(> ?i ?j)
(< ?j ?i))
(documentation =< "DEFINITION: The less-than-or-equal-to relation.")
(<=>
(=< ?i ?j)
(and
(Integer ?i)
(Integer ?j)
(or
(< ?i ?j)
(= ?i ?j))))
(documentation >= "DEFINITION: The greater-than-or-equal-to
relation.")
(<=>
(>= ?i ?j)
(and
(Integer ?i)
(Integer ?j)
(or
(> ?i ?j)
(= ?i ?j))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; STRUCTURAL NOTIONS THAT REQUIRE SEQUENCES ;;
;; (Row variables essential) ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(documentation valence "A relation has a definite valence only if it is
always true of the same number of arguments. Hence, that number is
defined to be the valence of the relation.")
(=>
(and
(Relation ?R)
(PositiveInteger ?n)
(valence ?R ?n))
(forall (@seq)
(=>
(?R @seq)
(= (length [@seq]) ?n))))
(documentation "AXIOM: Valence is a functional relation.")
(Functional valence)
(documentation "AXIOM: Valence applies only to classes and relations in
its first argument place and positive integers in its second.")
(Signature valence Relation PositiveInteger)
(documentation Signature "The signature of a relation gives the
classes, in order,of which objects standing in the relation,
respectively, must be instances. Thus, for example, the signature
square-root-of relation -- viewed as a relation that holds between a
perfect square and either of its integer square roots -- would be
expressed as `(signature square-root-of PositiveInteger integer)'.")
(=>
(and
(Relation ?R)
(Signature ?R @cls))
(forall (@args)
(=>
(holds ?R @args)
(and
(= (length [@args]) (length [@cls]))
(forall (?n)
(=>
(and
(PositiveInteger ?n)
(=< ?n (length [@args])))
(instance-of ([@args] ?n) ([@cls] ?n))))))))
(documentation nth-domain "AXIOM: The nth-domain relation holds
between a relation REL, positive integer INT, and class CLS then the
INT'th argument of any sequence of which REL is true must be an
instance of CLS. For example, `(nth-domain instance-of 2 Class)'.")
(=> (and
(Relation ?rel)
(PositiveInteger ?int)
(Class ?cls)
(nth-domain ?rel ?int ?cls))
(forall (?seq)
(=>
(and
(Sequence ?seq)
(>= (length ?seq) ?int)
(holds ?rel @args))
(instance-of (?seq ?int) ?cls))))
More information about the Scl
mailing list