Average-case analysis of unification algorithms

AbstractUnification 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 (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 (Robinson 1971), is finally retained in many applications despite its exponential worst-case time complexity. In this paper, we present unification algorithms in a uniform way and provide average-case complexity theoretic arguments. We estimate the number of unifiable pairs of trees. We analyse the different reasons for failure and get asymptotical and numerical evaluations. We then extend the previous results of Dershowitz 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 that various variants of Martelli and Montanari's algorithm all have a linear average cost on random pairs of trees. The reason 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 present a combinatorial extension of the problem for terms formed over a countable set of variables, and extend to this framework the results on the probability of the occur-check