Average Case Analysis of Unification Algorithms

Abstract : 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.
Type de document :
Communication dans un congrès
C. Choffrut and M. Jantzen. Proceedings of STACS'91 - 8th Annual Symposium on Theoretical Aspects of Computer Science, 1991, Hamburg, Germany. Springer, 480, pp.196-213, 1991, Lecture Notes in Computer Science. 〈10.1007/BFb0020799〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00917726
Contributeur : Paul Zimmermann <>
Soumis le : jeudi 12 décembre 2013 - 12:42:17
Dernière modification le : vendredi 25 mai 2018 - 12:02:03

Lien texte intégral

Identifiants

Collections

Citation

Luc Albert, Rafael Casas, François Fages, A. Torrecillas, Paul Zimmermann. Average Case Analysis of Unification Algorithms. C. Choffrut and M. Jantzen. Proceedings of STACS'91 - 8th Annual Symposium on Theoretical Aspects of Computer Science, 1991, Hamburg, Germany. Springer, 480, pp.196-213, 1991, Lecture Notes in Computer Science. 〈10.1007/BFb0020799〉. 〈hal-00917726〉

Partager

Métriques

Consultations de la notice

334