Affordable Access

On Equality Up-to Constraints over Finite Trees, Context Unification and One-Step Rewriting

Authors
  • Niehren, Joachim
  • Pinkal, Manfred
  • Ruhrberg, Peter
Publication Date
Jan 01, 1997
Source
HAL
Keywords
Language
English
License
Unknown
External links

Abstract

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 E*A*E* fragment of the theory of context unification is undecidable.

Report this publication

Statistics

Seen <100 times