Average-case analysis of unification algorithms

DOI10.1016/0304-3975(93)90208-BMaRDI QIDQ685442zbMATH OpenFDO

Authors Luc Albert, Rafael Casas, François Fages

Publication date 23 January 1994

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0304-3975(93)90208-B

average-case complexity occur check random pairs of trees unifiable pairs of tree unification algorithms

Logic programming (68N17) Analysis of algorithms and problem complexity (68Q25) Symbolic computation and algebraic computation (68W30)

Review text

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.

Recommendations

Cites work

Cited in

(9)

Describes a project that uses

Uses Software

Maple

This page was built for publication: Average-case analysis of unification algorithms

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q685442)