# Item

ITEM ACTIONSEXPORT

Released

Conference Paper

#### Context Unification is in PSPACE

##### External Resource

No external resources are shared

##### Fulltext (restricted access)

There are currently no full texts shared for your IP range.

##### Fulltext (public)

There are no public fulltexts stored in PuRe

##### Supplementary Material (public)

There is no public supplementary material available

##### Citation

Jeż, A. (2014). Context Unification is in PSPACE. In J. Esparza, P. Fraigniaud, T.
Husfeldt, & E. Koutsoupias (*Automata, Languages,
and Programming* (pp. 244-255). Berlin: Springer. doi:10.1007/978-3-662-43951-7_21.

Cite as: https://hdl.handle.net/11858/00-001M-0000-0024-55A0-5

##### Abstract

Contexts are terms with one `hole', i.e. a place in which we can substitute an
argument.
In context unification we are given an equation over terms with variables
representing contexts
and ask about the satisfiability of this equation.
Context unification at the same time is subsumed by a second-order unification,
which is undecidable,
and subsumes satisfiability of word equations, which is in PSPACE.
We show that context unification is in PSPACE, so as word equations.
For both problems NP is still the best known lower-bound.
This result is obtained by an extension of the recompression technique,
recently developed by the author and used in particular
to obtain a new PSPACE algorithm for satisfiability of word equations, to
context unification.
The recompression is based on applying simple compression rules (replacing
pairs of neighbouring function symbols),
which are (conceptually) applied on the solution of the context equation and
modifying the equation in a way so that such
compression steps can be performed directly on the equation, without the
knowledge of the actual solution.