[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |
Originator: Jean-Pierre Jouannaud
Date: April 1995
Summary: Is unification of patterns modulo any set of variable-preserving equations decidable?
Unification of patterns (à la [Mil91]) modulo associativity and commutativity has been shown decidable [BC97], repairing the incomplete solution in [QW94]. Does it extend to equational theories whose axioms have the same set of variables on left and right hand side?
Date: Mon Jan 12 15:20:45 MET 1998
In his conference paper, Qian claimed that he has solved the problem of unifying patterns a la Miller modulo AC, but in fact he never succeeded to prove the completeness of his algorithm. Actually his algorithm is not complete, since he uses a first-order unification algorithm for pure AC-patterns as a black box. The problem was solved last year by Boudet and Contejean [BC97]: the case of pure AC-patterns requieres is handled in the same spirit as the first order case, by counting things, but technically this is not exactly identical. In [BC97], the proof of completeness of the algorithm is given. I must admit that [BC97] takes advantage of the paper of Qian, in particular, the remark that the equations of the form
λ x_{1} ... x_{n} F(x_{1},...,x_{n}) = λ x_{1} ... x_{n} F(x_{π(1)},...,x_{π(n)}) |
have an infinite set of solutions {σ_{1},σ_{2},...} such that σ_{i+1} is strictly more general than σ_{i}. This leads to the notion of constrained solution of a unification problem, and every unification problem of patterns with AC symbols admits a finite complete set of constrained unifiers, and the algorithm proposed in [BC97] computes such a set.
[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |