AVERAGE-CASE ANALYSIS OF UNIFICATION ALGORITHMS

Unification in first-order languages is a central operation in symboli c computation and logic programming. Many unification algorithms have been proposed in the past: however. there is no consensus on which alg orithm is the best to use in practice. While Paterson and Wegman's lin ear unification algorithm (1978) 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 (Martelli and Montanari 1982), and Robinson's algorithm (Ro binson 1971), is finally retained in many applications despite its exp onential worst-case time complexity. In this paper, we present unifica tion algorithms in a uniform way and provide average-case complexity t heoretic arguments. We estimate the number of unifiable pairs of trees . We analyse the different reasons for failure and get asymptotical an d numerical evaluations. We then extend the previous results of Dersho witz and Lindenstrauss (1989) to these families of trees and 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 tha t various variants of Martelli and Montanari's algorithm all have a li near average cost on random pairs of trees. The reason is that failure s by clash are not sufficient to lead to a constant average cost; an e fficient occur check, i.e. without a complete traversal of subterms, i s necessary. In the last section, we present a combinatorial extension of the problem for terms formed over a countable set of variables, an d extend to this framework the results on the probability of the occur -check.