@conference {IIIA-2006-1250,
title = {Stratified Context Unification is NP-complete},
booktitle = {Lecture Notes in Computer Science},
volume = {4130},
year = {2006},
pages = {82-96},
publisher = {Springer-Verlag},
organization = {Springer-Verlag},
abstract = {Context Unification is the problem to decide for a given set of second-order equations $E$ where all second-order variables are unary, whether there exists a unifier, such that for every second-order variable X, the abstraction lambda x. r instantiated for X has exactly one occurrence of the bound variable x in r. Stratified Context Unification is a specialization where the nesting of second-order variables in E is restricted. It is already known that Stratified Context Unification is decidable, NP-hard, and in PSPACE, whereas the decidability and the complexity of Context Unification is unknown. We prove that Stratified Context Unification is in NP by proving that a size-minimal solution can be represented in a singleton tree grammar of polynomial size, and then applying a generalization of Plandowski{\textquoteright}s polynomial algorithm that compares compacted terms in polynomial time. This also demonstrates the high potential of singleton tree grammars for optimizing programs maintaining large terms. A corollary of our result is that solvability of rewrite constraints is NP-complete.},
author = {Jordi Levy and Manfred Schmidt-Schauss and Mateu Villaret}
}