On Equality Up-to Constraints over Finite Trees,
Context Unification and One-Step Rewriting
Author: Joachim Niehren and Manfred Pinkal and Peter Ruhrberg
Editor:
We introduce equality up-to constraints over finite trees
and investigate their expressiveness. Equality up-to
constraints subsume equality constraints, subtree constraints,
and one-step rewriting constraints.
We establish a close correspondence between
equality up-to constraints over finite trees and context unification.
Context unification subsumes string unification and is subsumed by
linear second-order unification. We obtain the following
three new results.
The satisfiability problem of equality up-to constraints is
equivalent to context unification, which is an open problem.
The positive existential fragment of the theory of one-step
rewriting is decidable. The $\exists^*\forall^*\exists^*$
fragment of the theory of context unification is undecidable.
|