摘要：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.
