de.mpg.escidoc.pubman.appbase.FacesBean
English
 
Help Guide Disclaimer Contact us Login
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Conference Paper

Context Unification is in PSPACE

MPS-Authors
http://pubman.mpdl.mpg.de/cone/persons/resource/persons79297

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

Locator
There are no locators available
Fulltext (public)
There are no public fulltexts available
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: http://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.