Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The termination of Nielsen transformations applied to word equations with length constraints

Benjamin Przybocki, Clark Barrett

Abstract

Nielsen transformations form the basis of a simple and widely used procedure for solving word equations. We make progress on the problem of determining when this procedure terminates in the presence of length constraints. To do this, we introduce extended word equations, a mathematical model of a word equation with partial information about length constraints. We then define extended Nielsen transformations, which adapt Nielsen transformations to the setting of extended word equations. We provide a partial characterization of when repeatedly applying extended Nielsen transformations to an extended word equation is guaranteed to terminate.

The termination of Nielsen transformations applied to word equations with length constraints

Abstract

Nielsen transformations form the basis of a simple and widely used procedure for solving word equations. We make progress on the problem of determining when this procedure terminates in the presence of length constraints. To do this, we introduce extended word equations, a mathematical model of a word equation with partial information about length constraints. We then define extended Nielsen transformations, which adapt Nielsen transformations to the setting of extended word equations. We provide a partial characterization of when repeatedly applying extended Nielsen transformations to an extended word equation is guaranteed to terminate.
Paper Structure (15 sections, 40 theorems, 112 equations, 9 figures)

This paper contains 15 sections, 40 theorems, 112 equations, 9 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Extended word equations
  4. Extended Nielsen transformations
  5. Termination of extended Nielsen transformations
  6. The cut graph
  7. A sufficient condition for termination
  8. A necessary condition for termination
  9. The incoherent case
  10. The coherent case
  11. Miscellaneous propositions
  12. Applying a coherent extended Nielsen transformation
  13. Preserving acyclicity
  14. A sufficient condition for coherence
  15. Future directions

Key Result

Theorem 6.1

Let $(U_1,U_2,<)$ be a coherent extended word equation. If $G_{U_1,U_2,<}$ is acyclic, then $(U_1,U_2,<)$ is terminating. Furthermore, $(U_1,U_2,<)$ terminates after the application of at most $2^N$ coherent extended Nielsen transformations, where $N = |U_1| + |U_2|$.

Figures (9)

  • Figure 1: A representation of the word equation $(\mathit{XXY}, \mathit{ZWZ})$
  • Figure 2: An equivalent representation of the word equation $(\mathit{XXY}, \mathit{ZWZ})$
  • Figure 3: A problematic extended word equation
  • Figure 4: Three extended word equations
  • Figure 5: How an extended Nielsen transformation should behave in case I
  • ...and 4 more figures

Theorems & Definitions (103)

  • Example 1.1
  • Example 2.1
  • Definition 2.2
  • Definition 2.3
  • Definition 3.1
  • Definition 3.2
  • Definition 3.3
  • Definition 3.4
  • Example 4.1
  • Definition 4.2
  • ...and 93 more