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


Problem #39

Originator: Jean-Pierre Jouannaud
Date: April 1991

Summary: Can the application condition on the Merge rule in the computation of dag-solved forms of unification problems be improved?

Rules are given in [JK91] for computing dag-solved forms of unification problems in equational theories. The Merge rule xs,xtxs,st given there assumes that s is not a variable and its size is less than or equal to that of t. Can this condition be improved by replacing it with the condition that the rule Check* does not apply? (In other words, is Check* complete for finding cycles when Merge is modified as above?)

Remark

The problem has been solved by Hubert Comon [Com93] using an extended Check rule (requiring a congruence closure step). The original question—for whatever it may be worth—stands.

References

[Com93]
Hubert Comon. Personal communication, 1993.
[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, Cambridge, MA, 1991.

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