*A variant of the paper has also been published in [Akç18, AHN17, AIN17]. Some of the results reported here are a partial fulfillment of the Ph.D. requirements of the fourth author, and will be part of his dissertation.

#  On Problems Dual to Unification:
The String-Rewriting Case

Zümrüt Akçam  The College of Saint Rose, Albany, NY, US<EMAIL_ADDRESS>,
Daniel S. Hono II  University at Albany, SUNY
Albany, NY, US<EMAIL_ADDRESS>,  Paliath Narendran  University at Albany,
SUNY
Albany, NY, US<EMAIL_ADDRESS>and  Andrew Pulver  University at
Albany, SUNY
Albany, NY, US<EMAIL_ADDRESS>
###### Abstract.

In this paper, we investigate problems which are dual to the unification
problem, namely the Fixed Point (FP) problem, Common Term (CT) problem and the
Common Equation (CE) problem for string rewriting systems. Our main motivation
is computing fixed points in systems, such as loop invariants in programming
languages. We show that the fixed point (FP) problem is reducible to the
common term problem. Our new results are: (i) the fixed point problem is
undecidable for finite convergent string rewriting systems whereas it is
decidable in polynomial time for finite, convergent and dwindling string
rewriting systems, (ii) the common term problem is undecidable for the class
of dwindling string rewriting systems, and (iii) for the class of finite,
monadic and convergent systems, the common equation problem is decidable in
polynomial time but for the class of dwindling string rewriting systems,
common equation problem is undecidable.

###### Key words and phrases:

unification, convergent string-rewriting systems, fixed point problem, common
term problem, common equation problem, conjugacy problem, common multiplier
problem

Thanks to Dr. Daniel J. Dougherty for his feedback

## Introduction

Unification, with or without background theories such as associativity and
commutativity, is an area of great theoretical and practical interest. The
former problem, called _equational_ or _semantic_ unification, has been
studied from several different angles. Here we investigate some problems that
can clearly be viewed as _dual_ to the unification problem. Our main
motivation for this work is theoretical, but, as explained below, we begin
with a practical application that is shared by many fields.

In every major research field, there are variables or other parameters that
change over time. These variables are modified — increased or decreased — as a
result of a change in the environment. Computing _invariants,_ or expressions
whose values do not change under a transformation, is very important in many
areas such as Physics, e.g., invariance under the _Lorentz_ transformation.

In Computer Science, the issue of obtaining invariants arises in _axiomatic
semantics_ or _Floyd-Hoare semantics_ , in the context of formally proving a
loop to be correct. A _loop invariant_ is a condition, over the program
variables, that holds before and after each iteration. Our research is partly
motivated by the related question of finding expressions, called _fixed
points_ , whose values will be the same before and after each iteration, i.e.,
will remain unchanged as long as the iteration goes on. For instance, for a
loop whose body is

X = X + 2; Y = Y - 1;

the value of the expression X + 2Y is a fixed point.

We can formulate this problem in terms of properties of substitutions _modulo_
a term rewriting system. One straightforward formulation is as follows:

### Fixed Point Problem (FP)

Input:

A substitution $\theta$ and an equational theory $E$.

Question:

Does there exist a non-ground term $t\in T(Sig(E),\,{\mathcal{D}om}(\theta))$
such that $\theta(t)\,\approx_{E}t$?

Example 1: Suppose $E$ is a theory of integers which contains linear
arithmetic.
Let $\theta=\\{x\mapsto x-2,\,y\mapsto y+1\\}$ and we would like to find a
term $t$ such that $\theta(t)\approx_{E}t$. Note that $x+2y$ is such a term,
since

$\theta(x+2y)=(x-2)+2*(y+1)\approx_{E}x+2y$

Example 2: What is the fixed point/invariant of the given loop?

Algorithm 1 Fixed Point Loop

1: $\\{x=X_{0},y=Y_{0}\\}$

2:while do $x>0$

3: $x=x-1$ $\triangleright$ $\theta=\\{x\mapsto x-1,\;y\mapsto y+x-1\\}$

4: $y=y+x$

5:end while

Note that the value of the expression $y+\dfrac{x*(x-1)}{2}$ is unchanged,
since

  * •

Before Iteration: $y+\dfrac{x*(x-1)}{2}$

  * •

After Iteration:

$y+x-1+\dfrac{(x-1)*(x-2)}{2}=y+\dfrac{x^{2}-3x+2+2(x-1)}{2}=y+\dfrac{x*(x-1)}{2}$

Thus $y+\dfrac{x*(x-1)}{2}$ is a fixed point of $\theta$.

Note that fixed points may not be unique. Consider the term rewriting system

$\\{a(b(y))\rightarrow a(y),\;c(b(z))\rightarrow c(z)\\}$

and let $\theta=\\{x\mapsto b(x)\\}$. We can see that both $a(x)$ and $c(x)$
are fixed points of $\theta$.

We plan to explore two related formulations, both of which can be viewed as
_dual_ to the well-known unification problem. Unification deals with solving
symbolic equations: thus a typical input would be either two terms, say $s$
and $t$, or an equation $s\approx^{?}t$. The task is to find a substitution
such that $\theta(s)\approx\theta(t)$. For example, given two terms
$s_{1}=f(a,y)$ and $s_{2}=f(x,b)$, where $f$ is a binary function symbol, $a$
and $b$ are constants, and $x$ and $y$ are variables, the substitution
$\sigma=\\{x\mapsto a,~{}y\mapsto b\\}$ unifies $s_{1}$ and $s_{2}$, or
equivalently, $\sigma$ is a unifier for the equation $s_{1}=^{?}s_{2}$.

There are two ways to “dualize” the unification problem:

Common Term Problem (CT):

Input:

Two ground111This may not be strictly necessary. substitutions $\theta_{1}$
and $\theta_{2}$, and an equational theory $E$. (i.e.,
$\mathcal{V\\!R}\\!\mathit{an}(\theta_{1})=\emptyset$ and
$\mathcal{V\\!R}\\!\mathit{an}(\theta_{2})=\emptyset$ )

Question:

Does there exist a non-ground term $t\in
T(Sig(E),\,\mathcal{D}om(\theta_{1})\cup\mathcal{D}om(\theta_{2}))$ such that
$\theta_{1}(t)\,\approx_{E}\theta_{2}(t)$?

Example 3: Consider the two substitutions

$\theta_{1}=\\{x\mapsto p(a),\,y\mapsto p(b)\\}\textrm{ and
}\theta_{2}=\\{x\mapsto a,\,y\mapsto b\\}.$

If we take the term rewriting system $R_{1}^{lin}$ in the Appendix A as our
background equational theory $E$, then there exists a common term $t=x-y$ that
satisfies $\theta_{1}(t)\approx_{E}\theta_{2}(t)$.

$\theta_{1}(x-y)\approx_{E}p(a)-p(b)\approx_{E}a-b$

and

$\theta_{2}(x-y)\approx_{E}a-b$

Remark: We can easily show that the fixed point problem can be reduced to the
CT problem, as seen in Lemma 14 in Appendix A.

Common Equation Problem (CE):

Input:

Two substitutions $\theta_{1}$ and $\theta_{2}$ with the _same domain_ , and
an equational theory $E$.

Question:

Does there exist a non-ground, non-trivial $(t_{1}\not\approx_{E}t_{2})$
equation $t_{1}\approx^{?}t_{2}$, where
$t_{1},t_{2}\,\in\,T(Sig(E),\,\mathcal{D}om(\theta_{1}))$ such that both
$\theta_{1}$ and $\theta_{2}$ are _E_ -unifiers of $t_{1}\approx^{?}t_{2}$?

By trivial equations, we mean equations which are identities in the equational
theory $E$, i.e., an equation $s\approx_{E}^{?}t$ is trivial if and only if
$s\approx_{E}t$. We exclude this type of trivial equations in the formulation
of this question.

Example 4: Let $\,E~{}=~{}\\{p(s(x))\approx x,\;s(p(x))\approx x\\}$. Given
two substitutions

$\theta_{1}=\\{x_{1}\mapsto s(s(a)),\,x_{2}\mapsto s(a)\\}\textrm{ and
}\theta_{2}=\\{x_{1}\mapsto s(a),\,x_{2}\mapsto a\\},$

we can see that $\theta_{1}(t_{1})\approx_{E}\theta_{1}(t_{2})$ and
$\theta_{2}(t_{1})\approx_{E}\theta_{2}(t_{2})$, with the equation
$p(x_{1})\approx_{E}x_{2}$. However, there is no term $t$ on which the
substitutions agree, i.e., there aren’t any solutions for the common term
problem in this example. Thus, CT and CE problems are not equivalent as we
observe in the example above.

We explore the Fixed Point, Common Term and Common Equation problems in
_convergent_ string rewriting systems, more specifically in the subclass of
_dwindling_ string rewriting systems. Length-reducing and monadic string
rewriting systems are thoroughly investigated by [Ott86], [NOW84], [OND98],
[NO97].

Dwindling convergent systems are especially important because they are a
special case of _subterm-convergent theories_ which are widely used in the
field of protocol analysis [AC06, Bau05, CDK09, CD09]. Tools such as TAMARIN
prover [MSCB13] and YAPA [BCD09] use subterm-convergent theories since these
theories have nice properties (e.g., finite basis property [CR10]) and
decidability results [AC06].

In this document we will discuss (and survey) these three problems for
_convergent_ string rewriting systems. The current literature and our
discoveries are summarized in the Table 1, the _rectangle_ boxes indicating
_our own results_ :

| Convergent | Length-reducing | Dwindling | Monadic
---|---|---|---|---
FP | undecidable | NP-complete | P | P
CT | undecidable | undecidable | undecidable | P
CE | undecidable | undecidable | undecidable | P
Table 1. Complexity results of the problems in String Rewriting Systems.

## Definitions

We start by presenting some notation and definitions on term rewriting systems
and particularly string rewriting systems. Only some definitions are given in
here, but for more details, refer to the books [BN99] for term rewriting
systems and [BO93] for string rewriting systems.

A signature $\Sigma$ consists of finitely many ranked function symbols. Let
$X$ be a (possibly infinite) set of variables. The set of all terms over
$\Sigma$ and $X$ is denoted as $T(\Sigma,X)$. $\mathcal{V}\\!\mathit{ar}(t)$
shows the the set of variables for term $t$ and a term is a ground term iff
$\mathcal{V}\\!\mathit{ar}(t)=\emptyset$. The set of _ground terms_ , or terms
with no variables is denoted $T(\Sigma)$. A term rewriting system (TRS) is a
set of rewrite rules that are defined on the signature $\Sigma$, in the form
of $l\rightarrow r$, where $l$ and $r$ are called the left- and right-hand-
side (_lhs_ and _rhs_) of the rule, respectively. The rewrite relation induced
by a term rewriting system $R$ is denoted by $\rightarrow_{R}$. The reflexive
and transitive closure of $\rightarrow_{R}$ is denoted $\rightarrow_{R}^{*}$.
A TRS $R$ is called _terminating_ iff there is no infinite chain of terms. A
TRS $R$ is _confluent_ iff, for all terms $t$, $s_{1}$, $s_{2}$, if $s_{1}$
and $s_{2}$ can be derived from $t$, i.e.,
$s_{1}\leftarrow_{R}^{*}t\rightarrow_{R}^{*}s_{2}$, then there exists a term
$t^{\prime}$ such that
$s_{1}\rightarrow_{R}^{*}t^{\prime}\leftarrow_{R}^{*}s_{2}$. A TRS $R$ is
_convergent_ iff it is both terminating and confluent.

A term is _irreducible_ iff no rule of TRS $R$ can be applied to that term.
The set of terms that are irreducible modulo $R$ is defined by $IRR(R)$ and
also called as terms in their _normal form_ s. A term $t^{\prime}$ is said to
be an _R-normal form_ of a term $t$, iff it is irreducible and reachable from
$t$ in a finite number of steps; this is written as
$t\rightarrow_{R}^{!}t^{\prime}$. Let $t_{\downarrow}$ denote the normal form
of $t$ when $R$ is understood from the context.

String rewriting systems are a restricted class of term rewriting systems
where all functions are unary. These unary operators, that are defined by the
symbols of a string, applied in the order in which these symbols appear in the
string, i.e., if $g,h\in\Sigma$, the string $gh$ will be seen as the term
$h(g(x))$.222 It may be more common to view $gh$ as $g(h(x))$ with function
application done in the reverse order.  The set of all strings over the
alphabet $\Sigma$ is denoted by $\Sigma^{*}$ and the empty string is denoted
by the symbol $\lambda$. Thus the term rewriting system $\\{p(s(x))\rightarrow
x,\;s(p(x))\rightarrow x\\}$ is equivalent to the string-rewriting system

$\\{sp\rightarrow\lambda,\;ps\rightarrow\lambda\\}$

If $R$ is a string rewriting system (SRS) over alphabet $\Sigma$, then the
single-step reduction on $\Sigma^{*}$ can be written as:

For any $u,v\in\Sigma^{*}$, $u\rightarrow_{R}v$ iff there exists a rule
$l\rightarrow r\in R$ such that $u=xly$ and $v=xry$ for some
$x,y\in\Sigma^{*}$; i.e.,

${\rightarrow}_{R}\;=\;\\{(xly,\,xry)\;\mid\;(l\rightarrow r)\in
R,\,x,y\in{{\Sigma}^{*}}\\}$

For any string rewrite system $R$ over $\Sigma$, the set of all irreducible
strings, $IRR(R)$, is a regular language: in fact,
$IRR(R)=\Sigma^{*}\smallsetminus\\{\Sigma^{*}l_{1}\Sigma^{*}\,\cup...\cup\,\Sigma^{*}l_{n}\Sigma^{*}\\}$,
where $l_{1},\dots,l_{n}$ are the left-hand sides of the rules in $T$.

Throughout the rest of the paper, $a,b,c,\dots,h$ will denote elements of the
alphabet $\Sigma$, and $l,r,u,v,w,x,y,z$ will denote strings over $\Sigma$.
Concepts such as normal form, terminating, confluent, and convergent have the
same definitions in the string rewriting systems as they have for the term
rewriting systems. An SRS $T$ is called canonical if and only if it is
convergent and inter-reduced, i.e., no lhs is a substring of another lhs.

For a string $x\in\Sigma^{*}$, the element at position $i$ is denoted
$x_{[i]}$, and the substring from position $i$ to position $j$ (inclusive) is
denoted as $x_{[i:j]}$ where $i\leq j$ and this shall denote the empty string
when $i>j$. We will write $x_{[i:]}$ to denote $x_{[i:|x|]}$ when it
cumbersome to use $|x|$. Additionally, for an index sequence
$\beta=(\beta_{1},\beta_{2},\dots,\beta_{c})$, we use
$x_{[\beta]}:=x_{[\beta_{1}]}x_{[\beta_{2}]}\dots x_{[\beta_{c}]}$.
Parenthesized superscripts shall be a general way to index elements in a
sequence of strings e.g. $(x^{(1)},x^{(2)},x^{(3)},\dots)$.

A string rewrite system $T$ is said to be:

  * -

monadic iff the rhs of each rule in $T$ is either a single symbol or the empty
string, e.g., $abc\rightarrow b$.

  * -

dwindling iff, for every rule $l\rightarrow r$ in $T$, the rhs $r$ is a proper
prefix of its lhs $l$, e.g., $abc\rightarrow ab$.

  * -

_length-reducing_ iff $|l|>|r|$ for all rules $l\rightarrow r$ in $T$, e.g.,
$abc\rightarrow ba$.

$Monadic$Length-Reducing$Dwindling$ Figure 1. Some of the classes of String
Rewriting Systems 444The trivial forms of monadic rules such as $a\rightarrow
b$ can be ignored. We can get rid of such rules by changing every occurrence
of $a$ to $b$.

##  1\. Fixed Point Problem

Note that for string rewriting systems the fixed point problem is equivalent
to the following problem:

Input:

A string-rewriting system $R$ on an alphabet $\Sigma$, and a string
$\alpha\in\Sigma^{+}$.

Question:

Does there exist a string $W$ such that $\alpha
W\;\stackrel{{\scriptstyle*}}{{{\longleftrightarrow}_{R}}}\;W$?

Fixed Point Problem is a particular case of the Common Term Problem discussed
in the next section and is thus decidable in polynomial time for finite,
monadic and convergent string rewriting systems.

It is also a particular case of the _conjugacy problem_. Thus for finite,
length-reducing and convergent systems it is decidable in NP [NOW84]. The NP-
hardness proof in [NOW84] also applies in our particular case: thus the
problem is NP-complete for finite, length-reducing and convergent systems.

###  1.1. Fixed Point Problem for Finite and Convergent Systems:

Theorem 4 shows that fixed point problem is undecidable for finite and
convergent string rewriting systems.

######  Theorem 1.

The following problem is undecidable:

>   * Input:
>
> A non-looping, deterministic linear bounded automaton $\mathcal{M}$ that
> restores its input for _accepted_ strings.
>
>   * Question:
>
> Is $\mathcal{L(M)}$ empty?
>
>

######  Proof 1.1.

Suitably modifying the construction given in [Car91] in a straightforward way,
we can prove the undecidability of this problem with a reduction from the
well-known Post Correspondence Problem (PCP). Recall that an instance of PCP
is a collection of pairs of strings over an alphabet $\Sigma$ (“dominos” in
[Sip96]) and the question is if there exists a sequence of indices
$i_{1},i_{2},\ldots i_{n}$ such that $x_{i_{1}}x_{i_{2}}\ldots
x_{i_{n}}=y_{i_{1}}y_{i_{2}}\ldots y_{i_{n}}$. Alternatively, we can define
the PCP in terms of two homomorphisms $\psi$ and $\phi$ from
$C^{*}=\\{c_{1},\;\ldots\;c_{n}\\}^{*}$ to $\Sigma^{*}=\\{a,b\\}^{*}$. The
question now is whether there exists a non-empty string $m_{C}$ such that
$\psi(m_{C})=\phi(m_{C})$.

The reduction proof is done by validating the “solution string”
$w\in\Sigma^{*}$, for the two homomorphisms using the DLBA $\mathcal{M}$ with
the following configuration,
$\mathcal{M}=(Q,\Sigma,\Gamma,\delta,q_{0},q_{a},q_{r})$. Assume
$w=w_{1}\;w_{2}$ where $w_{1}\in C^{*}$ and $w_{2}\in\Sigma^{*}$.
$\mathcal{M}$ will check the correctness of $w$ by going over one symbol at a
time in the string $w_{1}$ and its corresponding mapping in $w_{2}$.
$\mathcal{M}$ uses a marking technique, marking the symbols $c_{i}$ and their
correct mappings with overlined symbols. If every letter in the string is
overlined, then clearly the string is “okay” according to the first
homomorphism; $\mathcal{M}$ will then replace the overlined letters with the
same non-overlined letters as before and repeat the same steps for the second
homomorphism. Thus the DLBA will accept and re-create $w_{1}\;w_{2}$ if and
only if it is a solution string. $\mathcal{L(M)}$ is empty if and only if the
instance of PCP has no solution.

We construct a string rewriting system $R$ from the above-mentioned DLBA
$\mathcal{M}$. The construction of $R$ is similar to the one in [BO84]. Let
$\mathcal{M}=(Q,\Sigma,\Gamma,\delta,q_{0},q_{a},q_{r})$. Here $\Sigma$
denotes the input alphabet, $\Gamma$ is the tape alphabet, $Q$ is the set of
states, $q_{0}\in Q$ is the initial state, $q_{a}\in Q$ the accepting state
and $q_{r}\in Q$ the rejecting state. We assume that the tape has two end-
markers: $\cent\in\Gamma$ denotes the left end-marker and $\$\in\Gamma$ is the
right end-marker. We also assume that on acceptance the DLBA comes to a halt
at the left-end of the tape. Finally, $\delta:Q\times\Gamma\rightarrow
Q\times\Gamma\times\\{L,R\\}$ is the transition function of $\mathcal{M}$.

The alphabet of $R$ is $\Gamma=\Sigma\cup\Sigma^{\prime}\cup Q$ where
$\Sigma^{\prime}$ is a replica of the alphabet $\Sigma$ such that
$\Sigma^{\prime}\cap\Sigma=\emptyset$. $R$ has the rules

$\displaystyle q_{i}\,a_{k}$ $\displaystyle\rightarrow a_{k}^{\prime}\,q_{j}$
$\displaystyle\text{if }(q_{i},a_{k},q_{j},R)\in\delta$ $\displaystyle
a_{l}^{\prime}\,q_{i}\,a_{k}$ $\displaystyle\rightarrow q_{j}\,a_{l}\,a_{k}$
$\displaystyle\text{for all }a_{l}^{\prime}\in\Sigma^{\prime}\text{, if
}(q_{i},a_{k},q_{j},L)\in\delta$ $\displaystyle q_{a}\,\cent$
$\displaystyle\rightarrow\cent$

Since the linear bounded automaton is deterministic, $R$ is locally confluent.
Besides, $\mathcal{M}$ ultimately always halts, and that means there will be
no infinite chain of rewrites for $R$, and thus $R$ is terminating.

######  Lemma 2.

$\mathcal{M}$ accepts $w$ iff
$q_{0}\,\cent\,w\,\$\rightarrow_{R}^{+}q_{a}\,\cent\,w\,\$$.

######  Proof 1.2.

By inspection of the rules we can see that $\mathcal{M}$ makes the transition
$u_{1}\,q_{1}\,v_{1}~{}\vdash_{M}~{}{u_{2}}\,q_{2}\,v_{2}$ if and only if
$u_{1}^{\prime}\,q_{1}\,v_{1}\rightarrow_{R}u_{2}^{\prime}\,q_{2}\,v_{2}$.

######  Lemma 3.

$\cent\,w\,\$$ is a fixed point for $q_{0}$ in $R$ iff $\mathcal{M}$ accepts
$w$.

######  Proof 1.3.

Suppose $\mathcal{M}$ accepts $w$. Observe that
$q_{0}\,\cent\,w\,\$\rightarrow_{R}^{+}q_{a}\,\cent\,w\,\$$ by Lemma 2, and
$R$ has the rule $q_{a}\,\cent\,\rightarrow\cent$. Thus we get
$q_{0}\,\cent\,w\,\$\rightarrow_{R}^{+}q_{a}\,\cent\,w\,\$\rightarrow\cent\,w\,\$$.

For the “only if” part, suppose $\cent\,w\,\$$ is a fixed point for $q_{0}$,
i.e., $q_{0}\,\cent\,w\,\$\rightarrow_{R}^{+}\cent\,w\,\$$. Now note that the
_only_ rule that can remove a state-symbol from a string is the rule
$q_{a}\,\cent\,\rightarrow\,\cent$. But once that rule is applied, no other
rules are applicable. Therefore, there must be a reduction sequence such that
$q_{0}\,\cent\,w\,\$\rightarrow_{R}^{+}q_{a}\,\cent\,w\,\$$. This proves that
$w$ is accepted by the DLBA $\mathcal{M}$.

######  Theorem 4.

The fixed point problem is undecidable for finite and convergent string
rewriting systems.

###  1.2. Fixed Point Problem for Dwindling Convergent Systems:

Given a string $\alpha\in\Sigma^{*}$ and a dwindling, convergent, and finite
string rewriting system $R$, does there exist a string $W\in\Sigma^{*}$ such
that $\alpha W\rightarrow^{!}_{R}W$?

It will be notationally convenient to characterize dwindling rewrite rules by
a 3-tuple containing the LHS, the length of the LHS, and the length of the
RHS. In other words, for a dwindling rule $\ell\rightarrow\ell_{1:e}\in R$
where $|\ell|=d$ and $1\leq e<d$, we have the tuple $(\ell,d,e)$.

######  Lemma 5.

Let $A\in\Sigma^{+}$ irreducible, $X\in\Sigma^{+}$, and $R$ dwindling,
convergent.
If $AX\rightarrow_{R}^{*}S$, then $S=A_{[1:b]}X_{[\beta]}$ for some $b\leq|A|$
and index sequence
$\beta=(\beta_{1},\beta_{2},\dots,\beta_{c})$ where
$1\leq\beta_{1}<\beta_{2}<\dots<\beta_{c}\leq|X|$. Additionally, $c<|X|$ if
$S\neq AX$.

######  Proof 1.4.

This result follows closely from the irreducibility of the individual strings
$A$ and $X$, and the nature of dwindling rules. Applying a dwindling rule to
$AX$ either removes a substring spanning the end of $A$ and the beginning of
$X$ or a substring of only $X$. The details are as follows:

We will prove Lemma 5 by showing for an arbitrary sequence of terms

$(S^{(0)},S^{(1)},\dots,S^{(n)})$

where $S^{(0)}=AX$ and $S^{(i-1)}\rightarrow_{R}S^{(i)}$, that for each string
$S^{(i)}$ there exists integer $b$ and index sequence $\beta$ such that
$S^{(i)}=A_{[1:b]}X_{[\beta]}$. Clearly, the result holds for $i=0$. Assume
the result holds for some $i=k$. Since for any $S^{(k)}:=A_{[1:b]}X_{[\beta]}$
where $A_{[1:b]}$ irreducible, if the LHS $\ell$ of any rewrite rule
$(\ell,d,e)$ matches $S^{(k)}_{[p:p+d]}$, we must have $b<p+d$. Therefore,
applying $(\ell,d,e)$ and obtaining $S^{(k+1)}$ we have

$\displaystyle S^{(k+1)}$
$\displaystyle=(A_{[1:b]}X_{[\beta]})_{[1:p+e]}(A_{[1:b]}X_{[\beta]})_{[p+d+1:]}$
(1)
$\displaystyle=(A_{[1:b]}X_{[\beta]})_{[1:\eta]}(A_{[1:b]}X_{[\beta]})_{[\eta+1:p+e]}(A_{[1:b]}X_{[\beta]})_{[p+d+1:]}$
(2)

where $\eta=min(p+e,b)$.

The first substring $(A_{[1:b]}X_{[\beta]})_{[1:\eta]}$ is a prefix of
$A_{[1:b]}$. The second substring
$(A_{[1:b]}X_{[\beta]})_{[\eta+1:p+e]}$ is the empty string if $p+e\leq b$ and
a prefix of $X_{[\beta]}$ otherwise. Finally,
$(A_{[1:b]}X_{[\beta]})_{[p+d+1:]}$ is a (strict) right-substring of
$X_{[\beta]}$. It is also clearly seen that
$|(A_{[1:b]}X_{[\beta]})_{[\eta+1:p+e]}(A_{[1:b]}X_{[\beta]})_{[p+d+1:]}|<|X_{[\beta]}|$

Note that there may be more than one decomposition $(b,\beta)$ for Lemma (5).
However, if one assigns unique labels to each character instance and considers
a specific sequence of rewrites where each application of a (dwindling) rule
“deletes” a substring, then there is a specific coresponding tuple
$(b,\beta)$. Unless otherwise stated we shall assume maximum $b$ in our
application of (5).

######  Lemma 6.

Assume $W$ is a minimal-length solution to an instance of the fixed point
problem $(\alpha,R)$ for irreducible $\alpha$ and dwindling, convergent string
rewriting system $R$. Then $W_{[1]}=\alpha_{[1]}$.

######  Proof 1.5.

Let $n=|W|$. We must have that $|(\alpha W)_{\downarrow}|=n$. By Lemma 5, we
have that $(\alpha W)_{\downarrow}=\alpha_{[1:b]}W_{[\beta]}$ for some
$b\leq|\alpha|$ and $1\leq\beta_{1}<\beta_{2}<\dots<\beta_{c}\leq|W|$ where
$c<|W|$. If $\alpha_{[1:b]}$ not empty, then $\alpha_{[1:b]}$ is a prefix of
$(\alpha W)_{\downarrow}$. Otherwise $|(\alpha W)_{\downarrow}|<n$ because
$|W_{[\beta]}|<n$, contradicting $n=|W|$.

######  Theorem 7.

Given an instance of the fixed point problem $(\alpha,R)$ where $R$ is a
dwindling, convergent rewrite system and $\alpha$ is in normal form we can
determine if solutions exist in polynomial time.

######  Proof 1.6.

Since $R$ is length-reducing and convergent, the length of a smallest solution
(if solutions exist) is bounded above by $2\cdot max(\\{|l|:(l\rightarrow
r)\in R\\})\cdot|\alpha|$ which follows from the results in [NO85] and that
the fixed point problem is a special case of the conjugacy problem. Let $n$ be
an upper bound on the length of minimal-length solutions.

From Lemma 6, $W_{[1]}=\alpha_{[1]}$. Suppose the first $j$ symbols of a
minimal-length solution $W$ are known. Define $\alpha^{(j)}:=(\alpha
W_{[1]}\dots W_{[j]})_{\downarrow}$. Then
$\alpha^{(j)}W_{[j+1:|W|]}\rightarrow_{R}^{!}W$, and so either $|W|=j$ and we
know all the symbols of $W$, or $|\alpha^{(j)}|>j$. Applying Lemma 5 to
$\alpha^{(j)}W_{[j+1:|W|]}$ by taking $A=\alpha^{(j)}$, $X=W_{[j+1:|W|]}$, we
have that its normal form $\alpha^{(j)}_{[1:b]}W_{[\beta]}$ must be such that
$|W_{[\beta]}|<|W_{[j+1:|W|]}|$ and so $\alpha^{(j)}_{[1:b]}$ is a prefix of
$\alpha^{(j)}$ with $b>j$. Thus, $W_{[j+1]}=\alpha^{(j)}_{[j+1]}$. If there is
a minimum-length solution, it will be found within $n$ iterations.

######  Theorem 8.

Complexity: If solutions exist, a minimal-length solution $W$ can be found in
$O(n\cdot|R|)$ time, where $n$ is the upper bound on the length of minimal-
length solutions for a given instance of the fixed point problem $(\alpha,R)$
and $R$ is a dwindling, convergent rewrite system. Otherwise, the algorithm
will terminiate in $O(n\cdot|R|)$ time.

######  Proof 1.7.

The procedure in Theorem 1 determines a minimal-length solution if it exists.
Since $\alpha^{(j)}$ can be defined recursively as: $\alpha^{(0)}=\alpha$,
$\alpha^{(j)}=(\alpha^{(j-1)}\alpha_{[j]}^{(j-1)})_{\downarrow}$, and
$\alpha^{(j-1)}$ is already in normal form, only one position needs to be
matched to check whether a rule in $R$ can be used to reduce
$\alpha^{(j-1)}\alpha_{[j]}^{(j-1)}$. Additionally, no more than one reduction
must be applied to fully reduce $\alpha^{(j-1)}\alpha_{[j]}^{(j-1)}$. At most
$|\alpha|<n$ rewrites need to be applied in total before $\alpha W$ is reduced
to $W$ or before the existence of a solution is ruled out by
$|\alpha^{(j)}|\leq j$. The overall time complexity is thus $O(n\cdot|R|)$.

######  Corollary 9.

If the RHS of each rule in $R$ is also of length $\leq 1$ (i.e. the cases
where $R$ is a dwindling convergent system that is also special or monadic),
then a minimal-length solution $W$ must be a prefix of $\alpha$.

######  Proof 1.8.

In this case, we have $e\in\\{0,1\\}$ for each application of a rule
$(\ell,d,e)$. Recall that in Lemma 5, if the LHS $\ell$ of any rewrite rule
$(\ell,d,e)$ matches $S^{(k)}_{[p:p+d]}$, then

$S^{(k+1)}=(A_{[1:b]}X_{[\beta]})_{[1:\eta]}(A_{[1:b]}X_{[\beta]})_{[\eta+1:p+e]}(A_{[1:b]}X_{[\beta]})_{[p+d+1:]}$

for $\eta:=min(p+e,b)$. In these cases, $p+e<\eta+1$ and so the middle
substring

$(\alpha_{[1:b]}W_{[\beta_{1},\beta_{2},\dots,\beta_{c}]})_{[\eta+1:p+e]}$

is empty. It follows that every string reachable from $\alpha W$ consists of a
prefix of $\alpha$ followed by a postfix of $W$, and so minimal-length
solutions must be a prefix of $\alpha$.

##  2\. Common Term Problem

Note that for string rewriting systems the common term problem is equivalent
to the following problem:

Input:

A string-rewriting system $R$ on an alphabet $\Sigma$, and two strings
$\alpha,\beta\in\Sigma^{*}$.

Question:

Does there exist a string $W$ such that $\alpha
W\;\stackrel{{\scriptstyle*}}{{{\longleftrightarrow}_{R}}}\;\beta W$?

This is also known as Common Multiplier Problem which has been shown to be
decidable in polynomial time for monadic and convergent string-rewriting
systems (see, e.g., [OND98], Lemma 3.7). However, the CT problem is
undecidable for convergent and length-reducing string rewriting systems in
general [Ott86].555 In fact, Otto et al. [OND98] showed that there is a
_fixed_ convergent length-reducing string rewriting system for which the CT
problem is undecidable.

In this section, we focus on the decidability of the CT problem for
_convergent and dwindling_ string rewriting systems.

###  2.1. Common Term Problem for Convergent and Dwindling Systems

We show that the CT (Common Term) problem is undecidable for string rewriting
systems that are dwindling and convergent. We define CT as the following
decision problem:

Given:

A finite, non-empty alphabet $\Sigma$, strings $\alpha,\beta\in\Sigma^{*}$ and
a dwindling, convergent string rewriting system $S$.

Question:

Does there exist a string $W\in\Sigma^{*}$ such that $\alpha W\approx_{S}\beta
W$?

Note that interpreting concatenation the other way, i.e., $ab$ as $a(b(x))$,
will make this a _unification_ problem.

We show that Generalized Post Correspondence Problem ($GPCP$) reduces to the
CT problem, where $GPCP$ stands for a variant of the modified post
correspondence problem such that we will provide the start and finish dominoes
in the problem instance. This slight change does not effect the decidability
of the problem in any way, i.e., $GPCP$ is also undecidable [EKR82, Nic08].

Given:

A finite set of tuples $\left\\{(x_{i},\;y_{i})\right\\}^{n+1}_{i=0}$ such
that each $x_{i},y_{i}\in\Sigma^{+}$, i.e., for all $i$, $|x_{i}|>0$,
$|y_{i}|>0$, and $(x_{0},y_{0}),(x_{n+1},y_{n+1})$ are the _start_ and _end_
dominoes, respectively.

Question:

Does there exist a sequence of indices $i_{1},\ldots,i_{k}$ such that

$x_{0}\;x_{i_{1}}\;\ldots\;x_{i_{k}}\;x_{n+1}=y_{0}\;y_{i_{1}}\;\ldots\;y_{i_{k}}\;y_{n+1}?$

We work towards showing that the CT problem defined above is undecidable by a
many-one reduction from $GPCP$. First, we show how to construct a string-
rewriting system that is dwindling and convergent from a given instance of
$GPCP$.

Let $\left\\{(x_{i},\;y_{i})\right\\}^{n}_{i=1}$ be the set of “intermediate”
dominoes and $(x_{0},y_{0}),(x_{n+1},y_{n+1})$, the start and end dominoes
respectively, be given. Suppose $\Sigma$ is the alphabet given in the instance
of $GPCP$. Without loss of generality, we may assume $\Sigma=\\{a,\,b\\}$.
Then set
$\hat{\Sigma}:=\\{a,b\\}\cup\\{c_{0},\;\ldots\;c_{n+1}\\}\cup\\{\cent_{1},\cent_{2},B,a_{1},a_{2},a_{3},b_{1},b_{2},b_{3}\\}$
which will be our alphabet for the instance of CT.

Next we define a set of string homomorphisms used to simplify the discussion
of the reduction. Namely, we have the following:

$\begin{aligned} h_{1}(a)&=&a_{1}\,a_{2}\,a_{3},\\\
h_{1}(b)&=&b_{1}\,b_{2}\,b_{3},\end{aligned}\qquad\begin{aligned}
h_{2}(a)&=&a_{1}\,a_{2},\\\
h_{2}(b)&=&b_{1}\,b_{2},\end{aligned}\qquad\begin{aligned} h_{3}(a)&=&a_{1}\\\
h_{3}(b)&=&b_{1}\end{aligned}$

such that each $h_{i}:\Sigma\rightarrow\hat{\Sigma}^{+}$ is a homomorphism.

Reduction and form of solution: For the convenience of the reader, we state
the form of the $CT$ problem instance and its solutions before explaining the
details. In particular, $\alpha=\cent_{1}$, $\beta=\cent_{2}$. For instances
such that a solution $Z$ exists, it shall take the form $h_{1}(Z_{1})Z_{2}$,
where $Z_{1}\in\\{a,b\\}^{+}$ is the string of the GPCP solution and
$Z_{2}=c_{n+1}Bc_{i_{k}}\dots Bc_{i_{1}}Bc_{0}$. The sequence
$c_{n+1},c_{i_{k}},\dots,c_{i_{1}},c_{0}$ is the (reversed) sequence of tuple
indices, that is, the GPCP solution itself, and they are separated by the
symbol $B$. Informally, the purpose of the homormorphisms and $\cent_{1}$,
$\cent_{2}$ is to ensure that $\alpha Z$ and $\beta Z$ are processed with two
separate sets of rules, corresponding to the sets of first and second tuple
(tile, if the reader prefers) elements, respectively.

We are now in a position to construct the string rewriting system $S$, with
the following collections of rules, named as the Class D rules:

$\begin{aligned} \cent_{1}h_{1}(a)&\rightarrow&\cent_{1}h_{3}(a),\\\
\cent_{1}h_{1}(b)&\rightarrow&\cent_{1}h_{3}(b),\end{aligned}\qquad\begin{aligned}
\cent_{2}h_{1}(a)&\rightarrow&\cent_{2}h_{2}(a)\\\
\cent_{2}h_{1}(b)&\rightarrow&\cent_{2}h_{2}(b)\end{aligned}$

and,

$\begin{aligned} h_{i}(a)\,h_{1}(a)&\rightarrow&h_{i}(a)\,h_{i}(a),\\\
h_{i}(b)\,h_{1}(a)&\rightarrow&h_{i}(b)\,h_{i}(a),\end{aligned}\qquad\begin{aligned}
h_{i}(a)\,h_{1}(b)&\rightarrow&h_{i}(a)\,h_{i}(b)\\\
h_{i}(b)\,h_{1}(b)&\rightarrow&h_{i}(b)\,h_{i}(b)\end{aligned}$

for $i\in\\{2,3\\}$.

The erasing rules of our system consists of three classes. Class i@ rules are
defined as:

$\displaystyle\cent_{1}\,h_{3}(x_{0})\,B\,c_{0}$ $\displaystyle\rightarrow$
$\displaystyle\lambda$ $\displaystyle\cent_{2}\,h_{2}(y_{0})\,c_{0}$
$\displaystyle\rightarrow$ $\displaystyle\lambda$

and Class ii@ rules (for each $i=1,2,\ldots,n$),

$\displaystyle h_{3}(x_{i})\,B\,c_{i}$ $\displaystyle\rightarrow$
$\displaystyle\lambda$ $\displaystyle h_{2}(y_{i})\,c_{i}\,B$
$\displaystyle\rightarrow$ $\displaystyle\lambda$

and finally Class iii@ rules,

$\displaystyle h_{3}(x_{n+1})\,c_{n+1}$ $\displaystyle\rightarrow$
$\displaystyle\lambda$ $\displaystyle h_{2}(y_{n+1})\,c_{n+1}\,B$
$\displaystyle\rightarrow$ $\displaystyle\lambda$

Clearly given an instance of $GPCP$ the above set of rules can effectively be
constructed from the instance data. Also, by inspection, we have that our
system is confluent (there are no overlaps among the left-hand sides of
rules), terminating, and dwindling.

We then set $\alpha=\cent_{1}$ and $\beta=\cent_{2}$ to complete the
constructed instance of $CT$ from $GPCP$.

It remains to show that this instance of $CT$ is a “yes” instance if and only
if the given instance of $GPCP$ is a “yes” instance, i.e., the $CT$ has a
solution if and only if the $GPCP$ does. In that direction, we prove some
results relating to $S$.

######  Lemma 10.

Suppose $\cent_{1}h_{3}(w_{1})B\gamma\rightarrow^{!}\lambda$ and
$\cent_{2}h_{2}(w_{2})\gamma\rightarrow^{!}\lambda$ for some
$w_{1},w_{2}\,\in\,\\{a,b\\}^{*}$, then
$\gamma\in\\{c_{1}B,\;c_{2}B,\;...\;,c_{n}B\\}^{*}c_{0}$.

######  Proof 2.9.

Suppose $\gamma$ is a minimal counter example with respect to length and
$\gamma\in IRR(R)$. In order for the terms to be reducible,
$\gamma=c_{i}B\;\gamma^{\prime}$ (this follows by inspection of $S$). After we
replace the $\gamma$ at the equation in the lemma, we get:

$\displaystyle\cent_{1}\;h_{3}(w_{1})\;B\;c_{i}\;B\;\gamma^{\prime}$
$\displaystyle\rightarrow$
$\displaystyle\cent_{1}{h_{3}(w_{1})}^{\prime}B\;\gamma^{\prime}\rightarrow^{!}\lambda$
$\displaystyle\cent_{2}\;h_{2}(w_{2})\;c_{i}\;B\;\gamma^{\prime}$
$\displaystyle\rightarrow$
$\displaystyle\cent_{2}{h_{2}(w_{2})}^{\prime}\;\gamma^{\prime}\rightarrow^{!}\lambda$

by applying the Class ii@ rules and finally Class i@ rule to erase the $\cent$
signs. Then, however, $\gamma^{\prime}$ is also a counterexample, and
$|\gamma^{\prime}|<|\gamma|$, which is a contradiction.

We are now in a position to state and prove the main result of this section.

######  Theorem 11.

The CT problem is undecidable for dwindling convergent string-rewriting
systems.

######  Proof 2.10.

We first complete the “only if” direction. Suppose CT has a solution such that
$\cent_{1}Z\downarrow\cent_{2}Z$ where $Z$ is a minimal solution. We show that
$Z$ corresponds to a solution for $GPCP$. Let $Z_{1}$ be the longest string
such that $h_{1}(Z_{1})$ is a prefix of $Z$, and denote the rest of $Z$ by
$Z_{2}$, so that $Z$ can be written $Z=h_{1}(Z_{1})Z_{2}$.

$h_{1}(Z_{1})$ can be rewritten to $h_{3}(Z_{1})$ and $h_{2}(Z_{1})$ by
applying the Class D rules. Thus, we will get

$\displaystyle\cent_{1}\;h_{1}(Z_{1})\;Z_{2}$ $\displaystyle\rightarrow^{*}$
$\displaystyle\cent_{1}h_{3}(Z_{1})\;Z_{2}$
$\displaystyle\cent_{2}\;h_{1}(Z_{1})\;Z_{2}$ $\displaystyle\rightarrow^{*}$
$\displaystyle\cent_{2}h_{2}(Z_{1})\;Z_{2}$

In order for terms to be reducible simultaneously, $Z_{2}$ must be of the form
$Z_{2}=c_{n+1}\;B\;Z_{2}^{\prime}$. Thus

$\displaystyle\cent_{1}\;h_{3}(Z_{1})\;Z_{2}$ $\displaystyle=$
$\displaystyle\cent_{1}h_{3}(Z_{1})\;c_{n+1}\;B\;Z_{2}^{\prime}$
$\displaystyle\cent_{2}\;h_{2}(Z_{1})\;Z_{2}$ $\displaystyle=$
$\displaystyle\cent_{2}h_{2}(Z_{1})\;c_{n+1}\;B\;Z_{2}^{\prime}$

i.e., $Z_{1}=Z_{1}^{\prime}\>x_{n+1}$ and
$Z_{1}=Z_{1}^{\prime\prime}\>y_{n+1}$. By applying the Class iii@ rules, these
equations will reduce to:

$\displaystyle\cent_{1}h_{3}(Z_{1})\;c_{n+1}\;B\;Z_{2}^{\prime}$
$\displaystyle\rightarrow$
$\displaystyle\cent_{1}h_{3}(Z_{1}^{\prime})\;B\;Z_{2}^{\prime}$
$\displaystyle\cent_{2}h_{2}(Z_{1})\;c_{n+1}\;B\;Z_{2}^{\prime}$
$\displaystyle\rightarrow$
$\displaystyle\cent_{2}h_{2}(Z_{1}^{\prime\prime})\;Z_{2}^{\prime}$

We now apply Lemma 10 to conclude that
$Z_{2}^{\prime}\in\\{c_{1}B,\;c_{2}B,\;\ldots,c_{n}B\\}^{*}c_{0}$.

At this point we have that:

$Z_{2}=c_{n+1}Bc_{i_{k}}Bc_{i_{k-1}}{\cdots}Bc_{i_{2}}Bc_{i_{1}}Bc_{0}\text{\>\>\>
for some }i_{1},\ldots,i_{k}$

Then the sequence of dominoes

$(x_{0},y_{0}),(x_{i_{1}},y_{i_{1}}),{\ldots},(x_{i_{k}},y_{i_{k}}),(x_{n+1},y_{n+1})$

will be a solution to the given instance of $GPCP$ with solution string
$Z_{1}$ since the left-hand sides of the Class i@, ii@, iii@ rules consist of
the images of domino strings under $h_{2}$ and $h_{3}$. More specifically,
there is a finite number of $B$’s and $c_{i}$’s in $Z_{2}$, so there must be a
decomposition of $h_{1}(Z_{1})$:

$h_{1}(Z_{1})=h_{1}(x_{0})h_{1}(x_{i_{1}})\cdots
h_{1}(x_{i_{k}})h_{1}(x_{n+1})$

and

$h_{1}(Z_{1})=h_{1}(y_{0})h_{1}(y_{i_{1}})\cdots
h_{1}(y_{i_{k}})h_{1}(y_{n+1})$

Thus, we have the following reductions with Class D rules:

$\cent_{1}\;h_{1}(Z_{1})\;Z_{2}\rightarrow^{*}\cent_{1}\;h_{3}(Z_{1})\;Z_{2}$
$\cent_{2}\;h_{1}(Z_{1})\;Z_{2}\rightarrow^{*}\cent_{2}\;h_{2}(Z_{1})\;Z_{2}$

Finally, by Class i@, ii@, iii@ rules:

$\cent_{1}\;h_{3}(Z_{1})\;Z_{2}\rightarrow^{*}\cent_{1}\;h_{3}(x_{0})\;B\;c_{0}\rightarrow\lambda$
$\cent_{2}\;h_{2}(Z_{1})\;Z_{2}\rightarrow^{*}\cent_{2}\;h_{2}(y_{0})\;c_{0}\rightarrow\lambda$

and $Z_{1}$ is a solution to the instance of the $GPCP$.

We next prove the “if” direction. Assume that the given instance of $GPCP$ has
a solution. Let $Z_{1}$ be the string corresponding to the matching dominoes,
and let

$(x_{0},y_{0}),(x_{i_{1}},y_{i_{1}}),{\ldots},(x_{i_{k}},y_{i_{k}}),(x_{n+1},y_{n+1})$

be the sequence of tiles that induces the match. Let
$Z_{2}=c_{n+1}Bc_{i_{k}}Bc_{i_{k-1}}{\cdots}Bc_{i_{2}}Bc_{i_{1}}Bc_{0}$. We
show that
$\cent_{1}h_{1}(Z_{1})Z_{2}\;\downarrow\;\cent_{2}h_{1}(Z_{1})Z_{2}$. First
apply the Class $D$ rules to get:

${\cent_{1}}h_{1}(Z_{1})Z_{2}\rightarrow^{*}{\cent_{1}}h_{3}(Z_{1})Z_{2}$
${\cent_{2}}h_{1}(Z_{1})Z_{2}\rightarrow^{*}{\cent_{2}}h_{2}(Z_{1})Z_{2}$

but then we can apply Class i@, ii@, iii@ rules to reduce both of the above
terms to $\lambda$.

This result strengthens the earlier undecidability result of Otto [Ott86] for
string-rewriting systems that are _length-reducing_ and convergent.

##  3\. Common Equation Problem

To clarify the CE problem for string rewriting systems, let us consider two
substitutions $\theta_{1}$ and $\theta_{2}$ such that

$\displaystyle\theta_{1}=\\{x_{1}\mapsto\alpha_{1},\;x_{2}\mapsto\alpha_{2}\\}$
$\displaystyle\theta_{2}=\\{x_{1}\mapsto\beta_{1},\;x_{2}\mapsto\beta_{2}\\}$

Think of the letters of the alphabet as monadic function symbols as mentioned
in the section of Definitions.We have two cases for the equation
$e_{1}=e_{2}$: (i) both $e_{1}$ and $e_{2}$ have the same variable in them, or
(ii) they have different variables, i.e., one has $x_{1}$ and the other
$x_{2}$. Thus in the former, which we call the “one-mapping” case, we are
looking for _different_ irreducible strings $W_{1}$ and $W_{2}$ such that
either

  1. (1)

$\alpha_{1}W_{1}\stackrel{{\scriptstyle*}}{{{\longleftrightarrow}_{R}}}\alpha_{1}W_{2}\;\text{
and
}\;\beta_{1}W_{1}\stackrel{{\scriptstyle*}}{{{\longleftrightarrow}_{R}}}\beta_{1}W_{2},\;\;\;\text{or}$

  2. (2)

$\alpha_{2}W_{1}\stackrel{{\scriptstyle*}}{{{\longleftrightarrow}_{R}}}\alpha_{2}W_{2}\;\text{
and
}\;\beta_{2}W_{1}\stackrel{{\scriptstyle*}}{{{\longleftrightarrow}_{R}}}\beta_{2}W_{2}$.

In the latter (“two-mappings case”) case, we want to find strings $W_{1}$ and
$W_{2}$, _not necessarily distinct,_ such that

$\alpha_{1}W_{1}\stackrel{{\scriptstyle*}}{{{\longleftrightarrow}_{R}}}\alpha_{2}W_{2}\;\text{
and
}\;\beta_{1}W_{1}\stackrel{{\scriptstyle*}}{{{\longleftrightarrow}_{R}}}\beta_{2}W_{2}$

The one-mapping case can be illustrated by an example. Consider the term
rewriting system $\\{a(a(b(z)))\,\rightarrow\,a(b(z))\\}$ and two
substitutions $\theta_{1}=\\{x\mapsto b(c)\\}$ and $\theta_{2}=\\{x\mapsto
b(b(c))\\}$. Now $a(a(x))\;=\;a(x)$ is a common equation. Considering this in
the string rewriting setting, we have $R~{}=~{}\\{baa\,\rightarrow\,ba\\}$,
$\alpha=b$ and $\beta=bb$. Now $W_{1}~{}=~{}aa$ and $W_{2}~{}=~{}a$ is a
solution.

Hence we define CE as the following decision problem:

Input:

A string-rewriting system $R$ on an alphabet $\Sigma$, and strings
$\alpha_{1},\alpha_{2},\beta_{1},\beta_{2}\in\Sigma^{*}$.

Question:

Do there exist _irreducible_ strings $W_{1},W_{2}\in\Sigma^{*}$ such that one
of the following conditions is satisfied?

i. |  $\alpha_{1}W_{1}\stackrel{{\scriptstyle*}}{{{\longleftrightarrow}_{R}}}\alpha_{2}W_{2}$, |  $\alpha_{1}\neq\alpha_{2}$ $\lor$ $\beta_{1}\neq\beta_{2}$
---|---|---
|
$\beta_{1}W_{1}\;\stackrel{{\scriptstyle*}}{{{\longleftrightarrow}_{R}}}\;\beta_{2}W_{2}$,
ii. |  $\alpha_{i}W_{1}\stackrel{{\scriptstyle*}}{{{\longleftrightarrow}_{R}}}\alpha_{i}W_{2}$, |  $i\in\\{1,2\\}$ $\land$ $W_{1}\neq W_{2}$
|
$\beta_{i}W_{1}\;\stackrel{{\scriptstyle*}}{{{\longleftrightarrow}_{R}}}\;\beta_{i}W_{2}$,

CE is also undecidable for dwindling systems, since in the string-rewriting
case CT is a particular case of CE. To see this, consider the case where
$\alpha_{1}\,\neq\,\alpha_{2}$ and $\beta_{1}=\beta_{2}=\lambda$, i.e.,
consider the substitutions

$\displaystyle\theta_{1}$ $\displaystyle=$
$\displaystyle\\{x_{1}\mapsto\alpha_{1},\;x_{2}\mapsto\alpha_{2}\\}$
$\displaystyle\theta_{2}$ $\displaystyle=$
$\displaystyle\\{x_{1}\mapsto\lambda,\;x_{2}\mapsto\lambda\\}$

where $\alpha_{1}\,\neq\,\alpha_{2}$. This has a solution if and only if there
are irreducible strings $W_{1},W_{2}\in\Sigma^{*}$ such that either

i. |  $\alpha_{1}W_{1}\stackrel{{\scriptstyle*}}{{{\longleftrightarrow}_{R}}}\alpha_{2}W_{2}$, |
---|---|---
|  $W_{1}\;\stackrel{{\scriptstyle*}}{{{\longleftrightarrow}_{R}}}\;W_{2}$, |  or
ii. |  $\alpha_{i}W_{1}\stackrel{{\scriptstyle*}}{{{\longleftrightarrow}_{R}}}\alpha_{i}W_{2}$, |  $i\in\\{1,2\\}$ $\land$ $W_{1}\neq W_{2}$
|  $W_{1}\;\stackrel{{\scriptstyle*}}{{{\longleftrightarrow}_{R}}}\;W_{2}$,

Since $W_{1}$ and $W_{2}$ are irreducible strings,
$W_{1}\;\stackrel{{\scriptstyle*}}{{{\longleftrightarrow}_{R}}}\;W_{2}$ makes
$W_{1}$ equal to $W_{2}$. Thus, we eliminate the second condition.

With the second condition being out of the picture, we only consider the first
condition which shows a similarity with the definition of Common Term(CT)
problem. The CE problem for $\theta_{1}$ and $\theta_{2}$ has a solution if
and only if the CT problem for $\alpha_{1}$ and $\alpha_{2}$ has a solution.
Therefore, CT is reducible to CE problem.

It can also be shown, using the construction from [NO97] that there are
theories for which CT is decidable whereas CE is not666We can use Corollary
4.4 on page 101 of [NO97]. In Appendix C, we provided a simpler construction
than the one in [NO97] for reader’s ease of understanding.

We now show that CE is decidable for monadic string rewriting systems. We
start by plunging into the _two-mappings_ case first, since the solution for
_one-mapping_ case is similar to the _two-mapping_ case with a slightly
simpler approach.

###  3.1. Two-mapping CE Problem for Monadic Systems

For monadic and convergent string rewriting systems, the _two-mappings_ case
of Common Equation (CE) problem is decidable. This can be shown using Lemma
3.6 in [OND98]. (See also Theorem 3.11 of [OND98].) In fact, the algorithm
runs in polynomial time as explained below:

######  Theorem 12.

Common Equation (CE) problem, given below, is decidable in polynomial time for
monadic, finite and convergent string rewriting systems.

Input:

A string-rewriting system $R$ on an alphabet $\Sigma$, and strings
$\alpha_{1},\alpha_{2},\beta_{1},\beta_{2}\in\Sigma^{*}$.

Question:

Do there exist strings $X,Y\in\Sigma^{*}$ such that
$\alpha_{1}X\;\stackrel{{\scriptstyle*}}{{{\longleftrightarrow}_{R}}}\;\alpha_{2}Y$
and
$\beta_{1}X\;\stackrel{{\scriptstyle*}}{{{\longleftrightarrow}_{R}}}\;\beta_{2}Y$?

######  Proof 3.11.

The CE problem is a particular case of the simultaneous E-unification problem
of [OND98], but with a slight difference: CE consists of _only two_ equations,
while simultaneous E-unification problem is defined for an arbitrary number of
equations. Besides, simultaneous E-unification problem is PSPACE-hard. We will
use their construction, but we will modify it to obtain our polynomial time
result.

Given a monadic, finite and convergent string rewriting system $R$ and
irreducible strings $x$ and $y$, let $RF(x,y)$ define the set of _right
factors_ needed to derive $y$, i.e.,

$RF(x,y)=\\{z\in IRR(R)~{}|~{}xz\rightarrow_{R}^{!}y\\}.$

$RF(x,y)$ is a regular language for all $x$, $y$ [OND98] and a DFA for it can
be constructed in time polynomial in $|R|$, $|x|$ and $|y|$. We can
characterize the solutions of the equation
$\alpha_{1}X\;\downarrow_{R}\;\alpha_{2}Y$ by an analysis similar to that used
in Lemma 3.6 of [OND98] and its proof. Since $R$ is monadic, there exist
$a,b\in\Sigma\cup\\{\lambda\\}$ and partitions of the strings
$\alpha_{1}={\alpha_{11}}\;{\alpha_{12}}$,
$\alpha_{2}={\alpha_{21}}\;{\alpha_{22}}$, $X={X_{1}}\;{X_{2}}$ and
$Y={Y_{1}}\;{Y_{2}}$, such that

|  $\alpha_{12}X_{1}\;\rightarrow^{!}\;a$,
---|---
|  $\alpha_{22}Y_{1}\;\rightarrow^{!}\;b,\qquad$ and
|  ${\alpha_{11}}\;a\;{X_{2}}={\alpha_{21}}\;b\;{Y_{2}}$.

Now there are 2 main cases:

  * (a)

${X_{2}}$ is a suffix of ${Y_{2}}$:
${Y_{2}}=Z\;{X_{2}}$
${\alpha_{11}}\;a={\alpha_{21}}\;b\;Z$ $RF({\alpha_{12}},a)\times
RF({\alpha_{22}},b)\cdot Z$

  * (b)

${Y_{2}}$ is a proper suffix of ${X_{2}}$:
${X_{2}}=Z^{\prime\prime}\;{Y_{2}}$
${\alpha_{11}}\;a\;Z^{\prime\prime}={\alpha_{21}}b$
${\alpha_{11}}\;a\;U={\alpha_{21}}$, $\;Z^{\prime\prime}=U\,b$
$RF({\alpha_{12}},a)\cdot Z^{\prime\prime}\times RF({\alpha_{22}},b)$

Similar partitioning can be done for the second equation.

Let $Sol(\alpha_{1},\alpha_{2})$ stand for a set of ‘minimal’ solutions:

$\displaystyle Sol(\alpha_{1},\alpha_{2})\;=$
$\displaystyle\;\;\;\;\,\bigcup_{\begin{subarray}{c}a,b\;\in\;\Sigma\;\cup\;\\{\lambda\\}\\\\[3.0pt]
{\alpha_{11}a}={\alpha_{21}}\,b\,Z\end{subarray}}RF({\alpha_{12}},a)\;\mathbin{\leavevmode\hbox
to6.89pt{\vbox to6.89pt{\pgfpicture\makeatletter\hbox{\hskip
0.43056pt\lower-0.43056pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{}\pgfsys@setlinewidth{0.86111pt}\pgfsys@invoke{ }{}{{}}{} {}{}{}{{}}{}
{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{6.02776pt}{6.02776pt}\pgfsys@moveto{0.0pt}{6.02776pt}\pgfsys@lineto{6.02776pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\;RF({\alpha_{22}},b)\cdot
Z\;$
$\displaystyle\cup\bigcup_{\begin{subarray}{c}a,b\;\in\;\Sigma\;\cup\;\\{\lambda\\}\\\\[3.0pt]
{\alpha_{21}b}={\alpha_{11}}\,a\,Z^{\prime\prime}\end{subarray}}RF({\alpha_{12}},a)\cdot
Z^{\prime\prime}\;\mathbin{\leavevmode\hbox to6.89pt{\vbox
to6.89pt{\pgfpicture\makeatletter\hbox{\hskip 0.43056pt\lower-0.43056pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{}\pgfsys@setlinewidth{0.86111pt}\pgfsys@invoke{ }{}{{}}{} {}{}{}{{}}{}
{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{6.02776pt}{6.02776pt}\pgfsys@moveto{0.0pt}{6.02776pt}\pgfsys@lineto{6.02776pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\;RF({\alpha_{22}},b)$

Note that this is a finite union of cartesian products of regular languages.
More precisely, it is an expression of the form

$(L_{11}\mathbin{\leavevmode\hbox to6.89pt{\vbox
to6.89pt{\pgfpicture\makeatletter\hbox{\hskip 0.43056pt\lower-0.43056pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{}\pgfsys@setlinewidth{0.86111pt}\pgfsys@invoke{ }{}{{}}{} {}{}{}{{}}{}
{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{6.02776pt}{6.02776pt}\pgfsys@moveto{0.0pt}{6.02776pt}\pgfsys@lineto{6.02776pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}L_{12})\;\cup\;\ldots\;\cup\;(L_{m1}\mathbin{\leavevmode\hbox
to6.89pt{\vbox to6.89pt{\pgfpicture\makeatletter\hbox{\hskip
0.43056pt\lower-0.43056pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{}\pgfsys@setlinewidth{0.86111pt}\pgfsys@invoke{ }{}{{}}{} {}{}{}{{}}{}
{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{6.02776pt}{6.02776pt}\pgfsys@moveto{0.0pt}{6.02776pt}\pgfsys@lineto{6.02776pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}L_{m2})$

where $m$ is a polynomial over $|\alpha_{1}|$, $|\alpha_{2}|$ and $|\Sigma|$
and each $L_{ij}$ has a DFA of size polynomial in $|R|$ and
$\text{max}(|\alpha_{1}|,\,|\alpha_{2}|)$.
To find the complexity of a DFA concatenation with a letter or string, check
the Lemma 15 for the former and Lemma 16 for the latter.

The set of all solutions for the equation
$\alpha_{1}X\;\downarrow_{R}\;\alpha_{2}Y$ is

$\Delta(\alpha_{1},\alpha_{2})~{}=~{}\left\\{\vphantom{b^{b}}\,(w_{1}x_{1},\,z_{1}x_{1})~{}\;|\;~{}(w_{1},z_{1})\in
Sol(\alpha_{1},\alpha_{2})\text{ and }x_{1}\in IRR(R)\right\\}$

The minimal solutions for the second equation with $\beta_{1}$ and
$\beta_{2}$, $Sol(\beta_{1},\beta_{2})$, can be found by following the same
steps. Thus $Sol(\beta_{1},\beta_{2})$ can also be expressed as the union of
cartesian products of regular languages:

$(L_{11}^{\prime}\mathbin{\leavevmode\hbox to6.89pt{\vbox
to6.89pt{\pgfpicture\makeatletter\hbox{\hskip 0.43056pt\lower-0.43056pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{}\pgfsys@setlinewidth{0.86111pt}\pgfsys@invoke{ }{}{{}}{} {}{}{}{{}}{}
{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{6.02776pt}{6.02776pt}\pgfsys@moveto{0.0pt}{6.02776pt}\pgfsys@lineto{6.02776pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}L_{12}^{\prime})\;\cup\;\ldots\;\cup\;(L_{n1}^{\prime}\mathbin{\leavevmode\hbox
to6.89pt{\vbox to6.89pt{\pgfpicture\makeatletter\hbox{\hskip
0.43056pt\lower-0.43056pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{}\pgfsys@setlinewidth{0.86111pt}\pgfsys@invoke{ }{}{{}}{} {}{}{}{{}}{}
{}{}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{6.02776pt}{6.02776pt}\pgfsys@moveto{0.0pt}{6.02776pt}\pgfsys@lineto{6.02776pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}L_{n2}^{\prime})$

where $n$ is also a polynomial over $|\beta_{1}|$, $|\beta_{2}|$ and
$|\Sigma|$. The set of all solutions for $\beta_{1}X=\beta_{2}Y$ equals to

$\Delta(\beta_{1},\beta_{2})~{}=~{}\left\\{\vphantom{b^{b}}\,(w_{2}x_{2},\,z_{2}x_{2})~{}\;|\;~{}(w_{2},z_{2})\in
Sol(\beta_{1},\beta_{2})\text{ and }x_{2}\in IRR(R)\right\\}$

The solutions for both the equations are the tuples
$(w,z)\in\;\Delta(\alpha_{1},\alpha_{2})\;\cap\;\Delta(\beta_{1},\beta_{2})$.
That is, there must be $w_{1},\;w_{2},\;z_{1},\;z_{2},\;x_{1},\;x_{2}$ such
that

$(w_{1},\;z_{1})\in Sol(\alpha_{1},\alpha_{2}),(w_{2},\;z_{2})\in
Sol(\beta_{1},\beta_{2})\text{ and}$ $\displaystyle w$
$\displaystyle=w_{1}\;x_{1}=w_{2}\;x_{2}$ $\displaystyle z$
$\displaystyle=z_{1}\;x_{1}=z_{2}\;x_{2}$

If $x_{1}$ is a suffix of $x_{2}$, i.e., $x_{2}={x_{2}}^{\prime}x_{1}$, then

$\displaystyle w_{1}$ $\displaystyle=w_{2}\;{x_{2}}^{\prime}$ $\displaystyle
z_{1}$ $\displaystyle=z_{2}\;{x_{2}}^{\prime}$

(Similarly we repeat the same steps when $x_{2}$ is a suffix of $x_{1}$.)

Recall that $(w_{1},\;z_{1})\in L_{i1}\times L_{i2}$ for some $i>0$, and
$(w_{2},\;z_{2})\in L_{j1}^{\prime}\times L_{j2}^{\prime}$ for some $j>0$.
Thus $x_{2}^{\prime}\;\in\;L_{i1}\,\backslash\,L_{j1}^{\prime}$ and
$x_{2}^{\prime}\;\in\;L_{i2}\,\backslash\,L_{j2}^{\prime}$ where $\backslash$
stands for the left quotient operation on languages, defined as $A\backslash
B:=\\{v\in\Sigma^{*}~{}|~{}\exists u\in B:uv\in A\\}$ (See Lemma 17 for more
detail). Thus there is a solution if the intersection of
$L_{i1}\,\backslash\,L_{j1}^{\prime}$ and
$L_{i2}\,\backslash\,L_{j2}^{\prime}$ is nonempty. This check has to be
repeated for every $i,\,j$. The process of finding the intersection of two
languages is explained in Lemma 18 and to be able to find the strings in the
intersection and the quotient, you need to follow the steps in Lemma 19.

###  3.2. One-mapping CE Problem for Monadic Systems

One-mapping case of the CE problem is decidable for monadic and convergent
string rewriting systems. We can show it using a construction similar to the
two-mappings case. However it will be a slightly simpler approach since we
only have two input strings $\alpha$ and $\beta$ as opposed to four. The
algorithm for the one-mapping case also runs in polynomial time as explained
below:

######  Theorem 13.

The following CE problem is decidable in polynomial time for monadic, finite
and convergent string rewriting systems.

Input:

A string-rewriting system $R$ on an alphabet $\Sigma$, and irreducible strings
$\alpha,\beta\in\Sigma^{*}$.

Question:

Do there exist distinct irreducible strings $X,Y\in IRR(R)$ such that

  1. $\alpha X\downarrow_{R}\alpha Y\;\text{ and }\;\beta X\downarrow_{R}\beta Y$?

######  Proof 3.12.

This follows from Lemma 27, since we only need to check whether there are
strings $X^{\prime},Y^{\prime},V,\gamma_{1},\gamma_{2}$ such that
$X^{\prime}\text{ and }Y^{\prime}$ are distinct, $\gamma_{1}\text{ and
}\gamma_{2}$ belong to $MP(\alpha)\text{ and }MP(\beta)$ respectively, and one
of the following symmetric cases hold:

  1. (a)

$X^{\prime}V,\,Y^{\prime}V\,\in\,RF(\alpha,\gamma_{1})$ _and_

  2. (b)

$X^{\prime},\,Y^{\prime}\,\in\,RF(\beta,\gamma_{2})$

or

  1. (c)

$X^{\prime},\,Y^{\prime}\,\in\,RF(\alpha,\gamma_{1})$ _and_

  2. (d)

$X^{\prime}V,\,Y^{\prime}V\,\in\,RF(\beta,\gamma_{2})$

First of all there are only polynomially many strings in $MP(\alpha)$ and
$MP(\beta)$. The two cases can be checked in polynomial time by Lemma 19.

##  4\. Future Work

For the sake of brevity (and clarity), we only discussed string rewriting
systems in this paper. Our future work will include the investigation of these
two problems for general term rewriting systems.

## References

  * [AC06] Martín Abadi and Véronique Cortier.  Deciding knowledge in security protocols under equational theories.  Theoretical Computer Science, 367(1-2):2–32, 2006.
  * [AHN17] Zümrüt Akçam, II Hono, Daniel S., and Paliath Narendran.  On Problems Dual to Unification.  arXiv e-prints, page arXiv:1706.05607, June 2017.
  * [AIN17] Zümrüt Akçam, Daniel S. Hono II, and Paliath Narendran.  On problems dual to unification.  In Adrià Gascón and Christopher Lynch, editors, Informal Proceedings of the 31st International Workshop on Unification (UNIF 2017), 2017.  https://unif-workshop.github.io/UNIF2017/.
  * [Akç18] Zümrüt Akçam.  On Problems Dual to Unification: The String-Rewriting Case.  PhD thesis, State University of New York at Albany, ProQuest, 2018.
  * [Bau05] Mathieu Baudet.  Deciding security of protocols against off-line guessing attacks.  In Proceedings of the 12th ACM Conference on Computer and Communications Security, CCS ’05, pages 16–25, New York, NY, USA, 2005. ACM.
  * [BCD09] Mathieu Baudet, Véronique Cortier, and Stéphanie Delaune.  YAPA: A Generic Tool for Computing Intruder Knowledge.  Springer Berlin Heidelberg, Berlin, Heidelberg, 2009.
  * [BN99] Franz Baader and Tobias Nipkow.  Term Rewriting and All That.  Cambridge University Press, 1999.
  * [BO84] Günther Bauer and Friedrich Otto.  Finite complete rewriting systems and the complexity of the word problem.  Acta Informatica, 21(5):521–540, 1984.
  * [BO93] Ronald V Book and Friedrich Otto.  String-rewriting systems.  Springer, 1993.
  * [Car91] Anne-Cécile Caron.  Linear bounded automata and rewrite systems: Influence of initial configurations on decision properties.  In TAPSOFT’91, pages 74–89. Springer, 1991.
  * [CD09] V. Cortier and S. Delaune.  A method for proving observational equivalence.  In 2009 22nd IEEE Computer Security Foundations Symposium, pages 266–276, July 2009.
  * [CDK09] Ştefan Ciobâcă, Stéphanie Delaune, and Steve Kremer.  Computing Knowledge in Security Protocols under Convergent Equational Theories.  Springer Berlin Heidelberg, Berlin, Heidelberg, 2009.
  * [CR10] Yannick Chevalier and Michaël Rusinowitch.  Compiling and securing cryptographic protocols.  Information Processing Letters, 110(3):116–122, 2010.
  * [EKR82] Andrzej Ehrenfeucht, Juhani Karhumäki, and Grzegorz Rozenberg.  The (Generalized) Post Correspondence Problem with lists consisting of two words is decidable.  Theoretical Computer Science, 21:119–144, 1982.
  * [HMU03] John E. Hopcroft, Rajeev Motwani, and Jeffrey D. Ullman.  Introduction to automata theory, languages, and computation - international edition (2. ed).  Addison-Wesley, 2003.
  * [KSZ86] Deepak Kapur, G. Sivakumar, and Hantao Zhang.  RRL: A rewrite rule laboratory.  In Jörg H. Siekmann, editor, 8th International Conference on Automated Deduction, pages 691–692, Berlin, Heidelberg, 1986. Springer Berlin Heidelberg.
  * [MSCB13] Simon Meier, Benedikt Schmidt, Cas Cremers, and David Basin.  The TAMARIN Prover for the Symbolic Analysis of Security Protocols.  Springer Berlin Heidelberg, Berlin, Heidelberg, 2013.
  * [Nic08] François Nicolas.  (Generalized) Post Correspondence Problem and semi-Thue systems.  CoRR, abs/0802.0726, 2008.
  * [NO85] Paliath Narendran and Friedrich Otto.  Complexity results on the conjugacy problem for monoids.  Theoretical Computer Science, 35:227–243, 1985.
  * [NO97] Paliath Narendran and Friedrich Otto.  Single versus simultaneous equational unification and equational unification for variable-permuting theories.  J. Autom. Reasoning, 19(1):87–115, 1997.
  * [NOW84] Paliath Narendran, Friedrich Otto, and Karl Winklmann.  The uniform conjugacy problem for finite Church-Rosser Thue systems is NP-complete.  Information and Control, 63(1/2):58–66, 1984.
  * [OND98] Friedrich Otto, Paliath Narendran, and Daniel J. Dougherty.  Equational unification, word unification, and 2nd-order equational unification.  Theoretical Computer Science, 198(1-2):1–47, 1998.
  * [Ott86] Friedrich Otto.  On two problems related to cancellativity.  Semigroup Forum, 33(1):331–356, 1986.
  * [Sip96] Michael Sipser.  Introduction to the Theory of Computation.  International Thomson Publishing, 1st edition, 1996.

##  Appendix A Appendix

The following term rewriting system $R_{1}^{{lin}}$ specifies a fragment of
linear arithmetic using _successor_ and _predecessor_ operators:

$\displaystyle x-0$ $\displaystyle\rightarrow$ $\displaystyle x$
$\displaystyle x-x$ $\displaystyle\rightarrow$ $\displaystyle 0$
$\displaystyle s(x)-y$ $\displaystyle\rightarrow$ $\displaystyle s(x-y)$
$\displaystyle p(x)-y$ $\displaystyle\rightarrow$ $\displaystyle p(x-y)$
$\displaystyle x-p(y)$ $\displaystyle\rightarrow$ $\displaystyle s(x-y)$
$\displaystyle x-s(y)$ $\displaystyle\rightarrow$ $\displaystyle p(x-y)$
$\displaystyle p(s(x))$ $\displaystyle\rightarrow$ $\displaystyle x$
$\displaystyle s(p(x))$ $\displaystyle\rightarrow$ $\displaystyle x$

We checked convergence of these rules on RRL (Rewrite Rule Laboratory)
[KSZ86].

######  Lemma 14.

The fixed point problem is reducible to the common term problem.

######  Proof A.13.

Let $\theta_{2}$ be the identity substitution. Assume that the fixed point
problem has a solution, i.e., there exists a term $t$ such that
$\theta(t)\,\approx_{E}t$. Then the CT problem for $\theta$ and $\theta_{2}$
has a solution since $\theta_{2}(t)\approx_{E}t$ (because $\theta_{2}(s)=s$
for all $s$). The “only if” part is trivial, again because $\theta_{2}(s)=s$
for all $s$.

Alternatively, suppose that $\mathcal{D}om(\theta)$ consists of $n$ variables,
where $n\geq 1$. If we map all the variables in
$\mathcal{V\\!R}\\!\mathit{an}(\theta)$ to new constants, this will create a
ground substitution

$\theta_{1}=\\{x_{1}\mapsto a_{1},\;x_{2}\mapsto a_{2},\;...,\;x_{n}\mapsto
a_{n}\\}.$

$\theta_{1}$ will be the one of the substitutions for the CT problem. The
other substitution, $\theta_{2}$, is the composition of the substitutions
$\theta$ and $\theta_{1}$. The substitution $\theta_{1}$ will replace all of
the variables in $\mathcal{V\\!R}\\!\mathit{an}(\theta)$ with the new
constants, thus making $\theta_{2}$ a ground substitution. Now if
$\theta(t)\,\approx_{E}\,t$, then
$\theta_{2}(t)=\theta_{1}(\theta(t))\approx_{E}\theta_{1}(t)$; in other words,
$t$ is a solution to the common term problem.

The “only if” part can also be explained in terms of the composition above.
Suppose that $\theta_{1}(s)$ and $\theta_{2}(s)$ are equivalent, i.e.,
$\theta_{1}(s)\,\approx_{E}\,\theta_{2}(s)$ for some $s$. Since
$\theta_{2}=\theta_{1}\circ\theta$, the equation can be rewritten as
$\theta_{1}(\theta(s))\approx_{E}\theta_{1}(s)$. Since
$a_{1},\,\ldots,\,a_{n}$ are new constants and are not included in the
signature of the theory, for all $t_{1}$ and $t_{2}$,
$\theta_{1}(t_{1})\,\approx_{E}\theta_{1}(t_{2})$ holds if and only if
$t_{1}\approx_{E}t_{2}$ (See [BN99], Section 4.1, page 60) Thus
$\theta_{1}(\theta(s))\approx_{E}\theta_{1}(s)$ implies that
$\theta(s)\approx_{E}s$, making $s$ a fixed point.

##  Appendix B Appendix

######  Lemma 15.

Let $\,M\;=\;(Q,\Sigma,\delta,q_{0},F)$ be a DFA and $a\in\Sigma$. Then there
exists a DFA
$\,M^{\prime}\;=\;(Q^{\prime},\Sigma,\delta^{\prime},q_{0}^{\prime},F^{\prime})$
that recognizes $\mathcal{L}(M)\,\circ\,\\{a\\}$ such that
$|F^{\prime}|\leq|F|$ and $|Q^{\prime}|\;\leq\;|Q|+|F|$.

######  Proof B.14.

The concatenation of a letter with a DFA can be easily achieved by adding
extra transitions from each final state $q_{fi}$ to a new state $p_{i}$ for
the symbol $a$. However, that turns the DFA $M$ into a non-deterministic
finite automaton (NFA). We claim that there exists a DFA $M^{\prime}$ with
$|F|$ as the upper bound for accepting states.

Consider Figure 2: $q_{f1}$ through $q_{fn}$ are the $n$ final states of the
given DFA $M$. Suppose $\delta(q_{fi},a)=r_{i}$. Then the subset construction
gives us the new transition
$\delta{\prime}(\\{q_{fi}\\},a)=\\{r_{i},p_{i}\\}$. The new accepting states
for the new DFA $M^{\prime}$ will be $\\{r_{i},p_{i}\\}$, such that $1\leq
i\leq n$.

$q_{f1}$$\vdots$$q_{fn}$$p_{1}$$p_{n}$$r_{1}$$r_{n}$$r_{2}$$r_{n2}$(a)
$M$$a$$a$$b$$a$$a$$b$

$q_{f1}$$\vdots$$q_{fn}$$r_{1},p_{1}$$r_{n},p_{n}$$r_{1}$$r_{n}$$r_{2}$$r_{n2}$(b)
$M^{\prime}$$a$$a$$b$$b$$b$$b$

Figure 2. DFA $M$ concatenation with a single letter $a$.

Besides, if the transitions for the letter $a$ from two earlier accepting
states have the same destination state, we can combine the new accepting
states that were created. Thus in Figure 3, the state $\\{r_{1},p_{1}\\}$ can
be assigned to $\delta^{\prime}(\\{q_{fn}\\},a)$, avoiding needless
duplication.

Thus the number of final states, $|F^{\prime}|$ for the DFA $M^{\prime}$ is
less than or equal to the original number of final states, $|F|$, in DFA $M$.

Total number of states $|Q^{\prime}|$ for $M^{\prime}$ is bounded by the
number of the final states $|F|$ in $M$ as well as the number of total states,
$|Q|$, in $M$. Therefore, the number of states for $M^{\prime}$ can be less
than or equal to the both of the factors, i.e., $|Q^{\prime}|\leq|Q|+|F|$.

$q_{f1}$$\vdots$$q_{fn}$$p_{1}$$r_{1}$(a)
$M$$a$$a$$a$$a$$q_{f1}$$\vdots$$q_{fn}$$r_{1},p_{1}$(b) $M^{\prime}$$a$$a$

Figure 3. DFA $M^{\prime}$ can have less than $|F|$ states.

######  Lemma 16.

Concatenation of a deterministic finite automaton (DFA) with a single string
has the time complexity $O(|F|\ast|Z|\ast|\Sigma|)$, where $|F|$ is the number
of final states in the DFA, $|Z|$ is the length of the string and $|\Sigma|$
is the size of the alphabet.

######  Proof B.15.

Recall the previous lemma proved that the number of states in the new DFA
after the concatenation of one letter is at most $|Q|+|F|$ and that the number
of (new) accepting states is at most $F$. Thus repeatedly applying this
operation will result in a DFA with at most $|Q|+|Z|\ast|F|$ states and at
most $|F|$ accepting states. The number of new edges will be at most
$|F|\ast|Z|\ast|\Sigma|$. Thus the overall complexity is polynomial in the
size of the original DFA. The Figure 4 shows an example of DFA $M$’s
concatenation with the symbols in string $Z$.

$q_{0}$start$\ldots$$\vdots$$q_{a1}$$q_{an}$$p_{1}$$p_{2}$$\ldots$$p_{n}$$a_{1}$$a_{1}$$a_{1}$$a_{2}$$a_{3}$$a_{n}$
Figure 4. DFA $M$ concatenation with a string $Z=a_{1}a_{2}\ldots a_{n}$.

######  Lemma 17.

Let $M_{1}$ and $M_{2}$ be DFAs. Then a multiple-entry DFA (MEFA)
for $\mathcal{L}(M_{2})\,\backslash\,\mathcal{L}(M_{1})$ can be computed in
polynomial time.

######  Proof B.16.

Let $M_{1}=(Q_{1},\Sigma,\delta_{1},q_{01},F_{1})$ and
$M_{2}=(Q_{2},\Sigma,\delta_{2},q_{02},F_{2})$ and let
$L_{quo}=\mathcal{L}(M_{2})\backslash\mathcal{L}(M_{1})$. A string $y$ belongs
to $L_{quo}$ if and only if there exists a string $x$ and states $p\in Q_{1}$,
$p^{\prime}\in F_{1}$ and $q\in F_{2}$ such that
$\delta_{2}^{*}(q_{02},\,x)~{}=~{}q$, $\delta_{1}^{*}(q_{01},\,x)~{}=~{}p$ and
$\delta_{1}^{*}(p,\,y)~{}=~{}p^{\prime}$.

Let $P$ be the product transition system of the two automata, i.e.,

$P\;=\;(Q_{1}\times Q_{2},\Sigma,\delta,(q_{01},q_{02}))$

where $\delta$ is defined as

$\delta((r,r^{\prime}),c)=(\delta_{1}(r,c),\,\delta_{2}(r^{\prime},c))$

for all $c\in\Sigma$, $r\in Q_{1}$ and $r^{\prime}\in Q_{2}$. We can assume
that states which are not reachable from $(q_{01},q_{02})$ have been removed.
This can be done in time linear in the size of the transition graph. Now in
terms of the transition system we can say that a string $y$ belongs to
$L_{quo}$ if and only if there exists a string $x$ and states $p\in Q_{1}$,
$p^{\prime}\in F_{1}$, $q\in F_{2}$ and $q^{\prime}\in Q_{2}$ such that

$\delta^{*}((q_{01},q_{02}),\,x)~{}=~{}(p,q)\text{ and
}\delta^{*}((p,q),y)~{}=~{}(p^{\prime},q^{\prime})$

We can now convert $P$ into a multiple-entry DFA (MEFA). In the above case,
$(p,q)$ has to be one of the initial states of the new MEFA, and
$(p^{\prime},q^{\prime})$ one of its final states. Therefore, the states that
are reachable from $(q_{01},q_{02})$ that are in $F_{2}\times Q_{1}$ will be
the initial states of the MEFA and $F_{1}\times Q_{2}$ will be the final
states of the MEFA.

######  Lemma 18.

Given two MEFAs, we can check whether their intersection is empty in
polynomial time.

######  Proof B.17.

Consider two MEFAs $A_{1}\;=\;(Q_{1},\Sigma,\delta_{1},Q_{s_{1}},F_{A_{1}})$
and $A_{2}\;=\;(Q_{2},\Sigma,\delta_{2},Q_{s_{2}},F_{A_{2}})$. $Q_{s_{1}}$ and
$Q_{s_{2}}$ may include more than one initial state. A string $w$ is accepted
by both MEFAs if and only if there exist states $q_{init}^{1}\;\in\;Q_{s_{1}}$
and $q_{init}^{2}\;\in\;Q_{s_{2}}$ such that

$\delta_{1}^{*}(q_{init}^{1},w)\;\in\;F_{A1}\text{
and}\delta_{2}^{*}(q_{init}^{2},w)\;\in\;F_{A2}.$

To find such a string $w$, we take the product transition system of the two
MEFAs, named as $T$, i.e., $T\;=\;(Q_{1}\times
Q_{2},\Sigma,\delta,(Q_{s_{1}}\times Q_{s_{2}}))$ where

$\delta((r,r^{\prime}),c)=(\delta_{1}(r,c),\,\delta_{2}(r^{\prime},c))$

for all $c\in\Sigma$, $r\in Q_{1}$ and $r^{\prime}\in Q_{2}$. A string $w$ is
accepted by both of the MEFAs $A_{1}$ and $A_{2}$ if and only if there exist
states $p,q,p^{\prime},q^{\prime}$ such that $p\;\in\;Q_{s_{1}}$,
$q\;\in\;Q_{s_{2}}$, $p^{\prime}\;\in\;F_{A_{1}}$ and
$q^{\prime}\;\in\;F_{A_{2}}$, and

$\delta^{*}((p,q),w)~{}=~{}(p^{\prime},q^{\prime})$

We can now apply _depth-first search (DFS)_ to check, in time linear in the
size of $T$, if there exists a path from some state in $Q_{s_{1}}\times
Q_{s_{2}}$ to a state in $F_{A_{1}}\times F_{A_{2}}$.

######  Lemma 19.

The following problem is decidable in polynomial time:

> > Input:
>>
>>

>> DFAs $M$ and $N$.
>
>>

>> Question:

>>
>>

>> Do there exist strings $x,y,z$ such that $x\neq y$, $x,y\in\mathcal{L}(M)$,
_and_ $xz,yz\in\mathcal{L}(N)$?

######  Proof B.18.

Suppose there exist strings $x,y,z$ such that $x\neq y$,
$x,y\in\mathcal{L}(M)$, _and_ $xz,yz\in\mathcal{L}(N)$. We call the triple
$(x,y,z)$ a _solution_. Thus, we have two cases:

  1. (i)

Both $x$ and $y$ start from an initial state $q_{0}$ and reach the same state,
$q$, in $N$, i.e.,

$\exists\;q:\delta^{*}(q_{0}^{N},x)=\delta^{*}(q_{0}^{N},y)=q\;\;\mathrm{and}\;\;\delta^{*}(q,z)\in
F^{N}.$

  2. (ii)

$x$ and $y$ reach different states, say $q^{\prime}$ and $q^{\prime\prime}$,
in $N$, i.e.,

$\exists\;q^{\prime},q^{\prime\prime}:\delta^{*}(q_{0}^{N},x)=q^{\prime}\neq
q^{\prime\prime}=\delta^{*}(q_{0}^{N},y)\;\;\mathrm{and}\;\;\delta^{*}(q^{\prime},z)\in
F^{N}\land\delta^{*}(q^{\prime\prime},z)\in F^{N}.$

Let $A=(Q,\Sigma,\delta,s,F)$ be a DFA and $p$ be a state in $A$. By
$A^{F=\\{p\\}}$, we denote a replication of $A$, with the sole difference of
$p$ being the only accepting state of $A$. Thus $N^{F=\\{q\\}}$ denotes a
replication of $N$, with $q$ being the accepting state of $N$. Then, we
classify these states of $N$ which _are not dead states_ into GREEN, ORANGE
and BLUE states. Note that confirming the status of $q$ being a dead state can
be done in linear time w.r.t. to the size of graph.

  * •

_GREEN states:_
$\big{\\{}q\mid\;\scalebox{1.2}{$\mid$}\mathcal{L}(N^{F=\\{q\\}})\cap\mathcal{L}(M)\scalebox{1.2}{$\mid$}>1\big{\\}}$.

The state $q$ mentioned in case (i) is a GREEN state. (See Figure 5(a))

  * •

_ORANGE states:_
$\big{\\{}q\mid\;\scalebox{1.2}{$\mid$}\mathcal{L}(N^{F=\\{q\\}})\cap\mathcal{L}(M)\scalebox{1.2}{$\mid$}=1\big{\\}}$.

Suppose that case (i) does not apply, i.e., there are no GREEN states in $N$.
Then case (ii) must apply and the states $q^{\prime}$ and $q^{\prime\prime}$
must be ORANGE states; in other words, the intersection of $\mathcal{L}(M)$
individually with the two DFAs, $\mathcal{L}(N^{F=\\{q^{\prime}\\}})$ and
$\mathcal{L}(N^{F=\\{q^{\prime\prime}\\}})$ gives us exactly 1 string for
each. Note also that $x$ and $y$ are two strings in $\mathcal{L}(M)$ which are
not equal to each other since $q^{\prime}\;\neq\;q^{\prime\prime}$. (See
Figure 5(b))

  * •

_BLUE states:_
$\big{\\{}q\mid\;\scalebox{1.2}{$\mid$}\mathcal{L}(N^{F=\\{q\\}})\cap\mathcal{L}(M)\scalebox{1.2}{$\mid$}=0\big{\\}}$.

$q_{0}$start$q$$\vdots$$x$$y$$z$ (a) Green States

$q_{0}$start$q$$q^{\prime}$$\vdots$$x$$y$$z$$z$ (b) Orange States

Figure 5. Different Structures of Green and Orange States.

The algorithm for finding the triple $(x,y,z)$ is constructed as follows.
First, we identify the green and orange states. If there exists a green state,
then we have a solution. Otherwise we explore whether there exists a $z$ such
that $\delta^{*}(q^{\prime},z)\in F^{N}\land\delta^{*}(q^{\prime\prime},z)\in
F^{N}$ for orange states $q^{\prime}$ and $q^{\prime\prime}$, i.e., we check
whether

$\big{\\{}\,z\;\big{|}\;\exists(q^{\prime},q^{\prime\prime}):\,q^{\prime},q^{\prime\prime}\text{
are orange states }\land\;\delta^{*}(q^{\prime},z)\in
F^{N}\;\land\;\delta^{*}(q^{\prime\prime},z)\in F^{N}\big{\\}}$

is empty.

Given orange states $q^{\prime}$ and $q^{\prime\prime}$, we use DFA
intersection to check whether there is a string $z$ that takes both to an
accepting state. Let $N_{s=\\{q^{\prime}\\}}$ denote a replication of $N$,
with the difference of $q^{\prime}$ being the initial state of $N$.
$N_{s=\\{q^{\prime\prime}\\}}$ is similar to the $N_{s=\\{q^{\prime}\\}}$, but
this time $q^{\prime\prime}$ is the initial state. After creating these two
DFAs, we can find if there exists a string $z$ by intersecting the DFA
$N_{s=\\{q^{\prime}\\}}$ with $N_{s=\\{q^{\prime\prime}\\}}$. This process may
have to be repeated for every tuple $(q^{\prime},q^{\prime\prime})$ of orange
states.

Figure 6. How the monadic cone looks for $\alpha$

The Figure 6 illustrates how $\alpha X$ reduces to its normal form
$\alpha_{1}aX_{2}$. ($\alpha$ and $X$ are irreducible strings.)

Let $R$ be a convergent monadic SRS. For an irreducible string $\alpha$, let

$MP(\alpha)~{}=~{}\Big{\\{}\,w\\!\big{\downarrow}\;~{}\Big{|}~{}\;w\in
PREF(\alpha)\circ(\Sigma\cup\\{\epsilon\\})\Big{\\}}$

_MP_ stands for the term _Minimal Product_ and _PREF_ is the set of _prefixes_
of given string.

######  Lemma 20.

Let $\mu,\omega,X,Y\in IRR(R)$. Then $\mu X\downarrow\omega Y$ if and only if
there exist strings $X^{\prime},Y^{\prime},W,\gamma$ such that

  1. (1)

$\gamma\in MP(\mu)\cup MP(\omega)$,

  2. (2)

$X=X^{\prime}W$, $Y=Y^{\prime}W$, _and_

  3. (3)

$\mu
X^{\prime}\stackrel{{\scriptstyle!}}{{{\longrightarrow}_{R}}}~{}\gamma\;\;~{}{}_{R}{\\!{\stackrel{{\scriptstyle!}}{{\longleftarrow}}}}\;\omega
Y^{\prime}$.

######  Proof B.19.

This proof as well as the proof for Lemma 21 follows from [OND98] (see Lemma
3.6).

######  Lemma 21.

Let $\alpha_{1},\alpha_{2},\beta_{1},\beta_{2},X,Y\in IRR(R)$. Then
$\alpha_{1}X\downarrow\alpha_{2}Y$ and $\beta_{1}X\downarrow\beta_{2}Y$ if and
only if there exist strings $X^{\prime},Y^{\prime},V,W,\gamma_{1},\gamma_{2}$
such that

  1. (1)

$\gamma_{1}\in MP(\alpha_{1})\cup MP(\alpha_{2})$,

  2. (2)

$\gamma_{2}\in MP(\beta_{1})\cup MP(\beta_{2})$,

  3. (3)

$X=X^{\prime}VW$, $Y=Y^{\prime}VW,\;\;$ _and_

  4. (4)

either

     * (a)

$\alpha_{1}X^{\prime}V\stackrel{{\scriptstyle!}}{{{\longrightarrow}_{R}}}~{}\gamma_{1}\;\;~{}{}_{R}{\\!{\stackrel{{\scriptstyle!}}{{\longleftarrow}}}}\;\alpha_{2}Y^{\prime}V\;\;$
_and_

     * (b)

$\;\;\;\beta_{1}X^{\prime}\stackrel{{\scriptstyle!}}{{{\longrightarrow}_{R}}}~{}\gamma_{2}\;\;~{}{}_{R}{\\!{\stackrel{{\scriptstyle!}}{{\longleftarrow}}}}\;\beta_{2}Y^{\prime}$.

or

     * (c)

$\;\;\;\alpha_{1}X^{\prime}\stackrel{{\scriptstyle!}}{{{\longrightarrow}_{R}}}~{}\gamma_{1}\;\;~{}{}_{R}{\\!{\stackrel{{\scriptstyle!}}{{\longleftarrow}}}}\;\alpha_{2}Y^{\prime}\;\;$
_and_

     * (d)

$\beta_{1}X^{\prime}V\stackrel{{\scriptstyle!}}{{{\longrightarrow}_{R}}}~{}\gamma_{2}\;\;~{}{}_{R}{\\!{\stackrel{{\scriptstyle!}}{{\longleftarrow}}}}\;\beta_{2}Y^{\prime}V$.

######  Corollary 22.

Let $\alpha_{1},\alpha_{2},\beta_{1},\beta_{2}\in IRR(R)$. Then there exist
irreducible strings $X$ and $Y$ such that $\alpha_{1}X\downarrow\alpha_{2}Y$
and $\beta_{1}X\downarrow\beta_{2}Y$ if and only if there exist strings
$X^{\prime},Y^{\prime},V,\gamma_{1},\gamma_{2}$ such that

  1. (1)

$\gamma_{1}\in MP(\alpha_{1})\cup MP(\alpha_{2})$,

  2. (2)

$\gamma_{2}\in MP(\beta_{1})\cup MP(\beta_{2})$,

  3. (3)

$X^{\prime}V$ and $Y^{\prime}V$ are irreducible, _and_

  4. (4)

either

     * (a)

$\alpha_{1}X^{\prime}V\stackrel{{\scriptstyle!}}{{{\longrightarrow}_{R}}}~{}\gamma_{1}\;\;~{}{}_{R}{\\!{\stackrel{{\scriptstyle!}}{{\longleftarrow}}}}\;\alpha_{2}Y^{\prime}V\;\;$
_and_

     * (b)

$\;\;\;\beta_{1}X^{\prime}\stackrel{{\scriptstyle!}}{{{\longrightarrow}_{R}}}~{}\gamma_{2}\;\;~{}{}_{R}{\\!{\stackrel{{\scriptstyle!}}{{\longleftarrow}}}}\;\beta_{2}Y^{\prime}$.

or

     * (c)

$\;\;\;\alpha_{1}X^{\prime}\stackrel{{\scriptstyle!}}{{{\longrightarrow}_{R}}}~{}\gamma_{1}\;\;~{}{}_{R}{\\!{\stackrel{{\scriptstyle!}}{{\longleftarrow}}}}\;\alpha_{2}Y^{\prime}\;\;$
_and_

     * (d)

$\beta_{1}X^{\prime}V\stackrel{{\scriptstyle!}}{{{\longrightarrow}_{R}}}~{}\gamma_{2}\;\;~{}{}_{R}{\\!{\stackrel{{\scriptstyle!}}{{\longleftarrow}}}}\;\beta_{2}Y^{\prime}V$.

######  Lemma 23.

Let $\alpha_{1},\alpha_{2},\beta_{1},\beta_{2}\in IRR(R)$. Then there exist
irreducible strings $X$ and $Y$ such that $\alpha_{1}X\downarrow\alpha_{2}Y$
and $\beta_{1}X\downarrow\beta_{2}Y$ if and only if there exist strings
$X^{\prime},Y^{\prime},V,\gamma_{1},\gamma_{2}$ such that

  1. (1)

$\gamma_{1}\in MP(\alpha_{1})\cup MP(\alpha_{2})$,

  2. (2)

$\gamma_{2}\in MP(\beta_{1})\cup MP(\beta_{2})$,

  3. (3)

either

     * (a)

$X^{\prime}V\,\in\,RF(\alpha_{1},\gamma_{1})$,
$~{}Y^{\prime}V\,\in\,RF(\alpha_{2},\gamma_{1})$,
$~{}X^{\prime}\,\in\,RF(\beta_{1},\gamma_{2})$ _and_
$~{}Y^{\prime}\,\in\,RF(\beta_{2},\gamma_{2})$

or

     * (b)

$X^{\prime}\,\in\,RF(\alpha_{1},\gamma_{1})$,
$~{}Y^{\prime}\,\in\,RF(\alpha_{2},\gamma_{1})$,
$~{}X^{\prime}V\,\in\,RF(\beta_{1},\gamma_{2})$ _and_
$~{}Y^{\prime}V\,\in\,RF(\beta_{2},\gamma_{2})$

######  Lemma 24.

Let $\mu,X,Y\in IRR(R)$ where $X\neq Y$. Then $\mu X\downarrow\mu Y$ if and
only if there exist strings $X^{\prime},Y^{\prime},W,\gamma$ such that

  1. (1)

$\gamma\in MP(\mu)$,

  2. (2)

$X=X^{\prime}W$, $Y=Y^{\prime}W$, $X^{\prime}\neq Y^{\prime}\;$ _and_

  3. (3)

$\mu
X^{\prime}\stackrel{{\scriptstyle!}}{{{\longrightarrow}_{R}}}~{}\gamma\;\;~{}{}_{R}{\\!{\stackrel{{\scriptstyle!}}{{\longleftarrow}}}}\;\mu
Y^{\prime}$.

######  Proof B.20.

Let $Z$ be the normal form of $\mu X$ and $\mu Y$.
Then there exists strings
$\mu_{1},\mu_{2},\mu_{3},\mu_{4},X_{1},X_{2},Y_{1},Y_{2}$ such that
$\mu=\mu_{1}\mu_{2}=\mu_{3}\mu_{4}$, $X=X_{1}X_{2}$, $Y=Y_{1}Y_{2}$ and

|  $\mu_{2}X_{1}\;\rightarrow^{!}\;a$,
---|---
|  $\mu_{4}Y_{1}\;\rightarrow^{!}\;b,\qquad$ and
|  $Z={\mu_{1}}\,a\,{X_{2}}={\mu_{3}}\,b\,{Y_{2}}$.

where $a,b\in\Sigma\cup\\{\lambda\\}$. If $X_{1}=Y_{1}$, then the same
reduction can be applied on both sides, i.e., $\mu_{2}=\mu_{4}$ and $a=b$. But
the rest of the string $X_{2}\neq Y_{2}$ since $X\neq Y$. Therefore, we
conclude that $X_{1}\neq Y_{1}$. It can also be seen that
$\mu_{1}a,\,\mu_{3}b\in MP(\alpha)$.

We now consider two cases:

  1. (a)

$X_{2}$ is a suffix of $Y_{2}$: Let $Y_{2}=Y_{2}^{\prime}X_{2}$. Then
${\mu_{1}}\,a\;=\;{\mu_{3}}\,b\,{Y_{2}^{\prime}}$. We can take
$\gamma={\mu_{1}}\,a$, $X^{\prime}=X_{1}$, $Y^{\prime}=Y_{1}Y_{2}^{\prime}$
and $W=X_{2}$.

  2. (b)

$Y_{2}$ is a suffix of $X_{2}$: Let $X_{2}=X_{2}^{\prime}Y_{2}$. Then
${\mu_{1}}\,aX_{2}^{\prime}\;=\;{\mu_{3}}\,b$. In this case we can take
$\gamma={\mu_{3}}\,b$, $X^{\prime}=X_{1}X_{2}^{\prime}$, $Y^{\prime}=Y_{1}$
and $W=X_{2}$.

######  Lemma 25.

Let $\alpha,\beta\in IRR(R)$. Then there exist _distinct_ irreducible strings
$X$ and $Y$ such that $\alpha X\downarrow\alpha Y$ and $\beta X\downarrow\beta
Y$ if and only if there exist irreducible strings
$X^{\prime},Y^{\prime},V,W,\gamma_{1},\gamma_{2}$ such that

  1. (1)

$X^{\prime}\,\neq\,Y^{\prime}$,

  2. (2)

$\gamma_{1}\in MP(\alpha)$,

  3. (3)

$\gamma_{2}\in MP(\beta)$,

  4. (4)

$X=X^{\prime}VW$, $Y=Y^{\prime}VW$, and

  5. (5)

either

     * (a)

$\alpha
X^{\prime}V\stackrel{{\scriptstyle!}}{{{\longrightarrow}_{R}}}~{}\gamma_{1}\;\;~{}{}_{R}{\\!{\stackrel{{\scriptstyle!}}{{\longleftarrow}}}}\;\alpha
Y^{\prime}V\;\;$ _and_

     * (b)

$\;\;\;\beta
X^{\prime}\stackrel{{\scriptstyle!}}{{{\longrightarrow}_{R}}}~{}\gamma_{2}\;\;~{}{}_{R}{\\!{\stackrel{{\scriptstyle!}}{{\longleftarrow}}}}\;\beta
Y^{\prime}$.

or

     * (c)

$\;\;\;\alpha
X^{\prime}\stackrel{{\scriptstyle!}}{{{\longrightarrow}_{R}}}~{}\gamma_{1}\;\;~{}{}_{R}{\\!{\stackrel{{\scriptstyle!}}{{\longleftarrow}}}}\;\alpha
Y^{\prime}\;\;$ _and_

     * (d)

$\beta
X^{\prime}V\stackrel{{\scriptstyle!}}{{{\longrightarrow}_{R}}}~{}\gamma_{2}\;\;~{}{}_{R}{\\!{\stackrel{{\scriptstyle!}}{{\longleftarrow}}}}\;\beta
Y^{\prime}V$.

######  Proof B.21.

Assume that there exist strings
$X^{\prime},Y^{\prime},V,\gamma_{1},\gamma_{2}$ that satisfy the properties
above. Let us consider the fifth property. It shows that $\alpha
X^{\prime}V\downarrow\alpha Y^{\prime}V$ as well as $\beta
X^{\prime}V\downarrow\beta Y^{\prime}V$. Now suppose $X=X^{\prime}V$ and
$Y=Y^{\prime}V$. Therefore, we can see that $\alpha X\downarrow\alpha Y$ as
well as $\beta X\downarrow\beta Y$ and $X$ and $Y$ are distinct irreducible
strings.

Conversely, assume that there exist distinct irreducible strings $X$ and $Y$
such that $\alpha X\downarrow\alpha Y$ and $\beta X\downarrow\beta Y$. We
start by considering the case $\alpha X\downarrow\alpha Y$ such that $X\neq
Y$. By Lemma 24, there must be strings $X^{\prime}$, $Y^{\prime}$, $Z$ and
$\gamma_{1}$ such that $X=X^{\prime}Z$, $Y=Y^{\prime}Z$ and $\alpha
X^{\prime}\;\stackrel{{\scriptstyle!}}{{{\longrightarrow}_{R}}}~{}\gamma_{1}~{}\;\;{}_{R}{\\!{\stackrel{{\scriptstyle!}}{{\longleftarrow}}}}\;\alpha
Y^{\prime}$ where $\gamma_{1}\in MP(\alpha)$. Similarly, for the case $\beta
X\downarrow\beta Y$, $X$ can be written as $X^{\prime\prime}Z^{\prime}$ and
$Y$ can be written as $Y^{\prime\prime}Z^{\prime}$ such that $\beta
X^{\prime\prime}\;\stackrel{{\scriptstyle!}}{{{\longrightarrow}_{R}}}~{}\gamma_{2}\;\;~{}{}_{R}{\\!{\stackrel{{\scriptstyle!}}{{\longleftarrow}}}}\;\beta
Y^{\prime\prime}$ for some $\gamma_{2}\in MP(\beta)$.

We have to consider two cases depending on whether $X^{\prime}$ is a prefix of
$X^{\prime\prime}$ or vice versa. It is not hard to see that they correspond
to the two cases in condition 5.

######  Corollary 26.

Let $\alpha,\beta\in IRR(R)$. Then there exist _distinct_ irreducible strings
$X$ and $Y$ such that $\alpha X\downarrow\alpha Y$ and $\beta X\downarrow\beta
Y$ if and only if there exist irreducible strings
$X^{\prime},Y^{\prime},V,\gamma_{1},\gamma_{2}$ such that

  1. (1)

$X^{\prime}\,\neq\,Y^{\prime}$,

  2. (2)

$\gamma_{1}\in MP(\alpha)$,

  3. (3)

$\gamma_{2}\in MP(\beta)$,

  4. (4)

$X^{\prime}V$ and $Y^{\prime}V$ are irreducible, and

  5. (5)

either

     * (a)

$\alpha
X^{\prime}V\stackrel{{\scriptstyle!}}{{{\longrightarrow}_{R}}}~{}\gamma_{1}\;\;~{}{}_{R}{\\!{\stackrel{{\scriptstyle!}}{{\longleftarrow}}}}\;\alpha
Y^{\prime}V\;\;$ _and_

     * (b)

$\;\;\;\beta
X^{\prime}\stackrel{{\scriptstyle!}}{{{\longrightarrow}_{R}}}~{}\gamma_{2}\;\;~{}{}_{R}{\\!{\stackrel{{\scriptstyle!}}{{\longleftarrow}}}}\;\beta
Y^{\prime}$.

or

     * (c)

$\;\;\;\alpha
X^{\prime}\stackrel{{\scriptstyle!}}{{{\longrightarrow}_{R}}}~{}\gamma_{1}\;\;~{}{}_{R}{\\!{\stackrel{{\scriptstyle!}}{{\longleftarrow}}}}\;\alpha
Y^{\prime}\;\;$ _and_

     * (d)

$\beta
X^{\prime}V\stackrel{{\scriptstyle!}}{{{\longrightarrow}_{R}}}~{}\gamma_{2}\;\;~{}{}_{R}{\\!{\stackrel{{\scriptstyle!}}{{\longleftarrow}}}}\;\beta
Y^{\prime}V$.

######  Lemma 27.

Let $\alpha,\beta\in IRR(R)$. Then there exist _distinct_ irreducible strings
$X$ and $Y$ such that $\alpha X\downarrow\alpha Y$ and $\beta X\downarrow\beta
Y$ if and only if there exist strings
$X^{\prime},Y^{\prime},V,\gamma_{1},\gamma_{2}$ such that

  1. (1)

$X^{\prime}\,\neq\,Y^{\prime}$,

  2. (2)

$\gamma_{1}\in MP(\alpha)$,

  3. (3)

$\gamma_{2}\in MP(\beta)$,

  4. (4)

either

     * (a)

$X^{\prime}V,\,Y^{\prime}V\,\in\,RF(\alpha,\gamma_{1})$ _and_

     * (b)

$X^{\prime},\,Y^{\prime}\,\in\,RF(\beta,\gamma_{2})$

or

     * (c)

$X^{\prime},\,Y^{\prime}\,\in\,RF(\alpha,\gamma_{1})$ _and_

     * (d)

$X^{\prime}V,\,Y^{\prime}V\,\in\,RF(\beta,\gamma_{2})$

##  Appendix C Appendix

This corollary is a slightly simpler construction than the one in [NO97] for
the reader’s ease of understanding.

######  Corollary 28.

There is a finite and convergent string system for which the common term (CT)
problem is decidable, while the common equation (CE) problem is undecidable.

We show that CE is undecidable by a reduction from GPCP. (See Section 2.1.)
For notational convenience, we represent an instance of the GPCP as a 3-tuple

$\Bigg{\langle}\bigg{[}\dfrac{x}{y}\bigg{]},\,S,\,\bigg{[}\dfrac{u}{v}\bigg{]}\Bigg{\rangle}$

where $(x,y)$ is the start domino, $(u,v)$ is the end domino and $S$ the set
of intermediate dominos.

######  Theorem 29 ([HMU03]).

There exist strings $\alpha$, $\beta$, and a set of tuples of strings $S$ such
that following problem is undecidable:

Input:

Strings $x_{0},y_{0}$.

Question:

Does the GPCP
$\Bigg{\langle}\bigg{[}\dfrac{x_{0}}{y_{0}}\bigg{]},\,S,\,\bigg{[}\dfrac{\alpha}{\beta}\bigg{]}\Bigg{\rangle}$
have a solution?

Let
$\Bigg{\langle}\bigg{[}\dfrac{x_{0}}{y_{0}}\bigg{]},\,\left\\{(x_{i},\;y_{i})\right\\}^{n}_{i=1}\,\bigg{[}\dfrac{x_{n+1}}{y_{n+1}}\bigg{]}\Bigg{\rangle}$
be an instance of the GPCP, i.e.,
$\mathop{\left\\{(x_{i},\;y_{i})\right\\}}^{n}_{i=1}$ is the set of
intermediate dominoes and $(x_{0},y_{0}),(x_{n+1},y_{n+1})$, the start and end
dominoes respectively, where the strings are over the alphabet
$\Sigma=\\{a,\,b\\}$. Let

$\widehat{\Sigma}=\\{a,b\\}\,\cup\,\\{c_{0},\ldots,c_{n}\\}\,\cup\,\\{\cent_{1},\cent_{2},\$,\\#_{1},\\#_{2}\\}$

be the new alphabet for the instance of CE.

From the given instance, we construct a string-rewriting system $R_{1}$ with
the following rules:

$\begin{aligned} \cent_{1}\;c_{1}&\rightarrow&x_{1}\;\cent_{1},\\\
\mathmakebox[width("{}\cent_{1}\;c_{n}{}")][c]{\vdots}&\rightarrow&\mathmakebox[width("{}x_{n}\cent_{1}{}")][c]{\vdots}\\\
\cent_{1}\;c_{n+1}&\rightarrow&\\#_{1}\;x_{n+1}\$\\\\[20.0pt]
\cent_{2}\;c_{1}&\rightarrow&y_{1}\;\cent_{2},\\\
\mathmakebox[width("{}\cent_{2}\;c_{n}{}")][c]{\vdots}&\rightarrow&\mathmakebox[width("{}y_{n}\cent_{2}{}")][c]{\vdots}\\\
\cent_{2}\;c_{n+1}&\rightarrow&\\#_{2}\;y_{n+1}\$\end{aligned}\qquad\qquad\qquad\begin{aligned}
a\;\\#_{1}&\rightarrow&\\#_{1}\;a\\\
b\;\\#_{1}&\rightarrow&\\#_{1}\;b\\\\[20.0pt]
a\;\\#_{2}&\rightarrow&\\#_{2}\;a\\\ b\;\\#_{2}&\rightarrow&\\#_{2}\;b\\\
\end{aligned}$

######  Lemma 30.

$R_{1}$ is convergent.

######  Lemma 31.

GPCP has a solution if and only if there exist strings $w_{1},w_{2}$ such that
$x_{0}\cent_{1}\;w_{1}\rightarrow^{!}\\#_{1}w_{2}$ and
$y_{0}\cent_{2}\;w_{1}\rightarrow^{!}\\#_{2}w_{2}$.

######  Proof C.22.

We prove the “if” direction first. Assume GPCP has a solution. Let
$i_{1},\ldots,i_{k}$ be the indices of the intermediate dominoes used, i.e.,
there are $k+2$ dominoes in all including the start and end dominoes. This
will result in
$x_{0}\;x_{i_{1}},\ldots,x_{i_{k}}\;x_{n+1}=y_{0}\;y_{i_{1}},\ldots,y_{i_{k}}\;y_{n+1}$.
Let $w_{1}=c_{i_{1}}\ldots c_{i_{k}}c_{n+1}$ and $w_{2}=x_{0}\;x_{i_{1}}\ldots
x_{i_{k}}\;x_{n+1}\$$, then

$\displaystyle x_{0}\;\cent_{1}c_{i_{1}}\ldots c_{i_{k}}c_{n+1}$
$\displaystyle\rightarrow
x_{0}\;x_{i_{1}}\cent_{1}\;\ldots\;c_{i_{k}}c_{n+1}\rightarrow^{!}\\#_{1}\;x_{0}\;x_{i_{1}}\ldots
x_{i_{k}}\;x_{n+1}\$$ $\displaystyle y_{0}\;\cent_{2}c_{i_{1}}\ldots
c_{i_{k}}c_{n+1}$ $\displaystyle\rightarrow
y_{0}\;y_{i_{1}}\cent_{2}\;\ldots\;c_{i_{k}}c_{n+1}\rightarrow^{!}\\#_{1}\;y_{0}\;y_{i_{1}}\ldots
y_{i_{k}}\;y_{n+1}\$$

For the “only if” direction suppose there exist strings $w_{1}$ and $w_{2}$
such that

$x_{0}\;\cent_{1}\;w_{1}\rightarrow^{!}\\#_{1}w_{2}\text{
and}y_{0}\;\cent_{2}\;w_{1}\rightarrow^{!}\\#_{2}w_{2}.$

Without loss of generality, we can assume that $w_{1}$ and $w_{2}$ are
irreducible. The observation of the rules on the both sides shows that
$\\#_{1}w_{2}$ and $\\#_{2}w_{2}$ can be derived if and only if $c_{n+1}$
occurs in $w_{1}$ since only the rules with $c_{n+1}$ has a $\cent$ on the
left-hand side (LHS) and a $\\#$ symbol on the RHS.

Thus, we can write $w_{1}$ as
$w_{1}={w_{1}^{\prime}}\;c_{n+1}\;{w_{1}^{\prime\prime}}$ such that
${w_{1}^{\prime}}c_{n+1}$ is the shortest prefix of $w_{1}$ that contains
$c_{n+1}$. To be able to apply the rules with $\cent$ signs,
${w_{1}^{\prime}}$ should be in $\\{c_{1},\ldots,c_{n}\\}^{*}$. Let
${w_{1}}^{\prime}\,=\,c_{i_{1}}\ldots c_{i_{k}}$ where $k=|{w_{1}}^{\prime}|$.

$\displaystyle x_{0}\;\cent_{1}\;{w_{1}}^{\prime}\;c_{n+1}$
$\displaystyle\rightarrow^{*}\\#_{1}x_{0}\;x_{i_{1}}\;\ldots\;x_{i_{k}}\;x_{n+1}\$$
$\displaystyle y_{0}\;\cent_{2}\;{w_{1}}^{\prime}\;c_{n+1}$
$\displaystyle\rightarrow^{*}\\#_{2}y_{0}\;y_{i_{1}}\;\ldots\;y_{i_{k}}\;y_{n+1}\$$

Since $\$$ does not occur on the left hand side of the rules, the string after
the $\$$ sign, i.e., ${w_{1}^{\prime\prime}}$, does not take part in the
reductions. Thus

$\displaystyle
x_{0}\;\cent_{1}\;{w_{1}}^{\prime}\;c_{n+1}\;{w_{1}^{\prime\prime}}$
$\displaystyle\rightarrow^{!}\\#_{1}x_{0}\;x_{i_{1}}\;\ldots\;x_{i_{k}}\;x_{n+1}\$\;{w_{1}^{\prime\prime}}$
$\displaystyle
y_{0}\;\cent_{2}\;{w_{1}}^{\prime}\;c_{n+1}\;{w_{1}^{\prime\prime}}$
$\displaystyle\rightarrow^{!}\\#_{2}y_{0}\;y_{i_{1}}\;\ldots\;y_{i_{k}}\;y_{n+1}\$\;{w_{1}^{\prime\prime}}$

Thus it must be that
$x_{0}\;x_{i_{1}}\;\ldots\;x_{i_{k}}\;x_{n+1}\;=\;y_{0}\;y_{i_{1}}\;\ldots\;y_{i_{k}}\;y_{n+1}$,
which is a solution to the GPCP.

######  Theorem 32.

The CE problem is undecidable for the finite and convergent string rewriting
system $R_{1}$.

######  Lemma 33.

For all $a\in\widehat{\Sigma}$ and strings $Z_{1}$ and $Z_{2}$,
$~{}Z_{1}a\,\downarrow\,Z_{2}a~{}$ if and only if
$~{}Z_{1}\,\downarrow\,Z_{2}$.

######  Proof C.23.

Since $R_{1}$ is convergent, all we need to prove is that if $Z_{1},Z_{2}\in
IRR(R_{1})$ and $a\in\widehat{\Sigma}$, then $Z_{1}a\;\downarrow\;Z_{2}a$ if
and only if $Z_{1}=Z_{2}$.

Let $c\in\widehat{\Sigma}$ such that $Z_{1}c\,\downarrow\,Z_{2}c$ and
$Z_{1}\neq Z_{2}$ where $Z_{1}$ and $Z_{2}$ are irreducible strings. Clearly
either $Z_{1}c$ or $Z_{2}c$ must be reducible.
Thus it has to be that
$c\in\left\\{c_{1},\ldots,c_{n+1}\right\\}\cup\\{\\#_{1},\\#_{2}\\}$. We now
need to consider three cases:

  1. i.

$c\in\left\\{c_{1},\ldots,c_{n}\right\\}$:
The observation of the rules and the set $c$ belongs shows that, $Z_{1}$ and
$Z_{2}$ should end with $\cent_{1}$ or $\cent_{2}$ to make
$Z_{1}c\;\downarrow\;Z_{2}c$. Let $i$ be an index, such that $0\leq i\leq n$
and $Z_{1}$ and $Z_{2}$ can be written as $Z_{1}={Z_{1}^{\prime}}\;\cent_{1}$
and $Z_{2}={Z_{2}^{\prime}}\;\cent_{1}$:

$\displaystyle{Z_{1}^{\prime}}\;\cent_{1}\;c_{i}$
$\displaystyle\rightarrow{Z_{1}^{\prime}}\;x_{i}\;\cent_{1}$ (3)
$\displaystyle{Z_{2}^{\prime}}\;\cent_{1}\;c_{i}$
$\displaystyle\rightarrow{Z_{2}^{\prime}}\;x_{i}\;\cent_{1}$

Since ${Z_{1}^{\prime}},{Z_{2}^{\prime}}\in IRR(R_{1})$, so are
${Z_{1}^{\prime}}\;x_{i}$ and ${Z_{2}^{\prime}}\;x_{i}$, since no left-hand
sides end with either $a$ or $b$. Hence, ${Z_{1}^{\prime}}={Z_{2}^{\prime}}$.

  2. ii.

$c=\\#_{1}$:
Suppose $Z_{1}={Z_{1}^{\prime}}\;{Z_{1}^{\prime\prime}}\;$ and
$Z_{2}={Z_{2}^{\prime}}\;{Z_{2}^{\prime\prime}}\;$ such that
${Z_{1}^{\prime\prime}}$ and ${Z_{2}^{\prime\prime}}$ are the longest suffixes
of $Z_{1}$ and $Z_{2}$ that belong to $\\{a,b\\}^{*}$. Thus:

$\displaystyle{Z_{1}^{\prime}}\;{Z_{1}^{\prime\prime}}\;\\#_{1}$
$\displaystyle\rightarrow^{!}{Z_{1}^{\prime}}\;\\#_{1}\;{Z_{1}^{\prime\prime}}$
(4) $\displaystyle{Z_{2}^{\prime}}\;{Z_{2}^{\prime\prime}}\;\\#_{1}$
$\displaystyle\rightarrow^{!}{Z_{2}^{\prime}}\;\\#_{1}\;{Z_{2}^{\prime\prime}}$

Since ${Z_{1}^{\prime}}\\#_{1}{Z_{1}^{\prime\prime}}$ and
${Z_{2}^{\prime}}\\#_{1}{Z_{2}^{\prime\prime}}$ are irreducible,
${Z_{1}^{\prime}}={Z_{2}^{\prime}}$ and
${Z_{1}^{\prime\prime}}={Z_{2}^{\prime\prime}}$.

  3. iii.

$c=\\#_{2}$:
Follows the same construction as in the previous case, with the only
difference being $\\#_{2}$ instead of $\\#_{1}$.

  4. iv.

$c=c_{n+1}$:
Thus,

$\displaystyle{Z_{1}^{\prime}}\;\cent_{1}\;c_{n+1}$
$\displaystyle\rightarrow{Z_{1}^{\prime}}\;\\#_{1}\;x_{n+1}\;\$$ (5)
$\displaystyle{Z_{2}^{\prime}}\;\cent_{1}\;c_{n+1}$
$\displaystyle\rightarrow{Z_{2}^{\prime}}\;\\#_{1}\;x_{n+1}\;\$$

Since there are no left-hand sides that end with $a$, $b$ or $, we have
${Z_{1}^{\prime}}\;\\#_{1}\downarrow{Z_{2}^{\prime}}\;\\#_{1}$. By the case
(ii) above, we get ${Z_{1}^{\prime}}={Z_{2}^{\prime}}$.

######  Theorem 34.

The CT problem is decidable for the finite and convergent string rewriting
system $R_{1}$.