Recompression: New Approach to Word Equations and Context Unification (Invited Talk)

Author Artur Jez

Thumbnail PDF


  • Filesize: 272 kB
  • 3 pages

Document Identifiers

Author Details

Artur Jez

Cite AsGet BibTex

Artur Jez. Recompression: New Approach to Word Equations and Context Unification (Invited Talk). In 34th Symposium on Theoretical Aspects of Computer Science (STACS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 66, pp. 2:1-2:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


Word equations is given by two strings over disjoint alphabets of letters and variables and we ask whether there is a substitution that satisfies this equation. Recently, a new PSPACE solution to this problem was proposed, it is based on compressing simple substrings of the equation and modifying the equation so that such operations are sound. The analysis focuses on the way the equation is stored and changed rather than on the combinatorics of words. This approach greatly simplified many existing proofs and algorithms. In particular, unlike the previous solutions, it generalises to equations over contexts (known for historical reasons as context unification): contexts are terms with one special symbol that represent a missing argument and they can be applied on terms, in which case their argument replaces the special constant.
  • Word equations
  • exponent of periodicity
  • semantic unification
  • string unification
  • context unification
  • compression


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Hubert Comon. Completion of rewrite systems with membership constraints. Part I: Deduction rules. J. Symb. Comput., 25(4):397-419, 1998. URL:
  2. Hubert Comon. Completion of rewrite systems with membership constraints. Part II: Constraint solving. J. Symb. Comput., 25(4):421-453, 1998. URL:
  3. Warren D. Goldfarb. The undecidability of the second-order unification problem. Theor. Comput. Sci., 13:225-230, 1981. URL:
  4. Artur Jeż. Context unification is in PSPACE. In Elias Koutsoupias, Javier Esparza, and Pierre Fraigniaud, editors, ICALP, volume 8573 of LNCS, pages 244-255. Springer, 2014. full version at URL:
  5. Artur Jeż. Recompression: a simple and powerful technique for word equations. Journal of the ACM, 63(1):4:1-4:51, Feb 2016. URL:
  6. Gennadií Makanin. The problem of solvability of equations in a free semigroup. Matematicheskii Sbornik, 2(103):147-236, 1977. (in Russian). Google Scholar
  7. Wojciech Plandowski. Satisfiability of word equations with constants is in PSPACE. J. ACM, 51(3):483-496, 2004. URL:
  8. Manfred Schmidt-Schauß. Unification of stratified second-order terms. Internal Report 12/94, Johann-Wolfgang-Goethe-Universität, 1994. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail