Context Unification is in PSPACE

Jeż, Artur

doi:10.1007/978-3-662-43951-7_21

Item

ITEM ACTIONSEXPORT

Add to Basket

Local TagsRelease HistoryDetailsSummary

Released

Conference Paper

Context Unification is in PSPACE

MPS-Authors

/persons/resource/persons79297

Jeż, Artur
Algorithms and Complexity, MPI for Informatics, Max Planck Society;

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 (Eds.), 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.