On Solving Word Equations via Program Transformation

TL;DR

This paper explores solving word equations by transforming and specializing an interpreter program, enabling the decision of solvability for certain classes of equations with overlapping variables.

Contribution

It introduces a novel approach of using program transformation and specialization techniques to decide the solvability of word equations.

Findings

Specialized interpreters can decide solvability for specific word equations.

Unfold/fold strategy effectively specializes interpreters for this purpose.

Method extends the capabilities of existing decision procedures.

Abstract

The paper presents an experiment of solving word equations via specialization of a configuration WE(R,E), where the program WE can be considered as an interpreter testing whether a composition of substitutions R produces a solution of a word equation E. Several variants of such interpreters, when specialized using a basic unfold/fold strategy, are able to decide solvability for a number of sets of the word equations with the overlapping variables.