Word unification and transformation of generalized equations

Abstract

Makanin’s algorithm [Ma77] shows that it is decidable whether a word equation has a solution. The original description was hard to understmld and not designed for implementation. Since words represent a fundamental data type, various authors have given improved descriptions [Pé81, Ab87, Sc90, Ja90]. In this paper we present a version of the algorithm which probably cannot be further simplified without fundamentally new insights which exceed Makanin’s original ideas. We give a transformation rule which is efficient, conceptually simple and applies to arbitrary generalized equations. No further subprocedure is needed for search tree generation. In coutrast to our older work in [Sc90] the presentation wiU be based on Jaffar’s [Ja90] notion of generalized equations. We also prove that a combination of Plotkin’s algorithm (see [P172], also [LET21) and Ma’kanin’s algorithm offers a simple solution to the problem of terminating minimal mid complete word unification.