[Submit a comment] [RTALooP home] [Index] [Previous] [Next] [Postscript] [PDF] [BibTeX Source] [LaTeX Source]

Problem #44

Originator: Hubert Comon
Date: April 1991

Summary: How to compute finite and complete sets of unifiers for any finitary unification problem of a syntactic equational theory.

“Syntactic” theories enjoy the property that a (semi) unification algorithm can be derived from the axioms [JK91][Kir86]. This algorithm terminates for some particular cases (for instance, if all variable occurrences in the axioms are at depth at most one, and cycles have no solution) but does not in general. For the case of associativity and commutativity (AC), with a seven-axiom syntactic presentation, the derivation tree obtained by the non-deterministic application of the syntactic unification rules (Decompose, Mutate, Merge, Coalesce, Check*, Delete) in [JK91] can be pruned so as to become finite in most cases. The basic idea is that one unification problem (up to renaming) must appear infinitely times on every infinite branch of the tree (since there are finitely many axioms in the syntactic presentation). Hence, it should be possible to prune or freeze every infinite branch from some point on. The problem is to design such pruning rules so as to compute a finite derivation tree (hence, a finite complete set of unifiers) for every finitary unification problem of a syntactic equational theory.

Remark

The core of this problem has been solved [BC94].

References

[BC94]
Alexandre Boudet and Evelyne Contejean. “Syntactic” AC-unification. In Jean-Pierre Jouannaud, editor, First International Conference on Constraints in Computational Logics, volume 845 of Lecture Notes in Computer Science, pages 136–151, München, Germany, September 1994. Springer-Verlag.
[JK91]
Jean-Pierre Jouannaud and Claude Kirchner. Solving equations in abstract algebras: A rule-based survey of unification. In Jean-Louis Lassez and Gordon Plotkin, editors, Computational Logic: Essays in Honor of Alan Robinson. The MIT Press, 1991.
[Kir86]
Claude Kirchner. Computing unification algorithms. In First Symposium on Logic in Computer Science, pages 206–216, Cambridge, MA, June 1986. IEEE.

[Submit a comment] [RTALooP home] [Index] [Previous] [Next] [Postscript] [PDF] [BibTeX Source] [LaTeX Source]