Solving Trace Equations Using Lexicographical

Normal Forms?

Volker Diekert

Universität Stuttgart,
Institut für Informatik
Breitwiesenstr. 20-22

70565 Stuttgart, Germany

Yuri Matiyasevich

Steklov Institute of Mathematics at
St. Petersburg, Fontanka 27,

St. Petersburg, 191011 Russia

Anca Muscholl

Universität Stuttgart,
Institut für Informatik
Breitwiesenstr. 20-22

70565 Stuttgart, Germany

Abstract

Very recently, Matiyasevich showed that the question whether an equation 
over a trace monoid has a solution or not is decidable. In his proof 
this question is reduced to the solvability of word equations with 
constraints, by induction on the size of the commutation relation. In 
the present paper we give another proof of this result using 
lexicographical normal forms. Our method is a direct reduction of a 
trace equation system to a word equation system with regular 
constraints. We use for this a new result on lexicographical normal 
forms.

?Report Nr. 1997/01, Fakultät Informatik, Universität Stuttgart.

1


1 Introduction

Solving equations is a central topic in various fields of computer 
science, especially concerning unification, as required by automated 
theorem proving or logic programming. An important and deep result has 
been obtained in 1977 by Makanin [10], who showed that the question 
whether an equation over words has a solution or not is decidable. I.e., 
there exists an algorithm deciding for a given equation L = R, where L; 
R 2 (? [ ?)? contain both unknowns from ? and constants from ?, whether 
an assignment ö: ? ! ?? exists, satisfying ö(L) = ö(R). Slightly more 
general, the existential theory of equations over free monoids is 
decidable, i.e., given an existentially quantified, closed first-order 
formula S over atomic predicates of the form L = R and L 6= R, it is 
decidable whether S is valid over a given free monoid. Moreover, adding 
regular constraints, i.e., atomic predicates of the form x 2 C, where C 
is a regular language, preserves decidability [13]. In this paper we 
prove the generalization of Makanin's result to trace monoids. Trace 
monoids have been originally studied in combinatorics [4] as quotients 
of free monoids by partial commutations. A free, partially commutative 
monoid (or trace monoid) is associated to an alphabet ? and a symmetric, 
irreflexive commutation relation I ? ? ? ? as the quotient monoid M (?; 
I) = ??=fab = ba j (a; b) 2 Ig. Trace monoids became meaningful for 
computer science in concurrency theory, where they were introduced by 
Mazurkiewicz [12] in connection with the semantic of labelled Petri 
nets. As a mathematical model traces are simple enough in order to be 
able to generalize many interesting results from free monoids in areas 
as automata theory or logic. However, traces are complex enough in order 
to require in most cases ingenious proof techniques and new ideas. For a 
broad overview of trace theory and related topics see \The Book of 
Traces" [6]. The results obtained so far in the area of equations on 
traces were restricted to equations without constants, i.e. of the form 
L = R with L; R 2 ??, and parametrized solution sets. A reason for this 
consists in the additional inherent difficulty introduced by partial 
commutations. An overview of some results obtained is presented in [5] 
(see also [7]). The decidability of the solvability of equations with 
constants was stated as an important open question. Very recently, 
Matiyasevich showed that the question whether an equation over a trace 
monoid has a solution or not is decidable [11]. In his proof this 
question is reduced to the solvability of word equations with 
constraints by eliminating partial commutativity. The original proof is 
an induction on the

2


size of the commutation relation I. In the present paper we give another 
proof of this result using a new result on lexicographical normal forms. 
Our method is a direct reduction of a trace equation system to a word 
equation system with regular constraints. The result on lexicographical 
normal forms is stated in the Main Lemma of Section 3. Section 4 
contains the reduction from trace equations to word equations. Section 5 
presents a detailed formula for concatenating lexicographical normal 
forms, leading to an estimation of the increase in the number of 
unknowns and equations. We conclude with two remarks concerning the 
parallel complexity of computing lexicographical normal forms.

2 Notations and Preliminaries

An independence alphabet is a pair (?; I), where ? is a finite alphabet 
and I ? ? ? ? is an irreflexive and symmetric relation, called 
independence relation. The complement D = (? ? ?) n I is called 
dependence relation; it is a reflexive and symmetric relation.
With a given independence alphabet (?; I) we associate the trace monoid 
M (?; I). This is the quotient monoid ??= ?I , where ?I denotes the 
congruence being the equivalence relation generated by the set fuabv = 
ubav j (a; b) 2 I; u; v 2 ??g; an element t 2 M (?; I) is called a 
trace, the length jtj of a trace t is given by the length of any 
representing word. By alph(t) we denote the alphabet of a trace t, being 
the set of letters occurring in t. By 1 we denote both the empty word 
and the empty trace. Words v; w 2 ?? are called independent (w.r.t. I), 
if alph(v) ? alph(w) ? I. In this case we simply write (v; w) 2 I or v 2 
I(w) where I(w) for w 2 ?? is a shorthand for fa 2 ? j (a; w) 2 Ig.
The initial alphabet of w 2 ?? is the set init(w) = fa 2 ? j 9w0; w00 2 
?? with w ?I w0 and w0 = aw00g.
A word language L ? ?? is called I-closed if whenever v 2 L and w ?I v 
then we have w 2 L.

3 Lexicographical Normal Forms

Throughout the paper we will suppose that (?; I) denotes an independence 
alphabet, where ? has the cardinality n >= 1. We suppose that ? is 
totally

3


ordered by < and we identify ? with the set f1; : : : ; ng. The order on 
? is extended to the lexicographical order on ??.
A word v 2 ?? is in lexicographical normal form (w.r.t. I and <=) if v 
<= w holds for all w such that v ?I w. Let LNF denote the set of 
lexicographical normal forms, i.e., LNF ? ?? is the set of minimal 
representatives for M (?; I). For v 2 ?? we denote by Lnf(v) the unique 
word w 2 LNF such that w ?I v. We view Lnf as a mapping Lnf: ?? ! LNF.
There is a simple characterization of lexicographical normal forms due 
to Anisimov and Knuth:

Proposition 3.1 ([3]) Let ? be totally ordered by <. Then a word v 2 ?? 
is in lexicographical normal form (w.r.t. I, <=) if and only for every 
factor aub of v with a; b 2 ?, u 2 ?? and (au; b) 2 I we have a < b.

Remark 3.2 Note that the above characterization yields a star-free 
expression for the set of lexicographical normal forms LNF 
(equivalently, a firstorder formula defining the set LNF).

Definition 3.3 Let ? be totally ordered by <.
For ; 6= A ? ? let the height h(A) be h(A) = maxfa j a 2 Ag. Let also 
h(;) = 0. (Thus, h(A) 2 f0; : : : ; ng.)
The height h(v) of a word v 2 ?? is defined as h(v) = h(alph(v)).

Our reduction of trace equations to word equations is based on the 
ability of concatenating lexicographical normal forms in a simple way. 
We give a formula for the product of lexicographical normal forms in the 
Main Lemma below and we will consider it in more details in Section 5. 
First, the following remark is clear:

Remark 3.4 Let m >= 1 and s; t; v; s1; : : : ; sm; t1; : : : ; tm 2 ?? 
be words satisfying the following conditions:

s = s1 ? ? ? sm ;
t ?I t1 ? ? ? tm ;
v = s1t1 ? ? ? smtm ;
tj 2 I(sj+1 ? ? ? sm) for all 1 <= j < m :

Then we have st ?I v.

4


The converse of the previous remark will be stated for lexicographical 
normal forms in the Main Lemma below. It is the crucial correctness 
argument for our reduction from trace equations to word equations. The 
important point is that the value of m can be bounded as a function in 
the size of the alphabet, and that the height decreases in the first m? 
1 factors.

Lemma 3.5 (Main Lemma) Let s; t; v 2 LNF be words in lexicographical 
normal form such that st ?I v.
Let h = h(s) denote the height of s and suppose h > 0.
Then there exist an integer m, 1 <= m <= (n?1)(h?1)
2 + 1, and words s1; : : : ; sm,
t1; : : : ; tm 2 LNF in lexicographical normal form such that the 
following conditions hold: s = s1 ? ? ? sm ;
t ?I t1 ? ? ? tm ;
v = s1t1 ? ? ? smtm ;
si 6= 1; for all 1 < i <= m ;
tj 6= 1 for all 1 <= j < m ;
tj 2 I(sj+1 ? ? ? sm) for all 1 <= j < m ;
h(tj) < h for all 1 <= j < m :

Remark 3.6 Before giving the proof of the Main Lemma, let us note that 
the trace equality st ?I v above cannot be replaced by word equalities 
of type s = s1 ? ? ? sm, t = t1 ? ? ? tm, v = s1t1 ? ? ? smtm. For 
example, consider M (?; I) = fa; b; cg?=fab = ba; bc = cbg and s = c, t 
= ab. Then the lexicographical normal form of st is v = bca.

Proof of the Main Lemma. We have st ?I v with s; t; v 2 LNF and h = h(s) 
> 0. Consider the decomposition of v, v = s1t1 ? ? ? smtm, where m >= 1 
is minimal such that s ?I s1 ? ? ? sm, t ?I t1 ? ? ? tm, and tj 2 I(sj+1 
? ? ? sm) for all j, 1 <= j < m. Clearly, since m is minimal, we have si 
6= 1 and tj 6= 1 for all 1 < i <= m, 1 <= j < m. Moreover, the words si; 
tj are in lexicographical normal form.
Let us first show that s = s1 ? ? ? sm. Assume aub is a factor of s1 ? ? 
? sm with a; b 2 ?, u 2 ?? and b 2 I(au). If aub is a factor of some si, 
then a < b follows by Prop. 3.1 and we are done. Otherwise let i < j be 
such that si 2 ??au0, sj 2 u00b?? and u = u0si+1 ? ? ? sj?1u00. Since tk 
2 I(sj) for k < j we obtain b 2 I(au0si+1ti+1 ? ? ? sj?1tj?1u00), hence 
a < b due to v being in lexicographical normal form. Thus s1 ? ? ? sm is 
in lexicographical normal form, again by Prop. 3.1.

5


Suppose that 1 <= j < m and let b denote the first letter of sj+1. Let a 
2
alph(tj), i.e. tj = uau0 for some words u; u0. Then au0b is a factor of 
v 2 LNF satisfying b 2 I(au0), thus we have a < b. Therefore h(tj) < 
h(b) <= h for every 1 <= j < m.
Finally, assume by contradiction that m > (n ? 1)(h ? 1)=2 + 1. Let bi; 
aj denote the first letter of si, tj respectively, 1 < i <= m, 1 <= j < 
m. Consider the chain of alphabets I(s2 ? ? ? sm) ? I(s3 ? ? ? sm) ? ? ? 
? ? I(sm). Note that we have I(s2 ? ? ? sm) 6= ; due to t1 6= 1, and 
also I(sm) 6= ? due to sm 6= 1. Therefore by the pigeon-hole principle 
there exist some indices i; j with j ? i >= (h ? 1)=2 satisfying I(si+1 
? ? ? sm) = I(sj+1 ? ? ? sm). Consider the factor tisi+1ti+1 ? ? ? 
tjsj+1 of v. Note that (tk; sl) 2 I holds for every k, l such that i <= 
k; l ? 1 <= j, since tk 2 I(sk+1 ? ? ? sm) = I(si+1 ? ? ? sm). 
Therefore, v 2 LNF implies ai < bi+1 < ai+1 < ? ? ? < aj < bj+1 and we 
obtain h(s) >=
h(bj+1) >= 2(j ? i + 1) > h, a contradiction. 2

4 Trace Equation Systems

Definition 4.1 Let ? denote a finite alphabet and ? a finite set of 
unknowns, ? \ ? = ;.

i) A word equation over ? and ? has the form L = R, with L; R 2
(? [ ?)?.

ii) An assignment for an equation over ? and ? is a mapping ö: ? ! ?? 
being extended in a natural way to a homomorphism ö: (?[?)? ! ??, by öj? 
= id?.

A solution for the equation L = R is an assignment ö satisfying the 
equality ö(L) = ö(R) in ??.

Makanin [10] showed in 1977 that the question whether a word equation 
has a solution or not is decidable. Moreover, the solvability of a 
system of word equations can be reduced by well-known techniques to the 
solvability of a single equation. The problem can also be generalized by 
introducing regular constraints for the unknowns, i.e. regular sets Cx ? 
?? for x 2 ?. Here, a solution ö for an equation is required to satisfy 
ö(x) 2 Cx for all x. It has been shown by Schulz [13] that the 
solvability of word equations with regular constraints remains 
decidable. We are going to show that this more general result 
generalizes to traces.

6


Definition 4.2 Let (?; I) denote an independence alphabet and ? a finite 
set of unknowns, ? \ ? = ;.

i) A trace equation over (?; I) and ? has the form L ? R, with L; R 2 (? 
[ ?)?.

A solution for the equation L ? R is an assignment ö: ? ! ?? satisfying 
ö(L) ?I ö(R).

ii) A system of trace equations is a formula built with the connectives 
and (&), or (_), not (:) over atomic predicates of the form L ? R (trace 
equation) and x 2 C (constraint), where C ? ?? denotes an I-closed 
regular language.

A solution for a system S over (?; I); ? is an assignment ö: ? ! ?? such 
that S evaluates to true when the atomic predicates L ? R, x 2 C are 
replaced by the truth value of ö(L) ?I ö(R), ö(x) 2 C, respectively.

Remark 4.3 Later we will deal simultaneously with trace and word 
equations, so we distinguish notationally between L = R for a word 
equation, whereas L ? R denotes a trace equation. The difference is that 
equality under an assignment is interpreted in the free monoid ??, resp. 
in the trace monoid M (?; I).

Remark 4.4 A system of word equations (with regular constraints) is just 
a special case of Def. 4.2 where one takes I = ;. By Makanin's result 
(see the remarks after Def. 4.1), Schulz' generalization and the fact 
that negations can be eliminated, we note that the question whether a 
system of word equations has a solution or not is decidable.

Remark 4.5 Adding arbitrary regular constraints to a system of trace 
equations makes the question of solvability undecidable. This is due to 
the fact that the solvability of the equation x ? y with x 2 C, y 2 C 0 
is equivalent to the non-emptiness of the intersection fw 2 ?? j w ?I v 
for some v 2 Cg \ fw 2 ?? j w ?I v for some v 2 C 0g. For regular 
languages C; C 0 this last question is known to be undecidable, see [1].

Remark 4.6 Similar to the word case, the solvability of a trace 
equations system could be reduced to the solvability of a single trace 
equation (with additional constraints).

7


The aim of this section is to reduce the solvability problem for trace 
equations to word equations with regular constraints. We will give a 
direct proof using lexicographical normal forms to show the following

Theorem 4.7 ([11]) Let S be a trace equation system over (?; I) and ?. 
Then a set ?0 ? ? of unknowns and a system of word equations S 0 over ?; 
?0 can be effectively constructed, such that S is solvable if and only 
if S 0 is solvable.

Corollary 4.8 The following problem is decidable:

Instance: An independence alphabet (?; I), a finite set of unknowns ?, 
and a trace equation system S over (?; I); ?.

Question: Does S have a solution?

4.1 Basic reductions

For a given trace equation system S we first eliminate constants by 
introducing new unknowns xa and constraints xa 2 fag, for a 2 ?. Then we 
replace a by xa in each equation L ? R of S. Clearly, for every solution 
ö of S the assignment ö0 = ö [ fxa 7! a j a 2 ?g is a solution for S 0. 
Conversely, every solution ö0 for S 0 yields a solution ö = ö0j? for S.
Hence, without loss of generality atomic predicates are of the form

L ? R where L; R 2 ?? :

Furthermore, we may assume that the given system is written in 
disjunctive normal form. Then we replace every negation not(L ? R) by 
the following formula

9A; A0; B; B0 ? ? : (A \ A0 = ; & B [ B0 6= ; &

L ? xy & R ? xz &

init(y) = A & init(z) = A0 & alph(y) = B & alph(z) = B0) (1)

where x; y; z denote new unknowns. Clearly, constraints of the form 
init(x) = A or alph(x) = A, A ? ?, can be expressed by I-closed regular 
languages. Suppose that ö is a solution for S and ö(L) 6?I ö(R). Let s 
denote the longest word such that for some t; u 2 ??:

ö(L) ?I st and ö(R) ?I su :

8


Due to the maximality of s we obtain init(t) \ init(u) = ;. Moreover, tu 
6= 1, since st 6?I su. Hence, ö0 = ö [ fx 7! s; y 7! t; z 7! ug is a 
solution for the new subformula (1). Conversely, for every solution ö0 
of (1) one has ö0(x)ö0(y) 6?I ö0(x)ö0(z), hence ö0(L) 6?I ö0(R).
Since the set of I-closed regular languages forms an effective boolean 
algebra (as the family of recognizable subsets of a monoid [9]) we may 
also suppose that the formula contains no negated constraints, i.e. no 
formula of type not(x 2 C).
Moreover, it suffices to consider trace equations of the form x1 ? ? ? 
xk ? y1 ? ? ? yl with k >= l > 0, xi; yj 2 ?. (The equation x1 ? ? ? xk 
? 1 and the occurrences of xi can be deleted from all equations, adding 
the constraints alph(xi) = ;.)

4.2 From traces to words

The main idea for reducing trace equations to word equations will 
consist in replacing a trace equation L ? R by some word equations L1 = 
R1; : : : ; Lk = Rk with additional constraints and unknowns. Moreover, 
for every solution ö for L ? R the mapping Lnf ffi ö: ? ! ?? ! LNF can 
be extended to a solution for the equations L1 = R1; : : : ; Lk = Rk. 
Vice versa, each solution for the new equations will also be a solution 
for L ? R when restricted to its unknowns.
This reduction actually goes by a chain of additional trace equations. 
By choosing an appropriate ordering we will show that the reduction 
process terminates yielding a system of word equations (with 
constraints). We will consider in the following formulas S(T; W;C) in 
disjunctive normal form with atomic predicates from some finite sets T; 
W;C, containing no negations. T will denote a set of trace equations, W 
a set of word equations and C = fx 2 Cx j x 2 ?g a set of constraints, 
where each Cx is an I-closed regular language. Moreover, every L ? R in 
T has the form x1 ? ? ? xk ? y1 ? ? ? yl with k >= l >= 1, xi; yj 2 ?. A 
solution for S(T; W;C) is an assignment ö: ? ! ?? which makes the 
formula evaluate to true when (L ? R) from T , (L = R) from W and x 2 Cx 
from C are replaced by the truth value of ö(L) ?I ö(R), ö(L) = ö(R), and 
ö(x) 2 Cx, respectively.

Definition 4.9 A formula S(T; W;C) as above is called normalized if for 
every solution ö for S the mapping Lnf ffi ö is a solution for S, too.

9


Remark 4.10 Note that a formula S(T; ;; C) with I-closed constraints C 
is always normalized.

Remark 4.11 Suppose S = S(T; W;C) is normalized and let x ? y belong to 
T , where x; y 2 ?. Consider the new formula S 0 = S 0(T 0; W 0; C) 
obtained from S by replacing every occurrence of x ? y by x = y and 
letting T 0 = T n fx ? yg, W 0 = W [ fx = yg. Then S is solvable if and 
only if S 0 is solvable. Note that a solution for S 0 is a solution for 
S, too. However, the converse is true only because S is a normalized 
system. Without this assumption about S it cannot be guaranteed that 
every solution for S also solves S 0. Moreover, S 0 is a normalized 
system, too.

Example 4.12 Consider the trace equation system S = (fx ? yg; fx = ab; y 
= bag; ;) given as the conjunction (x ? y) & (x = ab) & (y = ba), where 
(a; b) 2 I. Then S is not normalized, but of course it has a solution. 
However, replacing x ? y by the word equation x = y yields a system with 
no solution.

Proof of Thm. 4.7. Recall that an equation system with I-closed 
constraints S = S(T; ;; fx 2 Cxgx2?) over (?; I); ? is a normalized 
system. As previously noted it suffices to consider a formula S with 
trace equations of the form
x1 ? ? ? xk ? y1 ? ? ? yl; k >= l >= 1; (k; l) 6= (1; 1) : (2)

We suppose without loss of generality that for all unknowns x 2 ? some 
Ax ? ? exists such that h(Ax) > 0, and x 2 Cx implies alph(x) = Ax, for 
all x. Then h(x) will mean h(Ax). (In fact, we could also assume that 
alph(x) ? Ax. The obvious modifications needed below are left to the 
reader.) Moreover, let S be a conjunction of trace equations as in (2), 
of word equations and of I-closed regular constraints x 2 Cx.
We define the weight of a trace equation x1 ? ? ? xk ? y1 ? ? ? yl as in 
(2) as the triple of natural numbers (l; h(x1 ? ? ? xk?1); k) and we 
consider the lexicographical ordering on N ? N ? N . We will show in the 
following that every such trace equation can be replaced by a formula 
over word equations and trace equations of lower weight, together with 
some additional constraints. Concretely, we apply the following rules.

Rule 1: Suppose l > 1 and let z denote a new unknown. Then we replace 
the equation x1 ? ? ? xk ? y1 ? ? ? yl by

x1 ? ? ? xk ? z & y1 ? ? ? yl ? z & alph(z) = [ki=1Axi :

10


Rule 2: Suppose l = 1 and k > 2, and let z denote a new unknown. Then we 
replace the equation x1 ? ? ? xk ? y1 by

x1z ? y1 & x2 ? ? ? xk ? z & alph(z) = [ki=2Axi :

Rule 3: Suppose l = 1 and k = 2 and, in order to simplify notation, 
consider the equation xy ? z (rather than uniformly x1x2 = y1). 
Moreover, let h = h(x) denote the height of x.
We replace xy ? z by the disjunction of the word equation

xy = z (3)

and of formulas of the type

x = x1 ? ? ? xm & y ? y1 ? ? ? ym & z = x1y1 ? ? ? xmym &

alph(x1) = A1 & ? ? ? & alph(xm) = Am &

alph(y1) = B1 & ? ? ? & alph(ym) = Bm ; (4)

where xi; yj are new unknowns and the disjunction is taken over all 
values of m such that 1 < m <= (n? 1)(h?1)=2+1 and over all alphabets 
A1; : : : ; Am, B1; : : : ; Bm ? ? such that

Ai 6= ; for all 1 < i <= m; and

1 <= h(Bj) < h for all 1 <= j < m; and

Bj ? Ai ? I for all 1 <= j < i <= m; and

A1 [ ? ? ? [ Am = alph(x); and

B1 [ ? ? ? [ Bm = alph(y) : (5)

The word equation xy = z in (3) corresponds to the case m = 1 in (4) 
(this is in particular the case when h = 1 in (5)). It is actually the 
main case where the number of trace equations in S decreases.
Let S 0 denote the formula obtained from S by applying one of the three 
rules described above. Note that none of the rules adds negations.

Lemma 4.13 Let S be a normalized equation system. Then the new system S 
0 is normalized, too. Moreover, S 0 is solvable if and only if S is 
solvable.

Proof. The claim is easily seen for the first two rules above, since 
there is a natural bijection between the set of solutions of S and of S 
0, respectively.

11


Clearly, if S 0 has been obtained from S by the third rule, then every 
solution for S 0 is a solution for S, too, see Rem. 3.4. Therefore, let 
us consider an equation xy ? z in S and a solution ö: ? ! ?? for S. Then 
ö0 = Lnf ffi ö is also solution for S, since S is normalized. We show 
that ö0 can be extended to a solution for S 0. Let s = ö0(x), t = ö0(y) 
and v = ö0(z). Hence, st ?I v with s; t; v 2 LNF. If h(s) = 1, then in 
the Main Lemma we have m = 1, hence v = st. Therefore ö0 is a solution 
of the new system S 0. Suppose that st ?I v with s; t; v 2 LNF, h(s) = h 
> 1. Then some m, 1 <= m <= (n?1)(h?1)=2+1, and words s1; : : : ; sm, 
t1; : : : ; tm exist, satisfying the conditions of the Main Lemma. With 
ö0(xi) = si, ö0(yj) = tj it is easily verified that ö0 is a solution for 
S 0.
The relation between the solution set of S and the solution set of S 0, 
together with the fact that S is normalized, imply that S 0 is 
normalized, too. This shows the lemma. 2

Finally, note that the new trace equation y1 ? ? ? ym ? y in (4) has 
lower weight than xy ? z due to h(y1 ? ? ? ym?1) < h = h(x). Hence the 
reduction rules establish a noetherian rewriting system on trace 
equation systems. Applying the rules as long as possible we end with a 
system of word equations S 0 = (;; W 0; C 0). 2

5 Computing Lexicographical Normal Forms

The aim of this section is to give a formula for computing the product 
of lexicographical normal forms. This yields an alternative proof of 
Thm. 4.7 and the so far best known upper bound on the number of new 
unknowns needed for the reduction. We conclude the section with two 
remarks concerning the parallel complexity of computing lexicographical 
normal forms.

Definition 5.1 Let ?I be a relation on (??)? defined as

(x1; : : : ; xm) ?I (x01; : : : ; x0m0)

if m = m0 and there exists some i, 1 <= i < m such that

xj = x0j for all 1 <= j <= m; j =2 fi; i + 1g; and

(xi; xi+1) = (x0i+1; x0i) and (xi; xi+1) 2 I :

By ßI we denote the equivalence relation generated on (??)? by ?I .

12


Let x 2 ??, by abuse of language we write (x1; : : : ; xm) ßI x if some 
words x01; : : : ; x0m exist such that

(x1; : : : ; xm) ßI (x01; : : : ; x0m) and x = x01 ? ? ? x0m :

Theorem 5.2 Let s; t; v 2 LNF be words in lexicographical normal form 
such that st ?I v.
Then there exist positive integers m; p with m <= (n?1)2
2 + 1, p <= nnn! such
that
s = s1 ? ? ? sm ;
t = t1 ? ? ? tp ;
(s1; : : : ; sm; t1; : : : ; tp) ßI v ;

for some words s1; : : : ; sm; t1; : : : ; tp 2 ??.

Proof. Let h = h(s) denote the height of s. Let m(h); p(h) denote the 
minimal integers such that

s = s1 ? ? ? sm(h) ;
t = t1 ? ? ? tp(h) ;
(s1; : : : ; sm(h); t1; : : : ; tp(h)) ßI v ;

for some words si; tj. Note that m(h); p(h) <= jvj. For h = 0 we have s 
= 1, thus m(0) = p(0) = 1, which satisfies the theorem.
For h >= 1 we will show by induction on h that m(h) <= (n ? 1)(h ? 1)=2 
+ 1 and p(h) <= nhh!, thereby proving the theorem.
Let h >= 1. By the Main Lemma there exist an integer m <= (n?1)(h?1)=2+1 
and words s1; : : : ; sm, t1; : : : ; tm in lexicographical normal form 
satisfying

s = s1 ? ? ? sm ;

t ?I t1 ? ? ? tm ;

v = s1t1 ? ? ? smtm ;

si 6= 1; tj 6= 1 for 1 < i <= m; 1 <= j < m ;

tj 2 I(sj+1 ? ? ? sm) and h(tj) < h for 1 <= j < m : (6)

If h = 1, then m = 1 in (6), so we can take m(h) = p(h) = 1, since t = 
t1 2 LNF, which satisfies the claim. Hence let h; m >= 2. Let ?t1 = t1 
and ?ti = Lnf(?ti?1ti) for i = 2; : : : ; m. Clearly, ?tm = t, h(?ti) < 
h for 1 <= i < m and
?ti?1ti ?I ?ti; for 1 < i <= m: (7)

13


Now we can apply the induction hypothesis to each of the (m?1) 
equivalences (7) obtaining
t ßI (t01; : : : ; t0p) ; (8)

for some p <= (m ? 1)[m(h ? 1) + p(h ? 1)], some words t01; : : : ; t0p 
and some integers 1 = l0 < l1 < ? ? ? < lm = p + 1 such that

ti = t0li?1 ? ? ? t0li?1 for every 1 <= i <= m : (9)

The above claim can be verified by noting that

t ßI (t01; : : : ; t0i; : : : ; t0j ; : : : ; t0q) and t0i ? ? ? t0j ßI 
(v1; : : : ; vk)

implies that
t ßI (t01; : : : ; t0i?1; v01; : : : ; v0l; t0j+1; : : : ; t0q) ;

for some l <= j ? i + k and v01; : : : ; v0l 2 ??, such that v01 ? ? ? 
v0l = v1 ? ? ? vk and each v0q is a factor of some vr.
Hence, we obtain from (8), (9) for suitable words t001; : : : ; t00p:

t = t001 ? ? ? t00p ;

v ßI (s1; : : : ; sm; t1; : : : ; tm) ßI (s1; : : : ; sm; t01; : : : ; 
t0p)

ßI (s1; : : : ; sm; t001; : : : ; t00p) :

Hence by the induction hypothesis we get

p(h) <= (m ? 1)[m(h ? 1) + p(h ? 1)]

<= (n ? 1)(h ? 1)=2 [(n ? 1)(h ? 2)=2 + 1 + nh?1(h ? 1)!]

<= nhh! ;

which concludes the proof. 2

Remark 5.3 We can also use Thm. 5.2 in order to prove the main result, 
Thm. 4.7. Recall that the main difficulty consists in replacing a trace 
equation of the form xy ? z, where x; y; z 2 ?. By Thm. 5.2 we simply 
replace such an equation xy ? z by a disjunction over clauses of the 
form

x = x1 ? ? ? xm & y = y1 ? ? ? yp &
z = zß(1) ? ? ? zß(m+p) & alph(xi) = Ai & alph(yj) = Bj ;

14


for all 1 <= m <= (n?1)2
2 + 1, 1 <= p <= nnn!, ß 2 SIm+p and Ai; Bj ? ?. Here
xi; yj denote new variables and zi = xi for 1 <= i <= m, resp. zm+j = yj 
for 1 <= j <= p. SIm+p denotes the set of permutations over f1; : : : ; 
m + pg such that for i < j the inequality ß(i) > ß(j) implies (zi; zj) 2 
I. This reduction of a single trace equation to word equations roughly 
yields an increase in the number of word equations by (N+2)!2n(N+1), 
where N = nnn!+(n?1)2=2+1. Hereby we need N additional unknowns.

We conclude this section with two remarks concerning the parallel 
complexity of computing lexicographical normal forms. We consider 
uniform circuit complexity classes like AC0 and TC0. Let f : ?? ! ?? be 
a function such that jf(w)j = p(jwj) for some polynomial p and every w 2 
??. Let k >= 0. Then f is ACk-computable if there is a family (Cn)n>=0 
of polynomial-size circuits of depth O(logk(n)) with AND and OR gates of 
unbounded fanin/out and unary NOT gates, such that Cjwj computes f(w) 
for all w 2 ??. A function f is TCk-computable if there is a family of 
circuits as above which in addition to AND, OR and NOT gates contain 
MAJORITY gates of unbounded fan-in/out. A MAJORITY gate yields 1 if and 
only if more than half of its inputs are 1. In order to be able to deal 
with arbitrary alphabets ? one usually assumes that the circuits have 
special input/output gates testing x = a for each input position x and 
letter a 2 ? (analogously for the outputs). Uniformity means that given 
n >= 0 (a fixed coding of) the circuit Cn can be easily computed (e.g. 
in logarithmic space). It is not very hard to verify that ACk ? TCk ? 
ACk+1, k >= 0. For more details about circuit complexity see e.g. [14]. 
We state the results below without proofs, which will appear elsewhere. 
With Thm. 5.2 we obtain

Corollary 5.4 Let (?; I) denote an independence alphabet. Then we can 
compute Lnf(st) on input s; t 2 LNF in uniform AC0.

Proof. Since m; p in Thm. 5.2 are bounded by the size of the alphabet we 
can build a subcircuit for each factorization s = s1 ? ? ? sm, t = t1 ? 
? ? tp and each permutation in SIm+p. Moreover, by Prop. 3.1 we can test 
whether a given word is in lexicographical normal form in AC0, too. 2

We could apply Cor. 5.4 in order to compute the function Lnf in AC1. 
However, we can do better: the mapping Lnf: ?? ! LNF is computable in 
uniform TC0. This result can be compared with the fact that the 
equivalence s ?I t can be verified in uniform TC0, too (see [2]).

15


Proposition 5.5 Let (?; I) denote an independence alphabet. Then we can 
compute Lnf(s) on input s 2 ?? in uniform TC0.

Proof. For w 2 ?+ and 1 <= i; j <= jwj let lex(i; j) denote the 
predicate which is satisfied by w if and only if the ith position of w 
precedes the jth position in the lexicographical normal form of w, 
Lnf(w). Then lex(i; j) is first-order definable, see [8, Prop. 3]. But 
first-order definable predicates are AC0-computable (see e.g. [14] for 
more details about the relation between circuit complexity and 
first-order logic). Finally, the ith position of a word w occurs as the 
jth position of Lnf(w) if and only if j = #fk j lex(k; i)g + 1. The last 
statement is easily seen to be checkable in TC0. 2

References

[1] IJ. J. Aalbersberg and H. J. Hoogeboom. Characterizations of the 
decidability of some problems for regular trace languages. Mathematical 
Systems Theory, 22:1{19, 1989.

[2] C. ?Alvarez and J. Gabarr?o. The parallel complexity of two problems 
on concurrency. Information Processing Letters, 38:61{70, 1991.

[3] A. V. Anisimov and D. E. Knuth. Inhomogeneous sorting. International 
Journal of Computer and Information Sciences, 8:255{260, 1979.

[4] P. Cartier and D. Foata. Probl?emes combinatoires de commutation et 
r?earrangements. Number 85 in Lecture Notes in Mathematics. Springer, 
Berlin-Heidelberg-New York, 1969.

[5] C. Choffrut. Combinatorics in trace monoids I. In V. Diekert and G. 
Rozenberg, editors, The Book of Traces, chapter 3, pages 71{82. World 
Scientific, Singapore, 1995.

[6] V. Diekert and G. Rozenberg, editors. The Book of Traces. World 
Scientific, Singapore, 1995.

[7] C. Duboc. On some equations in free partially commutative monoids. 
Theoretical Computer Science, 46:159{174, 1986.

[8] W. Ebinger and A. Muscholl. Logical definability on infinite traces. 
Theoretical Computer Science, 154:67{84, 1996.

16


[9] S. Eilenberg. Automata, Languages, and Machines, volume A. Academic 
Press, New York and London, 1974.

[10] G. S. Makanin. The problem of solvability of equations in a free 
semigroup. Math. Sbornik, 103:147{236, 1977. English transl. in Math. 
USSR Sbornik 32 (1977).

[11] Yu. Matiyasevich. Reduction of trace equations to word equations, 
1996. Talk given at the \Colloquium on Computability, Complexity, and 
Logic", 5./6. December 1996, Institut für Informatik, Universität 
Stuttgart, Germany.

[12] A. Mazurkiewicz. Concurrent program schemes and their 
interpretations. DAIMI Rep. PB 78, Aarhus University, Aarhus, 1977.

[13] K. U. Schulz. Makanin's algorithm for word equations | Two 
improvements and a generalization. In K. U. Schulz, editor, Word 
Equations and Related Topics, number 572 in Lecture Notes in Computer 
Science, pages 85{150, Berlin-Heidelberg-New York, 1991. Springer.

[14] H. Straubing. Finite automata, formal logic, and circuit 
complexity. Birkhäuser, 1994.

17