[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |
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?)
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.
[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |