A pair of expressions e1 and e2 (called a constraint) is unifiable when e1 and e2 can be made identical by uniformly substituting the variables in them by expressions. Constraints may not be unifiable because of the presence of terms beginning with different function symbols, as in f(x,g(x)) and f(y,a), where x and y are variables, f is a function symbol, and a is a constant. Another reason may be that unification leads to terms occurring in one another, as in f(x) and f(f (x)).
Many efficient algorithms exist for unification, and unification is crucial in logic programming implementations. For efficiency reasons, it is desirable that when a set of constraints is found to be nonunifiable, constraints are deleted in such a manner that the resulting one is maximally unifiable. This paper presents an algorithm for doing so and proves its correctness.
The method is simple. Given a set of constraints C, the author presents an algorithm CLASSIFY(C) that returns a unique partition of the set of subexpressions of C, and a graph U(C) such that C is unifiable if and only if no class of CLASSIFY(C) has two terms beginning with different function symbols and U(C) has no cycles. Then a nondeterministic pushdown automation A(C) is constructed directly from C (using subexpressions as states, C as the input alphabet, and indexed function symbols as the pushdown alphabet) with the property that A(C) has a loop^ if and only if U(C) has a closed walk. Then, to identify a maximal unifiable subset of C, it is sufficient to find all computations of A(C) that involve loops and that attach incompatible equivalent terms under CLASSIFY(C). The crucial lemma shows that it is sufficient to restrict attention to a certain finite set of computations. The the author constructs a Boolean function B written as a sum of products using loops and covers in A(C) such that C1−C is a maximal unifiable if and only if C−C=C1, . . .Cn implies that C1, . . . ,Cn is a product in B.
The presentation is lucid and clear and the proofs are simple and easy to follow. The reader is referred to other papers by the author for a discussion of implementation. Unfortunately, there is no discussion of complexity at all, and the discussion of related work is quite sketchy. Yet, this paper is self contained and rigorous and hence should be of interest to researchers in automatic theorem proving, logic program execution, and general unification theory.
