Equality for Prolog

1. Introduction

Prolog is a computer language based on Horn clause resolu­ tion. The basic resolution procedure, similarly with Prolog, does not allow statements about equality. We cannot, for example, express that 6 = successor(S) and then be able to unify P(6) with P( succesor(5)). We have adapted a Lisp­ based Prolog system < Kahn 82> so that it is possible to specify theorems about equality. The unification algorithm has been modified so that if the unification of two terms fails , an assertion is looked for that will prove the two terms are equal. As with any application of the unification pro­ cedu.re, the proof of equality of the two terms may cause the. binding of variables in either or both of the terms.

Our Prolog-with-Equality is a natural extension to stan­ dard Prolog. We have found several applications for it that extend the power, expressibility, and generality of Prolog. These principally fall into two categories- extensible data­ types and greater opportunities to pass partially specified data objects. The former turns out, surprisingly, to aug-

Equality for Prolog

William A. Kornfeld MIT Artificial Intelligence Laboratory 545 Technology Square Cambridge, Massachusetts 02139

U.S.A.

telephone: (617) 492 6172

arpanet: BAK@MIT-MC

mcut Prolog with all the flexibility of "object-oriented" lan­ guages typified by Smalltalk < Ingalls 78>, and potentially much more. The second major application area is a greatly improved facility for passing partially instantiated data ob­ jects as an alternative to a backtracking-based enumera­ tion of possible bindings. These turn out to be quite easily implemented in Prolog-with-Equality. Moreover, the effect on efficiency in interpreted Prolog is minimal and there is every reason to suppose that most computational overhead that is introduced can be eliminated in compilation.

The notion of equality theorems is very similar to the para­ modulation rule found in the theorem proving literature <Chang, Lee 73>.

2. Example-Rational Number Datatype

We will create a rational number datatype as an example of the use of equality theorems. Rational numbers will be represented by a term made up of the functor rat ~ith two arguments, the numerator and denominator respectively. There is a distinguished predicate symbol equals which is used to specify the equality axioms.

We add the following assertion to our database: 1

(equals (rat ~num1 +-denom1) (rat +-num2 +-denom2)) (times ~num1 ~denom2 +-intermediate) (times ~num2 ~denom1 +-intermediate)

This expresses the usual cross-multiplication rule for decid­ ing if two rationals are equal to one another.

Our augmented unification rule works as follows: When the interpreter attempts to unify two objects <I> and Ill using standard unification anp fails, it will establish the goal (EQUALS <I> W). If this demonstration succeeds, the unification succeeds with the new variable bindings. If this fails, it will attempt to prove (EQUALS W <I>). An attempt to unify (rat 2 3) with (rat <-X 3) will succeed because standard unification succeeds. An attempt to unify

1 Our Prolog syntax is not standard and should be briefly explained. A term is represented as a Lisp list whose first element is the functor and the remaining elements are the arguments. A literal prefaced by the symbol "+-" is a variable.

(rat 2 3) wi!,h (rat ··X 6) will cause the goal

(EQUALS (RAT 2 3) (RAT <-X 6))

to be posed by the system. This will succeed with the variable <-X bound to 4. The original computation continues with this binding and it is placed in the trail for undoing on backtracking.

We have not yet told the system how to match rationals with any other kind of object. We wish to express a method to decide if a rat is the same as an integer. The following assertion is added:

(equals (rat <-num <-denom) <-n) (type <-n integer) (if (and (variable <-num) (variable <-denom)) (and (= <-num <-n) (= <-denom 1)) (times <-denom <-n <-num))

If both the numerator and the denominator are uninstan­ tiated it succeeds by unifying the numerator with the in­ teger, otherwise it proves the multiplicative relationship that must hold for the equality to hold.

The following little program will now succeed 3 times:

(member (rat 4 <-x) [2 3 (cons <-y <-z) (rat <-r <-w) (rat 2 7)]) <-x = 2 <-r = 4, <-x = <-w <-x = 14

We will also wish. to specify th~ behavior of this new data­ type for several additional relations. The > relation for rationals is implemented with ·the following assertion:

(> (rat <-n1 <-d1) (rat <-n2 <-d2)) :­ (times <-n1 <-d2 <-x) (times <-d1 <-n2 <-y) (> <-x <-y)

This rule could of course work in a Prolog without equality theorems when comparing two terms beginning with the functor rat. Now, however, if we try to prove the goal (> (rat 3 2) 1), the attempt to unify this goal with the head of this assertion will cause an attempt to prove that 1 equals (rat <-n2 <-d2) which will succeed with the ap­ propriate bindings (n2=1, d2=1), allowing the > goal to succeed. In other languages this might be called "automatic type conversion."

3. Extensible Datatypes and Generic Operations

Equality theorems allow us to gain the modularity advantages of generic operations and class structuring as are found in object-oriented languages like SmallLalk. The important contributions of this class of languages are two:

1. One can specify methods for computing facts about whole classes of objects and then have those methods auto­ matically inherited by subclasses.
2. A given operation will have different effects on different data, in a manner determined ·by the datum's class. This is decided at run time rather than compile time.

The paradigm of logic programming is very different from the paradigm of message passing systems. We do not have "objects" which receive "messages." The role of objects are played by terms; the role of messages by relations. The concept of "class" has no formal analog in Prolog-with­ Equality. The effect of class structuring is accomplished by the use of equals assertions. A subclass relationship is indicated by a single equals assertion containing terms for the sub- and super-class. The pattern of variables between the two terms and the body of the assertion express the relationship between the two classes.

As an example, we might have the class regular-polygon. All regular polygons have four attributes, an X andY loca­ tion, a side length, and the number of sides. In Prolog we might want to specify a method for computing the areas of regular polygons. This would be done as follows:

(area (regular-polygon c~x ~y ~side-number ~length)) ~area) (quotient 180 ~side-number ~theta) (cotangent ~theta ~cotangent) (times ~length ~length ~length-squared) (times ~length-squared ~side-number ~prodl) (times ~prodl ~cotangent ~prod2) (quotient ~prod2 4 ~area)

We could then have a functor equilateral-triangle that is defined to be equal to a regular-polygon with three sides:

(equals (equilateral-triangle <-x <-y <-length) (regular-polygon <-x <-y 3 <-length)) :-. Then if we prove the goal (area (equilateral-triangle <- <- 100) <-ans)

the attempt to unify it with the head of the area assertion will result in an attempt to show the term with functor equilateral-triangle is equal to a term with functor regular-polygon. This will succeed with <-length bound to 3 and the goal will succeed with <-ans bound to 150. Of course, since this is Prolog, we could ask the question: "How long does the side of an equilateral triangle have to be to have an area of 150?" This would be:

(area (equilateral-triangle <- <- <-length) 150)

This goal will succeed with <-length bound to 100.

We could also have area assertions for other kinds of objects such as ellipses:

(area (ellipse ~x ~y ~minor-axis ·major-axis) ~area) :-

This will not interfere in any way with goals asking for the areas of triangles because there is no theorem that allows us to show Triangles and Ellipses are equal.

We could define a circle by saying:

(equals (circle <-x <-y .. radius) (ellipse <-x <-y <-diameter .. diameter)) :- (times 2 <-radius <-diameter)

that will then allow the usc of theorems about ellipses for answering questions about circles.

There is one sense in which we have more flexibility in Prolog-with-Equalit.y than can be achieved with object­ oriented languages. As with other aspects of Prolog, we arc able t.o leave many aspects of onr computation undeter­ mined and still carry out the computation. Within object­ oriented languages an object 's class is known at object in­ stantiation time. Thi s is not. true for terms in Prolog-with­ Equalit.y. Suppose we have the goal:

(and (= ~obj (regular - polygon (~ ~ ~side - number ~length))) (= ~side-number 3) (predicate ~obj))

The variable obj is unified with a regular-polygon of an indeterminate number of sides. Side-number is later unified with 3 and predicate is called. If predicate has assertions that will allow proofs about triangles then we will succeed because obj will unify with triangles.

A fanciful example involves the term closed-figure with two argument, a perimeter and an area. We can state the followin.g equality assertion:

(equals (closed- figure ~perimeter ~area) (circle ~ ~ ~radius)) (times 6. 2831853 ~radius ~perimeter) (times ~radius ~radius ~squared-radius) (times 3.14159265 ~radius-squared ~area)

expressing the fact that if the perimeter of a closed figure is 27rr and t.he area is 1rr 2 for some r, then it is a circle. A closed-figure described in this way, if instantiated to be a circle, can be used m any proof that was defined using the circle functor.

The code above is most unlikely to appear as part of a practical program. When things are left so undetermined, simple programs can take very long because there may be very esoteric ways of doing proofs. It is important, however, : to see that such generality is available. Moreover, the uses : of equality theorems that model the class-structuring idea are very efficiently implemented. We discuss these issues briefly in section 7.

4. Partially Specified Obje.cts

One of the desirable features of Prolog is its ability to deal with partially instanti<Jted data objects. One way to look at this is that the partially instantiated data object stands for a non-singleton subset. of t.hc Herbrand Universe cor­ responding to our Prolog program. If we were not able to pass such objects freely in our programs the control struc­ ture of Pro log (or any logic programming language remotely like it) would require us to successively generate bindings of the variable to ground objects for consideration by the remainder of the proof. This is the power that unification gets us and also t.he principle difference between Prolog and the language Micro-Planner <Sussman, et. a!. 70 > which preceded it but was otherwise similar. We find that our in­ clusion of equality proofs in Prolog extends the range of possibility for passing partially instantiated data. In some cases this can significantly improve the efficiency of pro­ grams by replacing an otherwise expensive enumeration of ground terms with backtracking. In other cases it makes possible a program that would not be possible otherwise because there is no convenient way to enumerate the space.

We define a binary functor called f1 which will represent an arbitrary partially specified object. The first argument to an n term is a variable that is uninstantiated when the term is introduced. The second argument is a relation that must hold for all terms in the subset of the I-Ierbrand Universe that this f1 term represents; it is expressed in terms of the uninstantiated variable. For example, if we execute t.he goal (> <-x 3) where the variable x is at this point uninst.antiated, we will succeed with the binding for x: CO <-num C> .. num 3)) . This represents (and will unify with) all numbers that are greater than three. When this is unified with a number (e.g. 5) the variable num is unified with 5 and the unification succeeds of the relation succeeds (which it does because three is greater than five).

The equals relation for f1 terms is defined as follows:

(equals en ~obj ~relation) ~thing) (instantiate ~thing ~value) (= +-obj ~value) ~relation (equals (0 (and +-obj1 ~relation1) (0 ~obj2 +-relation2)) (not-instantiated ~obj1) (not-instantiated ~obj2) (conjoin-relations +-obj1 +-relation! (= ~obj1 ~obj2) · .. obj2 ~relation2 ~obj ~relation) (= ~obj2 (0 ~obj ~relation)))

The predicate instantiate succeeds if its argument is in­ stantiated, i.e. that it is neither a variable nor an uninstan­ tia:bed -0 term; when it succeeds the second argument is bound to the instantiated value. The first assertion declares that an n term is equal to something if the item the n functor represents ( obj) is equal to the thing's instantiated value and the constraining relation is true. The second assertion applies if two !1 terms are unified and neither has yet been instanti ated . Doth !1 terms are made equal to one another and to another !1 term whose relation is the conjunct of the two previous relations. This new term represents the intersection of the space of possible ground terms of the two !1 terms that were unified.

The code for > is as follows: 2

(> +-m +-n) (cases ((and (instantiate +-m +-ml) (ins tant iate +-n +-nl)) (lisp-> +-ml +-nl)) ((instantiate +-m +-ml) (= +-n (0 +-num (> +-ml +-num)))) ((instantiate +-n +-nl) (= +-m (0 +-numl (> +-numl +-nl)))) ((= +-n (0 +-num (> +-m +-num))) (= +-m (0 +-numl (> +-numl +-n)))))

If we had the Prolog goal:

(and (> <-x 3) (member <-x [2 4 6 <-y]))

we would succeed 3 times with the bindings 4, 6, and (!1 <-num1 (> <-num1 3)), the last which is also bound to y.

The goal

(and (> <-x <-y) (= <-x 3) (= +-y 2)) succeeds, while the goal: (and (> <-x +-y) (= <-x 3) (= +-y 4))

does not.

The basic arithmetic functions are defined in a similar way, and have the property of not failing if any or all of their arguments are ;:wt instantiated. The definition of the times predicate is:

2 The preponderance of the impure instantiate relation is only neces­ sary when data is to be passed to evaluable predicates (such as lisp->). As <Warren 77 > points out, most of" the work in building a Pro log is in writing the "evaluable predicates" . However, our > relation is a true Prolog predicate in that it is not required for its arguments to be instantiated when called. Our goal is to be able to bury such impure evaluable predicates inside logically sound relations.

(times +-argl +-arg2 +-result) (cases ((instantiate +-arg1 +-ansl) (cases ((instantiate +-arg2 +-ans2) (lisp-value +-result (* +-ansl +-ans2))) ((instantiate +-result +-ans) (lisp-value +-arg2 (/ / +-ans +-ansl))) ((= +-result (0 +-ans (times +-ans l +-arg2 +-ans))) (= +-arg2 (0 +-ans2 (times +-ansl +-ans2 +-result)))))) ((instantiate +-arg2 +-ans2) (cases ((instantiate +-resul t +-ans) (lisp-value +-argl (// +-ans +-ans2))) ((= +-result (0 +-ans (times +-argl +-ans2 +-ans))) (= +-argl (0 +-ansl (times +-ansl +-ans2 +-result)))))) ((instantiate +-result +-ans) (= +-argl (0 +-ansl (times +-ansl +-arg2 +-ans))) (= +-arg2 (0 +-ans2 (times +-arg l +-ans2 +-ans)))) ((= +-argl (0 +-ansl (times +-ansl +-arg2 +-result))) (= +-arg2 (0 +-ans2 (times +-argl +-ans2 +-result))) (= +-result (0 +-ans (times +-arg l +-arg2 +-ans)))))

The definition of times determines which arguments are instantiated and takes an appropriate action. If two or three are instantiated it executes an evaluable predicate corresponding to a Lisp function call. Otherwise it creates !1 terms that express the arithmetic constraints on the value of the variable. Other arithmetic funct ions are defined analogously. Prolog programs written using these relations have the property that the relations can be in any order and the program will find the answer without any backtracking. For example, the goal

(and (times <-x +y +-z) (plus +a 3 +-x) (plus 1 +a 2) (= +z 12))

will succeed with correct bindings for all the variables. This is accomplished with sequential evaluation of the predicates and no backtracking. Ari thmetic expressed in this way can solve systems of equations that are not simultaneous. 3 It is a very efficient way of doing arithmetic, and will work for floating point as well as integer computations. 4

Arithmetic expressions are an example where it is impos­ sible in a practical sense to generate each of the possible bindings as ground terms. However there are other situa­ tions where we may wish to use !1 terms as an alternative to enumerating the bindihgs.

3 This is equivalent in power to the constraint network formalisms <Borning 79, Sussman, Steele 78> .

4 IC-Prolog < Clark 82.> provides arithmetic on integers by building the integers using successor. This is very general, but not efficient Cor practical problema.

Consider the following goal:

where on entry very-long-list is instantiated to a very long list and xis uninstantiated. Suppose that pred is true of only a few of those elements. In this case, using the standard Pro log definition of member, the relation would become a generator of succesive elements from the list. An alternative way of writing member would be that, if x is not instantiated upon entry into the member relation, the relation would instantiate x to:

This would effectively save the constraint that x be a mem­ ber of the list until there was some item under considera­ tion. Then, and only then, would the constraint be checked.

It is far from clear how one would characterize the condi­ tions under which 0 terms will be preferable to using a predicate as a generator. Yet this does seem an important tool. It is distinct from, yet compatible with, extralogical control annotation as in IC-Prolog <Clark 82>.

5. Functional Notation

Many people are uncomfortable with the flat relational style of Prolog as opposed to the functional notation Lisp and most other languages. Lisp syntax allows the com­ position of functions without the need to introduce tem­ porary variables to glue successive relations together as in the above example for computing the area of a polygon. We can straightforwardly augment Prolog with functional notation by using equality theorems:

Notice that we distinguish the function %plus from the relation plus. It makes no sense in (logic or) Prolog to unify a relation and a function. Using these new functors we can define a temperature converter relation that expresses the relationship between the Fahrenheit and centigrade scales. The relation is a one-liner:

(temp-converter ~f (%times (%difference ~f 32) (rat 5 9)))

This is like the "executable pattern" of <Nakashima 82>.

6. Equality Assertion Invocation

Prolog constructs can be understood in either a declara­ tive or procedural sense. Thus far we have not considered the precise procedural semantics of Prolog-with-Equality. Certain care must be exercised in defining the procedural semantics to avoid infinite loops or otherwise unaccept­ ably wasteful searches. Our solution to this yields a ~s­ tem which is far from complete in the logical sense, yet is sufficient for the classes of examples in this paper. It has a further desirable property that allows the compiler to precompute certain information that will allow most fail­ ing unifications to fail in constant time. Such a property is critical if this mechanism is to find its was into practical programs.

The first restriction we put on unification via equality asser­ tions is that the assertions can only be used one way. Suppose we attempt to match (foo 1) with (bar 2). This will cause the unifier to generate a goal of the form:

Now suppose we had an equality Lheorem whose head was: (equals (bar ~n) ~s). An attempt to unify the goal with this assertion head would cause a recursive goal of (equals (foo 1) (bar 1)). This will lead to an infinite computation. To avoid this problem we require that in matching the first term of the equals goal with its coun­ terpart in the head of the assertion the functors must be the same. The unification of the second argument may recursively create new equality assertions. This allows for chains of equality matches (but not cycles).

Unification in Prolog-with-Equality, as in standard Prolog, is deterministic-it can only succeed once. For normal Prolog there is no problem because there can be only one most general unifier. However, in consideration of of models other than the standard Herbrand model (see, for example, a survey of equational theories <Siekmann, Szabo 82>) it is possible for there to be no unique most general unifier. To properly handle such cases would require introducing a backtracking point in the unification itself. For the class of applications I have looked at so far there does not seem to be a compelling reason for doing so, yet this is possible route to be taken in the future. One way this could be understood within the class hierarchy paradigm is that there may be more than one most general unifier because there is more than one way to view the fitst as an instance of the second.

7. Efficiency Considerations

It is critically important from the efficiency point of view that one of the functors must be explicitly present as the first functor of an equals assertion. Thus equals asser­ tions can be grouped in much the same way that assertions with the same first predicate are grouped in the implementation. If one tries to match two terms, neither of which has equals assertions for it, the match can fail quickly. In the event that one or both have assertions associated with them a series of equals derivations may ensue that is potentially coslly. A compil'er can do mttch to eliminate this when­ ever the terms are not relatable by figuring the chains of functors statically from the code. If neither functor can be reached by a chain of equals assertions from the other the two can definitely not be unified. By using hash tables to store this information most failures can be discovered very quickly. In particular, the usc of equality to model object-oriented languages requires no backtracking and a small, constant, overhead to determine failure.

8. Conclusions

My experience with Prolog-with-Equality to date has been very encouraging. The modifications necessary to the inter­ preter to make equality theorems possible was done in one even ing of programming. The basic paradigms explored (extended datatyping, partially instantiated 0 terms) ap­ pear quite natural and general. Moreover the added fea­ tures do not impinge on the efficiency of basic Prolog. I am hopeful that new paradigms for using equality will emerge as more experience is gained.

I am currently developing a system in Prolog-with-Equality for composition of musical examples of species counter­ point. This area of music theory has been studied exten­ sively over several centuries and large, precise rules systems exists for it. The two paradigms are quite important for developing this system. The partially instantiated term notion is used to represent classes of pitches (when the fully instantiated note must be one of those pitches). The unification process for two partially instantiated pitches be­ comes a set intersect. This way expensive backtracking is avoided.

9. Bibliograp~

Attardi G., M. Simi, Consistency and Completeness of Olv!EGA, a Logic for Knowledge Representation, Sev­ enth International Joint Conference on Artificial Intellgence, Vancouver, August 1981.

Borning, A., Thinglab-A Constraint-Oriented Simu­ lation Laboratory, Xerox PARC report SSL-79-3, July 1979.

Chang, C., R. Lee, Symbolic Logic and Mechanical Theo­ rem Proving, Academic Press, 1973.

Clark, K., IC-Prolog Language Features, in Clark & Tarn­ lund, Logic Programming, Academic Press, 1982.

Ingalls The Smalltalk-76 Programming System: Design and Implementation, Fifth Annual ACM Symposium on Principles ol' Programming Languages, Tucson Ari'l.ona, Jan­ uary 1978.

Kahn, K., Unique Features of LM-Prolog, unpublished manuscript.

Nakashima, H. Prolog K/ R language f eature, First Inter­ national Logic Programming Conference, Marseille, Sep­ tember, 1982.

Siekmann, J., P . Szabo, Universal Unification and a Class­ ification of Equational Th eories, 6th Conference on Auto­ mated Deduction, New York, June 1982.

Sussman, G., T. Winograd, E. Charniak, Micro-Planner Reference Ma~ual, MIT Artificial Intelligence Laboratory memo 203, 1970.

Sussman, G., G. Steele, Constraints MIT Artificial Intelli­ gence Laboratory memo 502, November, 1978.

Warren, D., Implementing Prolog- Compiling Predicate Logic Programs, University of Edinburgh Department of Artificial Intelligence Report No. 39.