Unrestricted Partial Definitions



next up previous
Next: Conservative Partial Definitions Up: Partial Definitions Previous: Partial Definitions

Unrestricted Partial Definitions

Unrestricted partial definitions can specify any sentence as a defining axiom, as described below. The following table shows the defining axiom specified by each form of unrestricted partial definition:

#&#Definition&Defining Axiom


(defobject ... )&(and ... )&(deffunction ... )&(and ... )&(defrelation ... )&(and ... )&(defrelation ( ... )&(and (=> (member ?x ) (= (length ?x) n)) :=> :axiom )& (=> ( ... ) )& )&(defrelation ( ... )&(and (=> (member ?x ) (>= (length ?x) n)) :=> :axiom )& (=> ( ... ) )& )

In an unrestricted partial definition of an object constant, the first argument, , is the constant being defined, and the remaining arguments, ... , are sentences. For example, the following definition defines the constant id to be a left and right identity for the binary function f.

(defobject id (= (f ?x id) ?x) (= (f id ?x) ?x))

The defining axiom specified by this definition of id (which is just the

conjunction of the second and third arguments in the definition) is unrestricted in that it may contradict other partial definitions of id and f may not have a left and right identity.

In an unrestricted partial definition of a function constant, the first argument, , is the constant being defined and the remaining arguments, ... , are sentences. For example, the following definition defines f to be a function which has a value that is greater than 1 for all numbers.

(deffunction f (=> (number ?y) (> (f ?y) 1)))

The defining axiom specified by this definition of f is just the implication that is the second argument in the definition.

There are two basic forms of unrestricted partial definitions for relations. Both forms allow inclusion of an arbitrary sentence to be a defining axiom for the constant being defined. The second form additionally provides for the specification of necessary conditions for the relation to hold. The second form has two variants, depending on whether a sequence variable is included in the function's argument list.

In the first form of unrestricted partial definition of a relation constant, the first argument, , is the constant being defined and the remaining arguments, ... , are sentences. For example, the following definition defines R to be a relation that holds for all single arguments that are positive numbers.

(defrelation R (=> (> ?z 0) (R ?z)))

The defining axiom specified by this definition of R is just the implication that is the second argument in the definition.

In the second form of unrestricted partial definition of a relation constant, the first argument, , is the constant being defined, the second argument is a list of individual variables specifying the arguments of the relation, and the arguments, and , following the :=> and :axiom keywords, are sentences. The form has two variants, depending on whether the argument list includes a sequence variable. The following is an example of this form of definition in which above is defined to be a binary transitive relation that holds only for "located objects".

(defrelation above (?b1 ?b2)
     :=> (and (located-object ?b1) (located-object ?b2))
     :axiom (transitive above))

The defining axiom specified by this definition of above is:

(and (=> (member ?x above) (= (length ?x) 2))
     (=> (above ?b1 ?b2)
         (and (located-object ?b1) (located-object ?b2)))
     (transitive above))



next up previous
Next: Conservative Partial Definitions Up: Partial Definitions Previous: Partial Definitions



Vishal I. Sikka
Wed Dec 7 13:23:42 PST 1994