Read an Excerpt
The Implementation of Prolog
By Patrice Boizumault, Ara M. Djamboulian, Jamal Fattouh PRINCETON UNIVERSITY PRESS
Copyright © 1993 Princeton University Press
All rights reserved.
ISBN: 978-0-691-08757-3
CHAPTER 1
UNIFICATION
Unification is an essential part of any Prolog system. Unification is the process of determining whether two terms can be made identical by appropriate substitutions for their variables. The first unification algorithm was proposed by J. A. Robinson in 1965 [Rob65].
But a vast majority of Prolog systems do not use Robinson's unification algorithm. For reasons of efficiency, they deliberately choose not to perform the occur check (a variable can thus be unified with a term containing it).
This choice entails some problems from a theoretical point of view, since it destroys the soundness of the SLD-resolution strategy used by Prolog. From a practical point of view, a unification algorithm without the occur check may not terminate.
In order to solve these problems, Prolog-II [Col82b], [Can82], [Kan82] has proposed a new theoretical model taking into account the infinite terms created by the absence of occur check. Unifying two finite terms is replaced by solving a system of equations over rational trees.
After briefly recalling some definitions, we will describe the unification algorithm of J. A. Robinson. Then we will study the particular algorithm used by Prolog by indicating the problems that arise when the occur check is abandoned. We will then examine various proposals to remedy this situation, particularly Prolog-II's approach. Finally, we will close with the implementation of the various algorithms previously described.
1.1. Definitions
A Prolog term is a variable, a constant symbol, or a structured term. A structured term is either a list or a functional term. A functional term t is an expression of the form f(t1, ..., tm) where f is a functional symbol, and tt are terms. We will say that f is the functor of t whose arity is m. Lists can also be specified as functional terms using the functor '.' of arity 2. [a, b, c] and '.' (a '.' (b, '.' (c, []))) denote the same list.
A substitution σ is a finite set of pairs (variable, term) such that the same variable does not appear as the left side of two or more pairs.
Example:
σ = [(Y, f(X, Z)); (X, α)}.
We will say that the variable X (resp. Y) is bound to the term α (resp. f(X, Z)). On the other hand, the variable Z is said to be free, since it does not appear as the left side entry in any pair. Applying the substitution σ to the term t gives the term t' = σ(t) obtained by replacing in t, all occurrences of variables by their related terms given by σ. t' is said to be an instance of t.
Example:
let t = g(X, Y) and σ the preceding substitution
then t' = σ(t) = g(a, f(a, Z)).
A unifier of two terms t1 and t2 is a substitution σ such that σ(t1) = σ(t2). If such a substitution exists, we say that the terms t1 and t2 are unifiable.
Examples:
t1 = f(X, Y) and t2 = f(Y, g(a)) are unifiable and the substitution
σ = {(X, Y); (Y, g(a))} is such that σ(t1) = σ(t2).
t1 = f(X, X) and t2 = f(a, b) are not unifiable.
A unifier σ of two terms t1 and t2 is said to be the most general unifier of t1 and t2 if and only if, for all unifiers θ of the two terms, there exists a substitution λ such that θ = λ * σ.
Example:
Let t1 = f(X, a) and t2 = f(Y, Z).
Their most general unifier is σ = {(X, V); (Z, a)}.
If θ = {(X, Y); (Y, a); (Z, a)} then θ(t1) = θ(t2)
but there exists λ = {(Y, a)} such that θ = λ * σ.
If two terms are unifiable then their most general unifier always exists. The first algorithm to calculate this was proposed by J. A. Robinson in 1965 [Rob65].
1.2. Robinson's Unification Algorithm
We will look at the unification algorithm of J. A. Robinson [Rob65], [Rob71] in its recursive form as described in [BC83]. Constants are functional terms of arity zero.
Given: two terms t1 and t2.
Result: a pair (bool, σ) such that:
-bool = true if and only if the two terms are unifiable.
-if bool = true then σ is the most general unifier for t1 and t2.
Algorithm:
if one of the two terms is a variable x, call the other term t.
then if x = t
then bool := true; s := θ
else if occur(x, t)
then bool := false
else bool := true; σ := {(x, t)}
endif
endif
else let t1 = f(x1 ..., xm) and t2 = g(y1, ..., yn)
if f ≠ g or n ≠ m
then bool := false
else i := 0
bool := true;
σ:= θ;
while i< n and bool do
i := i + 1;
(bool, σ1) := unify(σ(xk), σ(yk));
if bool then σ := σ1 * σ endif
endwhile
endif
endif
Thus, unify(f(X, a, T), f(Y, Z, b)) successively constructs the substitutions {(X, Y)}, then {(X, Y); (Z, a)}, and finally {(X, Y); (Z, a); (T, b)}, which is the most general unifier of the two terms whose most general common instance is f(Y, a, b).
According to the algorithm of J. A. Robinson, a variable cannot unify with a term containing it. Thus, the two terms f(X, Y) and f(Y, g(X)) are nonunifiable. This verification, called occur check, is carried out by the function occur(x, t) which returns true if and only if the variable ? appears in the term t.
1.3. Prolog's Unification Algorithm
The vast majority of Prolog systems do not perform the occur check. Thus, contrary to Robinson's unification algorithm, a variable can be unified to a term containing it. After we describe the reasons for such a choice, we will examine the problems it entails.
1.3.1. Unification without Occur Check
The unification algorithm of Prolog does not perform the occur check. When unifying a variable x against a term te, the system does not check whether the variable x occurs in te. Thus, the two terms f(X) and f(g(X)) become unifiable in Prolog with unifier {(X, g(X))}.
The main reason for this omission is a sensible gain in execution time. Indeed, the occur check is a costly operation since, before binding a variable x to a term te, one must scan the term te in order to determine whether x occurs in it. Without the occur check, unifying a variable x to a term te is done in constant time independent of the size of te. As noted by A. Colmerauer in [Col82a], the concatenation of two lists is quadratic in the length of the first list if a unification algorithm with an occur check is used, whereas it is linear without such a test.
So unifying a term against a variable, which can be considered the basic operation in Prolog, can take constant time only if the occur check is omitted. As quoted by Pereira in [Per84a], "The absence of occur check is not a bug or design oversight, but a conscious design decision to make Prolog into a practical programming language."
1.3.2. Resulting Problems
The absence of the occur check entails the unsoundness of the resolution strategy used by Prolog. Consider the following Prolog program:
unsound :- eq(Y,f(Y)).
eq(X,X).
The proof of unsound leads to a success unifying Y to f (Y) while unsound is not a logical consequence of the program.
Unification without occur check is likely to generate circular terms, which no longer belong to the universe of finite terms. So, such a unification algorithm may not terminate. In fact, any attempt to access an infinite term leads to a loop.
When trying to prove the goal eq(f (X, Y, X), f (g(X), g(Y), Y)), the unification algorithm will enter an infinite loop in attempting to unify X and Y in the substitution {(Y, g(Y)); (X, g(X))}.
This problem did not arise during the proof of unsound because the circular term created by unifying Y and f (Y) is never accessed. But attempting to write such a term will lead the Prolog printer to enter a loop:
| ?- eq(Y, f(Y)).
Y = f (f(f(f(f(f(f(f(....
These examples may appear artificial. In fact, experience shows that a vast majority of the problems usually solved in Prolog do not require the occur check. But there are useful programs in which the absence of occur check is a major drawback.
This problem appears most commonly in the use of difference lists [LI086]. A difference list is a term of the form d(X, Y) that represents the difference between the two lists X and Y. d (X, X) denotes the empty list. The main interest of difference lists is that they can be concatenated in constant time.
Consider the following example from [SS87]. We want to implement queues so that insertion and deletion are constant time operations.
enqueue(Item, d(QS, [Item I QT]), d(QS, QT)).
dequeue(Item, d([Item I QS], qT), d(QS, QT)).
empty_queue(d(QS, QS)).
Every call to empty_queue with a nonempty list as argument proceeds erroneously by creating a circular term.
1.4. Solutions
A first solution is to bring in the unification algorithm with occur check, when necessary. The second approach consists in extending the theoretical Prolog model to take the infinite terms into account. This is the solution proposed by Prolog-II.
1.4.1. Bring in the Occur Check
A first remedy is to introduce into the Prolog system an option for unification with occur check. The user may then choose, depending on the circumstances, the suitable unification algorithm, that is, with or without occur check. Generally, it is this latter option that holds by default. This is the case for Prolog-P [BJM83], [Man84], with the options occur-on and occur-off and also for Prolog-Criss [Don83], [Lep85]. Nevertheless, in the default mode, the user still faces the same problems described above.
A more suitable approach is to have a preprocessor that is able to detect places in a Prolog program where infinite terms may be created. D. Plaisted [Pla84] has developed such a preprocessor, which adds checking code to these places in order to cause subgoals to fail if they create infinite terms.
1.4.2. Prolog-II's Solution
Prolog-II offers a completely different solution, which consists in taking advantage of, rather than rejecting, the infinite terms. As shown by A. Colmerauer [Col82a], [Col82b], infinite trees are natural representations for graphs, grammars, and flowcharts. Prolog-II extends the domain of the finite terms to rational trees (infinite terms) and accordingly replaces the notion of unification with that of the resolution of a system of equations over rational trees.
We will briefly present the basic notions of this approach with some examples. The interested reader can refer to [Col82b] and [CKC83], where a complete description of the Prolog-II theoretical model may be found.
1.4.2.1. Definitions
A tree is rational if and only if the set of its subtrees is finite. In particular, each finite tree is rational. Thus, f(X, g(a, Y), h(Z)) and f(f(f ... (X) ...)) are rational trees. In fact, the first one is a finite tree and the second one contains itself as its only subtree.
Since a rational tree has only finitely many subtrees, it can be represented simply by a finite diagram. All nodes having the same subtrees are merged together. So diagrams 2 and 3 of Figure 1.1 represent the same rational tree.
A tree assignment is a set X of the form X = {x1 = t1, ..., xn = tn, ...} where the xi's are distinct variables and the ti's are rational trees, te(X) denotes the tree obtained by replacing each occurrence of xi in the term te by the corresponding tree ti according to the tree assignment X.
The tree assignment X is said to be a solution of the system, possibly infinite, {p1 = q1, p2 = q2, ...} if X is a subset of a tree assignment Y such that for all i, pi(Y) = qi(Y).
A reduced system is a finite system of equations, without a cycle of variables, of the form {x1 = t1, ...,xn = tn} where the xi are distinct variables and the ti are terms.
We define a cycle to be a nonempty system of the form {t1 = t2, ..., tn = t1} where the ti are distinct terms.
Finally, we define [Can84], [Can86] the representative of a term p in a system S without a cycle as follows: if there is an equation in S of the form p = q, then rep(p, S) = rep(q, S) else rep(p, S) = p.
1.4.2.2. An Algorithm for Base Reduction
The algorithm for base reduction is used to transform a finite system of equations into an equivalent system, that is either reduced or trivially unsolvable. In fact, one can show [Col82b], [CKC83] that each system in reduced form is solvable (the solvability property) and that each solvable system is equivalent to a system in reduced form (the normal form property).
We will present an algorithm based on a version described by M. Van Caneghem in his thesis [Can84]: let T be the initial system. We try to transform the initial system T into an equivalent reduced system S.
S := θ;
E := θ; E saves the equations which are generated by the reduction
namely all the pairs of subterms previously tried to unify
E is called the stack of equations.
Reduce(T):
Given: a finite system of equations T.
Result: a pair (ok, S) such that
-ok = true if and only if T can be put in reduced form,
-if ok = true then S is a reduced system equivalent to T.
Algorithm:
if T = θ then ok := true
else let (s = t) be an equation of T
let s1 = rep{s, S [union] E), t1 = rep(t, S [union] E)
if s1 = t1
then reduce(T - {s = t})
else
if one of the terms is a variable x, let y be the other term
then S := S [union] {x = y}
reduce (T - {s = t})
else
let s1 = f(x1, ..., xn) and t1 = g(y1, ..., ym)
if (f = g) and (m = n)
then E := E [union] {s1 = t1)
reduce ((T - {s = t}) [union] {x1 = y1, ..., xn = yn})
else ok:=false
endif
endif
endif
endif
One of the important points in this algorithm is the calculation of the representative of a term by means of S and the stack of equations E. Indeed, this computation is done at each step of the reduction and is a function of the size of the stack of equations. We must therefore try to minimize the size of this stack. For a discussion of this problem and the comparison between different algorithms, we refer the reader to M. Van Caneghem's thesis [Can84].
(Continues...)
Excerpted from The Implementation of Prolog by Patrice Boizumault, Ara M. Djamboulian, Jamal Fattouh. Copyright © 1993 Princeton University Press. Excerpted by permission of PRINCETON UNIVERSITY PRESS.
All rights reserved. No part of this excerpt may be reproduced or reprinted without permission in writing from the publisher.
Excerpts are provided by Dial-A-Book Inc. solely for the personal use of visitors to this web site.
