[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 x ≈ s,x ≈ t ⇒ x ≈ s,s ≈ t 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]