Deciding Context Unification

In first-order term unification, variables represent well-formed terms over a given signature, and we are to solve equations built using function symbols from the signature and such variables; this problem is well-known to be decidable (in linear time). In second-order term unification, the variables take arguments (i.e., other terms) and a substitution uses those arguments an arbitrary number of times; for instance, an equation f(X(c),X(c)) = X(f(c,c)) has a solution X = •, where • is a special symbol denoting the place in which the argument is substituted. Under this substitution, both sides evaluate to f(c,c). There are other solutions, for instance X = f(•,•), which evaluates both sides tof(f(c,c),f(c,c)); in general, a solution that evaluates both sides to full binary tree of arbitrary height is easy to construct. Second-order unification is in general undecidable. Context unification is a natural problem in between first- and second-order unification—we deal with equations over terms, the variables take arguments, but we restrict the set of solutions: The argument is used exactly once. Formally, contexts are terms with exactly one occurrence of the special symbol • and in context unification, we are given an equation over terms with variables representing contexts and ask about the satisfiability of this equation. For instance, when the aforementioned equation f(X(c),X(c)) = X(f(c,c)) is treated as a context unification problem, then it has exactly one solution: X = •. Other substitutions that are solutions of it as an instance of the second-unification problem, say X = f(•, •), are not valid, as • is used more than once. Context unification also generalizes satisfiability of word equations, which is decidable (in PSPACE). The decidability status of context unification remained unknown for almost two decades. In this article, we show that context unification is in PSPACE (in EXPTIME, when tree regular constraints are also allowed). Those results are obtained by extending the recently developed recompression technique, which was previously defined for strings and used to obtain a new PSPACE algorithm for satisfiability of word equations. In this article, the technique is generalized to trees, and the corresponding algorithm is generalized from word equations to context unification. The idea of recompression is to apply simple compression rules (replacing pairs of neighboring function symbols) to the solution of the context equation; to this end, we appropriately modify the equation (without the knowledge of the actual solution) so compressing the solution can be simulated by compressing parts of the equation. It is shown that if the compression operations are appropriately chosen, then the size of the instance is polynomial during the whole algorithm, thus giving a PSPACE-upper bound.