[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |
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.
The core of this problem has been solved [BC94].
[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |