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

Problem #84

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?

Comment sent by Evelyne Contejean

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

λ x1 ... xn F(x1,...,xn) =  λ x1 ... xn 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.

References

[BC97]
Alexandre Boudet and Evelyne Contejean. AC-unification of higher-order patterns. In Gert Smolka, editor, Principles and Practice of Constraint Programming, volume 1330 of Lecture Notes in Computer Science, pages 267–281, Linz, Austria, October 1997. Springer-Verlag.
[Mil91]
Dale Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. In P. Schroeder-Heister, editor, Extensions of Logic Programming, volume 690 of Lecture Notes in Computer Science. Springer-Verlag, 1991.
[QW94]
Zheniu Qian and Kang Wang. Modular AC-unification of higher-order patterns. In Jean-Pierre Jouannaud, editor, First International Conference on Constraints in Computational Logics, volume 845 of Lecture Notes in Computer Science, pages 105–120, München, Germany, September 1994. Springer-Verlag.

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