Average-case analysis of unification algorithms (Q685442)

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 \textit{M. S. Paterson} and \textit{M. N. Wegman}'s [J. Computer System Sci. 16, 158-167 (1978; Zbl 0371.68013)] 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 \textit{A. Martelli} and \textit{U. Montanari}'s algorithm [ACM Trans. Program. Lang. Syst. 4, 258-282 (1982; Zbl 0478.68043)] and \textit{Robinson}'s algorithm [in \textit{B. Meltzer} and \textit{D. Michic} (ed.), Mach. Intell. 7, Edinburgh (1972; Zbl 0246.00009)] is finally retained in many applications despite its exponential worst- case time complexity. We present unification algorithms in a uniform way and provide average- case complexity theoretic arguments. We estimate the number of unifiable pairs of tree. We analyse the different reasons for failure and get asymptotic and numerical evaluations. We then extend the previous results of \textit{N. Dershowitz} and \textit{J. Lindenstrauss} [Average time analyses related to logic programming, in: 6th Int. Conf. on Logic Programming, Lisboa, 369-381 (1989)] to these families of trees and show that a slight modification of Herbrand-Robinson's algorithms has a constant average cost on random pairs of trees. On the other hand, we show that various variants of Martelli Montanari's algorithm all have a linear average cost on random pairs of trees. The reasons 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 results on the probability of the occur check.