LIPIcs.STACS.2017.2.pdf
- Filesize: 272 kB
- 3 pages
Document
Recompression: New Approach to Word Equations and Context Unification (Invited Talk)
Author
-
Part of:
Volume:
34th Symposium on Theoretical Aspects of Computer Science (STACS 2017)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Symposium on Theoretical Aspects of Computer Science (STACS) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2017-03-06
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)
https://doi.org/10.4230/LIPIcs.STACS.2017.2
https://doi.org/10.4230/LIPIcs.STACS.2017.2
Abstract
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.
Keywords
- Word equations
- exponent of periodicity
- semantic unification
- string unification
- context unification
- compression
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- Hubert Comon. Completion of rewrite systems with membership constraints. Part I: Deduction rules. J. Symb. Comput., 25(4):397-419, 1998. URL: http://dx.doi.org/10.1006/jsco.1997.0185.
- Hubert Comon. Completion of rewrite systems with membership constraints. Part II: Constraint solving. J. Symb. Comput., 25(4):421-453, 1998. URL: http://dx.doi.org/10.1006/jsco.1997.0186.
- Warren D. Goldfarb. The undecidability of the second-order unification problem. Theor. Comput. Sci., 13:225-230, 1981. URL: http://dx.doi.org/10.1016/0304-3975(81)90040-2.
- 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 http://arxiv.org/abs/1310.4367. URL: http://dx.doi.org/10.1007/978-3-662-43951-7_21.
- Artur Jeż. Recompression: a simple and powerful technique for word equations. Journal of the ACM, 63(1):4:1-4:51, Feb 2016. URL: http://dx.doi.org/10.1145/2743014.
-
Gennadií Makanin. The problem of solvability of equations in a free semigroup. Matematicheskii Sbornik, 2(103):147-236, 1977. (in Russian).
- Wojciech Plandowski. Satisfiability of word equations with constants is in PSPACE. J. ACM, 51(3):483-496, 2004. URL: http://dx.doi.org/10.1145/990308.990312.
-
Manfred Schmidt-Schauß. Unification of stratified second-order terms. Internal Report 12/94, Johann-Wolfgang-Goethe-Universität, 1994.