Average case analysis of unification algorithms

Unification in first-order languages is a central operation in symbolic computation and logic programming. Many unification algorithms have been proposed in the past, however there is no consensus on which algorithm is the best to use in practice. While Paterson and Wegman’s linear unification algorithm has the lowest time complexity in the worst case, it requires an important overhead to be implemented. This is true also, although less importantly, for Martelli and Montanari’s algorithm [MM82], and Robinson’s algorithm [Rob71] is finally retained in many applications despite its exponential worst-case time complexity. There are many explanations for that situation: one important argument is that in practice unification subproblems are not independent, and linear unification algorithms do not perform well on sequences of unify-deunify operations [MU86]. In this paper we present average case complexity theoretic arguments. We first show that the family of unifiable pairs of binary trees is exponentially negligible with respect to the family of arbitrary pairs of binary trees formed over l binary function symbols, c constants and v variables. We analyze the different reasons for failure and get asymptotical and numerical evaluations. We then extend the previous results of [DL89] to these families of trees, we show that a slight modification of Herbrand-Robinson’s algorithm has a constant average cost on random pairs of trees. On the other hand, we show that various variants of Martelli and Montanari’s algorithm all have a linear average cost on random pairs of trees. The point is that failures by clash are not sufficient to lead to a constant average cost, an efficient occur check (i.e. without a complete traversal of subterms) is necessary. In the last section we extend the results on the probability of the occur check in presence of an unbounded number of variables.