Solving Trace Equations Using Lexicographical Normal Forms

Volker Diekert^{1}, Yuri Matiyasevich^{2}^{⋆}, and Anca Muscholl^{1}

1 Institut für Informatik, Universität Stuttgart, Breitwiesenstr. 20-22, 70565 Stuttgart, Germany 2 Steklov Institute of Mathematics at St.Petersburg Fontanka 27, St. Petersburg, 191011 Russia

Abstract. Very recently, the second author showed that the question whether an equation over a trace monoid has a solution or not is decidable [11,12]. In the original 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, using a new result on lexicographical normal forms.

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. A celebrated result of Makanin [10] states that the question whether an equation over words has a solution or not is decidable: There exists an algorithm deciding for a given equation L = R, where L, R ∈ (Ω ∪ Σ)^{∗} 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 ≠ 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 ∈ C, where C is a regular language, preserves decidability [14]. In this paper we prove the generalization of Makanin’s result to trace monoids, which were originally studied in combinatorics [4]. They became meaningful for computer science in concurrency theory, where they were introduced by Mazurkiewicz [13] in connection with the semantics of labelled Petri nets. For an overview of trace theory and related topics see “The Book of Traces” [7]. Most results obtained so far in the area of equations on traces were restricted to equations without constants, see [8,5]. The decidability of the solvability of equations with constants was stated as an important open question.

⋆ This work was done during a stay at the University of Stuttgart.

2 Notations, Preliminaries and Lexicographical Normal Forms

An independence alphabet is a pair (Σ, I), where Σ is a finite alphabet and I ⊆ Σ ×Σ is an irreflexive and symmetric relation, called independence relation. With a given independence alphabet (Σ, I) we associate the trace monoid 𝕄(Σ, I). This is the quotient monoid Σ^{∗}/≡_{I}, where ≡_{I} denotes the congruence being the equivalence relation generated by the set {uabv = ubav | (a, b) ∈ I, u, v ∈ Σ^{∗}}; an element t ∈ 𝕄(Σ, I) is called a trace, the length |t| 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 ∈ Σ^{∗} are called independent (w.r.t. I), if alph(v) × alph(w) ⊆ I. In this case we simply write (v, w) ∈ I or v ∈ I(w) where I(w) for w ∈ Σ^{∗} is a shorthand for {a ∈ Σ | {a} × alph(w) ⊆ I}. The initial alphabet of w ∈ Σ^{∗} is the set init(w) = {a ∈ Σ | ∃w′, w′′ ∈ Σ^{∗} with w ≡_{I} w′ and w′ = aw′′}. A word language L ⊆ Σ^{∗} is called I-closed if whenever v ∈ L and w ≡_{I} v then we have w ∈ L.

Throughout the paper we will suppose that (Σ, I) denotes an independence alphabet, where Σ has the cardinality n ≥ 1. We suppose that Σ is totally ordered by < and we identify Σ with the set {1, …, n}. The order on Σ is extended to the lexicographical order on Σ^{∗}. A word v ∈ Σ^{∗} 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 𝕄(Σ, I). For v ∈ Σ^{∗} we denote by lex(v) the unique word w ∈ LNF such that w ≡_{I} v. We view lex as a mapping lex : Σ^{∗} → LNF. There is a simple characterization of lexicographical normal forms due to Anisimov and Knuth:

Proposition 1 ([3]). Let Σ be totally ordered by <. Then a word v ∈ Σ^{∗} is in lexicographical normal form (w.r.t. I, <) if and only for every factor aub of v with a, b ∈ Σ, u ∈ Σ^{∗} and (au, b) ∈ I we have a < b.

Definition 2. Let Σ be totally ordered by <. For ∅ ≠ A ⊆ Σ let the height h(A) be h(A) = max{a | a ∈ A}. Let also h(∅) = 0. (Thus, h(A) ∈ {0, …, n}.) The height h(v) of a word v ∈ Σ^{∗} is defined as h(v) = h(alph(v)).

Remark 3. Let m ≥ 1 and s, t, v, s_{1}, …, s_{m}, t_{1}, …, t_{m} ∈ Σ^{∗} be words satisfying the following conditions:

s = s_{1} ⋯ s_{m} ,
t ≡_{I} t_{1} ⋯ t_{m} ,
v = s_{1}t_{1} ⋯ s_{m}t_{m} ,
t_{j} ∈ I(s_{j+1} ⋯ s_{m}) for all 1 ≤ j < m .

Then we have st ≡_{I} v.

The previous remark is clear and its converse 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 (given below) can be bounded as a function in the size of the alphabet, and that the height decreases.

Lemma 4 (Main Lemma). Let s, t, v ∈ 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 ≤ \frac{(n−1)(h−1)}{2} + 1, and words s_{1}, …, s_{m}, t_{1}, …, t_{m} ∈ LNF in lexicographical normal form such that the following conditions hold:

s = s_{1} ⋯ s_{m} ,
t ≡_{I} t_{1} ⋯ t_{m} ,
v = s_{1}t_{1} ⋯ s_{m}t_{m} ,
s_{i} ≠ 1, for all 1 < i ≤ m ,
t_{j} ≠ 1 for all 1 ≤ j < m ,
t_{j} ∈ I(s_{j+1} ⋯ s_{m}) for all 1 ≤ j < m ,
h(t_{j}) < h for all 1 ≤ j < m .

Remark 5. 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 = s_{1} ⋯ s_{m}, t = t_{1} ⋯ t_{m}, v = s_{1}t_{1} ⋯ s_{m}t_{m}. For example, consider 𝕄(Σ, I) = {a, b, c}^{∗}/{ab = ba, bc = cb} 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 ∈ LNF and h = h(s) > 0. Consider the decomposition of v, v = s_{1}t_{1} ⋯ s_{m}t_{m}, where m ≥ 1 is minimal such that s ≡_{I} s_{1} ⋯ s_{m}, t ≡_{I} t_{1} ⋯ t_{m}, and t_{j} ∈ I(s_{j+1} ⋯ s_{m}) for all j, 1 ≤ j < m. Clearly, since m is minimal, we have s_{i} ≠ 1 and t_{j} ≠ 1 for all 1 < i ≤ m, 1 ≤ j < m. Moreover, the words s_{i}, t_{j} are in lexicographical normal form. Let us first show that s = s_{1} ⋯ s_{m}. Assume aub is a factor of s_{1} ⋯ s_{m} with a, b ∈ Σ, u ∈ Σ^{∗} and b ∈ I(au). If aub is a factor of some s_{i}, then a < b follows by Prop. 1 and we are done. Otherwise let i < j be such that s_{i} ∈ Σ^{∗}au′, s_{j} ∈ u′′bΣ^{∗} and u = u′s_{i+1} ⋯ s_{j−1}u′′. Since t_{k} ∈ I(s_{j}) for k < j we obtain b ∈ I(au′s_{i+1}t_{i+1} ⋯ s_{j−1}t_{j−1}u′′), hence a < b due to v being in lexicographical normal form. Thus s_{1} ⋯ s_{m} is in lexicographical normal form, again by Prop. 1, and it follows that s = s_{1} ⋯ s_{m}. Suppose that 1 ≤ j < m and let b denote the first letter of s_{j+1}. Let a ∈ alph(t_{j}), i.e. t_{j} = uau′ for some words u, u′. Then au′b is a factor of v ∈ LNF satisfying b ∈ I(au′), thus we have a < b. Therefore h(t_{j}) < h(b) ≤ h for every 1 ≤ j < m. Finally, assume by contradiction that m > (n − 1)(h − 1)/2 + 1. Let b_{i}, a_{j} denote the first letter of s_{i}, t_{j} respectively, 1 < i ≤ m, 1 ≤ j < m. Consider the chain of alphabets I(s_{2} ⋯ s_{m}) ⊆ I(s_{3} ⋯ s_{m}) ⊆ ⋯ ⊆ I(s_{m}). Note that we have I(s_{2} ⋯ s_{m}) ≠ ∅ due to t_{1} ≠ 1, and also I(s_{m}) ≠ Σ due to s_{m} ≠ 1. Therefore by the pigeon-hole principle there exist some indices 1 ≤ i, j < m with j − i ≥ (h − 1)/2 satisfying I(s_{i+1} ⋯ s_{m}) = I(s_{j+1} ⋯ s_{m}). Consider the factor t_{i}s_{i+1}t_{i+1} ⋯ t_{j}s_{j+1} of v. Note that (t_{k}, s_{l}) ∈ I holds for every k, l such that i ≤ k, l − 1 ≤ j, since t_{k} ∈ I(s_{k+1} ⋯ s_{m}) = I(s_{i+1} ⋯ s_{m}). Therefore, v ∈ LNF implies a_{i} < b_{i+1} < a_{i+1} < ⋯ < a_{j} < b_{j+1} and we obtain h(s) ≥ h(b_{j+1}) ≥ 2(j − i + 1) > h, a contradiction.

3 Trace Equation Systems

Definition 6. Let Ω denote a finite set of unknowns with Σ ∩ Ω = ∅.

i) A word equation over Σ and Ω has the form L = R, with L, R ∈ (Σ ∪ Ω)^{∗}. ii) An assignment for an equation over Σ and Ω is a mapping σ: Ω → Σ^{∗}

being extended in a natural way to a homomorphism σ: (Σ ∪ Ω)^{∗} → Σ^{∗}, by σ|_{Σ} = 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 C_{x} ⊆ Σ^{∗} for x ∈ Ω. Here, a solution σ for an equation is required to satisfy σ(x) ∈ C_{x} for all x. It has been shown by Schulz [14] that the solvability of word equations with regular constraints remains decidable. We are going to show that this more general result generalizes to traces.

Definition 7. 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 ∈ (Σ ∪ Ω)^{∗}. 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 ∈ 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 ∈ C are replaced by the truth value of σ(L) ≡_{I} σ(R), σ(x) ∈ C, respectively.

Remark 8. 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 𝕄(Σ, I).

Remark 9. A system of word equations (with regular constraints) is just a special case of Def. 7 where one takes I = ∅. Since negations can be eliminated (see also 3.1), we note that the question whether a system of word equations has a solution or not is decidable.

Remark 10. Adding arbitrary (i.e., not I-closed) 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 ∈ C, y ∈ C′ is equivalent to the non-emptiness of the intersection {w ∈ Σ^{∗} | w ≡_{I} v for some v ∈ C} ∩ {w ∈ Σ^{∗} | w ≡_{I} v for some v ∈ C′}. For regular languages C, C′ this last question is known to be undecidable, see [1].

Remark 11. 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). However, this would be of no use here.

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 12 ([11,12]). Let S be a trace equation system over (Σ, I) and Ω. Then a set Ω′ ⊇ Ω of unknowns and a system of word equations S′ over Σ, Ω′ can be effectively constructed, such that S is solvable if and only if S′ is solvable.

Corollary 13. It is decidable whether a system of trace equations has a solution.

3.1 Basic Reductions

For a given trace equation system S we first eliminate constants by introducing new unknowns x_{a} and constraints x_{a} ∈ {a}, for a ∈ Σ. Then we replace a by x_{a} in each equation L ≡ R of S. Hence, without loss of generality atomic predicates are of the form L ≡ R, where L, R ∈ Ω^{∗}. Furthermore, we may assume that the given system is written in disjunctive normal form. Then we replace every negation not(L ≡ R) by the disjunction of formulas of the type

L ≡ xy & R ≡ xz & init(y) = A & init(z) = A′  (1)

where x, y, z denote new unknowns and the disjunction is taken over all alphabets A, A′ ⊆ Σ such that A ∩ A′ = ∅ and A ∪ A′ ≠ ∅. Clearly, constraints of the form init(x) = A or alph(x) = A, A ⊆ Σ, can be expressed by I-closed regular languages. 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 ∈ C). Moreover, it suffices to consider trace equations of the form x_{1} ⋯ x_{k} ≡ y_{1} ⋯ y_{l} with k ≥ l > 0, x_{i}, y_{j} ∈ Ω. (The equation x_{1} ⋯ x_{k} ≡ 1 and the occurrences of each x_{i} can be deleted from all equations, adding the constraints alph(x_{i}) = ∅.)

3.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 L_{1} = R_{1}, …, L_{k} = R_{k} with additional constraints and unknowns. Moreover, for every solution σ for L ≡ R the mapping lex ∘ σ: Ω → Σ^{∗} → LNF can be extended to a solution for the equations L_{1} = R_{1}, …, L_{k} = R_{k}. 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 intermediate 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 = {x ∈ C_{x} | x ∈ Ω} a set of constraints, where each C_{x} is an I-closed regular language. Moreover, every L ≡ R in T has the form x_{1} ⋯ x_{k} ≡ y_{1} ⋯ y_{l} with k ≥ l ≥ 1, x_{i}, y_{j} ∈ Ω. 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 ∈ C_{x} from C are replaced by the truth value of σ(L) ≡_{I} σ(R), σ(L) = σ(R), and σ(x) ∈ C_{x}, respectively.

Definition 14. A formula S(T, W, C) as above is called normalized if for every solution σ for S the mapping lex ∘ σ is a solution for S, too.

Remark 15. Note that a formula S(T, ∅, C) with I-closed constraints C is always normalized.

Remark 16. Suppose S = S(T, W, C) is normalized and let x ≡ y belong to T, where x, y ∈ Ω. Consider the new formula S′ = S′(T′, W′, C) obtained from S by replacing every occurrence of x ≡ y by x = y and letting T′ = T \ {x ≡ y}, W′ = W ∪ {x = y}. Then S is solvable if and only if S′ is solvable. Note that a solution for S′ 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′, see the example below. Moreover, S′ is a normalized system, too.

Example 17. Consider the trace equation system S = ({x ≡ y}, {x = ab, y = ba}, ∅) given as the conjunction (x ≡ y) & (x = ab) & (y = ba), where (a, b) ∈ 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. 12. Recall that an equation system with I-closed constraints S = S(T, ∅, {x ∈ C_{x}}_{x∈Ω}) over (Σ, I), Ω is a normalized system. As previously noted it suffices to consider a formula S with trace equations of the form

x_{1} ⋯ x_{k} ≡ y_{1} ⋯ y_{l}, k ≥ l ≥ 1, (k, l) ≠ (1, 1) .  (2)

We suppose without loss of generality that for all unknowns x ∈ Ω some A_{x} ⊆ Σ exists such that h(A_{x}) > 0, and x ∈ C_{x} implies alph(x) ⊆ A_{x}, for all x. Moreover, let S be a conjunction of trace equations as in (2), of word equations and of Iclosed regular constraints x ∈ C_{x}. We define the weight of a trace equation x_{1} ⋯ x_{k} ≡ y_{1} ⋯ y_{l} as in (2) as the triple of natural numbers (l, h(∪_{i=1}^{k−1}A_{x_{i}}), k) and we consider the lexicographical ordering on ℕ × ℕ × ℕ. 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 x_{1} ⋯ x_{k} ≡ y_{1} ⋯ y_{l} by

x_{1} ⋯ x_{k} ≡ z & y_{1} ⋯ y_{l} ≡ z & alph(z) ⊆ ∪_{i=1}^{k}A_{x_{i}} .

Rule 2: Suppose l = 1 and k > 2, and let z denote a new unknown. Then we replace the equation x_{1} ⋯ x_{k} ≡ y_{1} by

x_{1}z ≡ y_{1} & x_{2} ⋯ x_{k} ≡ z & alph(z) ⊆ ∪_{i=2}^{k}A_{x_{i}} .

Rule 3: Suppose l = 1 and k = 2 and, in order to simplify notation, consider the equation xy ≡ z (rather than uniformly x_{1}x_{2} = y_{1}). Moreover, let h = h(A_{x}) denote the height of A_{x} (where alph(x) ⊆ A_{x} follows from the constraint x ∈ C_{x}). We replace xy ≡ z by the disjunction of the word equation

xy = z  (3)

and of formulas of the type

x = x_{1} ⋯ x_{m} & y ≡ y_{1} ⋯ y_{m} & z = x_{1}y_{1} ⋯ x_{m}y_{m} &
alph(x_{1}) ⊆ A_{1} & ⋯ & alph(x_{m}) ⊆ A_{m} &
alph(y_{1}) ⊆ B_{1} & ⋯ & alph(y_{m}) ⊆ B_{m} ,  (4)

where x_{i}, y_{j} 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 A_{1}, …, A_{m}, B_{1}, …, B_{m} ⊆ Σ such that^{1}

A_{i} ≠ ∅ for all 1 < i ≤ m, and
1 ≤ h(B_{j}) < h for all 1 ≤ j < m, and
B_{j} × A_{i} ⊆ I for all 1 ≤ j < i ≤ m, and
A_{1} ∪ ⋯ ∪ A_{m} ⊆ A_{x}, and B_{1} ∪ ⋯ ∪ B_{m} ⊆ A_{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′ denote the formula obtained from S by applying one of the three rules described above. Note that none of the rules adds negations.

1 Obviously some equations become redundant and they can be actually omitted in the disjunction.

Lemma 18. Let S be a normalized equation system. Then the new system S′ is normalized, too. Moreover, S′ 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′, respectively. Clearly, if S′ has been obtained from S by the third rule, then every solution for S′ is a solution for S, too, see Rem. 3. Therefore, let us consider an equation xy ≡ z in S and a solution σ: Ω → Σ^{∗} for S. Then σ′ = lex ∘ σ is also solution for S, since S is normalized. We show that σ′ can be extended to a solution for S′. Let s = σ′(x), t = σ′(y) and v = σ′(z). Hence, st ≡_{I} v with s, t, v ∈ LNF. If h(s) = 1, then in the Main Lemma we have m = 1, hence v = st. Therefore σ′ is a solution of the new system S′. Suppose that st ≡_{I} v with s, t, v ∈ LNF, h(s) = h > 1. Then some m, 1 ≤ m ≤ (n − 1)(h − 1)/2 + 1, and words s_{1}, …, s_{m}, t_{1}, …, t_{m} exist, satisfying the conditions of the Main Lemma. With σ′(x_{i}) = s_{i}, σ′(y_{j}) = t_{j} it is easily verified that σ′ is a solution for S′. The relation between the solution set of S and the solution set of S′, together with the fact that S is normalized, imply that S′ is normalized, too. This shows the lemma.

Finally, note that the new trace equation y_{1} ⋯ y_{m} ≡ y in (4) has lower weight than xy ≡ z due to h(∪_{j=1}^{m−1}B_{j}) < h = h(A_{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′ = (∅, W′, C′). This concludes our proof.

4 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. 12 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 19. Let ∼_{I} be a relation on (Σ^{∗})^{∗} defined as

(x_{1}, …, x_{m}) ∼_{I} (x′_{1}, …, x′_{m′})

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

x_{j} = x′_{j} for all 1 ≤ j ≤ m, j ∉ {i, i + 1}, and
(x_{i}, x_{i+1}) = (x′_{i+1}, x′_{i}) and (x_{i}, x_{i+1}) ∈ I .

By ≈_{I} we denote the equivalence relation generated on (Σ^{∗})^{∗} by ∼_{I}.

Let x ∈ Σ^{∗}, by abuse of language we write (x_{1}, …, x_{m}) ≈_{I} x if some words x′_{1}, …, x′_{m} exist such that

(x_{1}, …, x_{m}) ≈_{I} (x′_{1}, …, x′_{m}) and x = x′_{1} ⋯ x′_{m} .

Theorem 20. Let s, t, v ∈ LNF be words in lexicographical normal form such that st ≡_{I} v. Then there exist positive integers m, p with m ≤ \frac{(n−1)^{2}}{2} + 1, p ≤ n^{n}n! such that

s = s_{1} ⋯ s_{m} ,
t = t_{1} ⋯ t_{p} ,
(s_{1}, …, s_{m}, t_{1}, …, t_{p}) ≈_{I} v ,

for some words s_{1}, …, s_{m}, t_{1}, …, t_{p} ∈ Σ^{∗}.

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

s = s_{1} ⋯ s_{m(h)} ,
t = t_{1} ⋯ t_{p(h)} ,
(s_{1}, …, s_{m(h)}, t_{1}, …, t_{p(h)}) ≈_{I} v ,

for some words s_{i}, t_{j}. Note that m(h), p(h) ≤ |v|. 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) ≤ n^{h}h!, thereby proving the theorem. Let h ≥ 1. By the Main Lemma there exist an integer m ≤ (n − 1)(h − 1)/2 + 1 and words s_{1}, …, s_{m}, t_{1}, …, t_{m} in lexicographical normal form satisfying

s = s_{1} ⋯ s_{m} ,
t ≡_{I} t_{1} ⋯ t_{m} ,
v = s_{1}t_{1} ⋯ s_{m}t_{m} ,
s_{i} ≠ 1, t_{j} ≠ 1 for 1 < i ≤ m, 1 ≤ j < m ,
t_{j} ∈ I(s_{j+1} ⋯ s_{m}) and h(t_{j}) < 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 = t_{1} ∈ LNF, which satisfies the claim. Hence let h, m ≥ 2. Let t̄_{1} = t_{1} and t̄_{i} = lex(t̄_{i−1}t_{i}) for i = 2, …, m. Clearly, t̄_{m} = t, h(t̄_{i}) < h for 1 ≤ i < m and

t̄_{i−1}t_{i} ≡_{I} t̄_{i}, for 1 < i ≤ m.  (7)

Now we can apply the induction hypothesis to each of the (m − 1) equivalences (7) obtaining

t ≈_{I} (t′_{1}, …, t′_{p}) ,  (8)

for some p ≤ (m−1)[m(h−1)+p(h−1)], some words t′_{1}, …, t′_{p} and some integers 1 = l_{0} < l_{1} < ⋯ < l_{m} = p + 1 such that

t_{i} = t′_{l_{i−1}} ⋯ t′_{l_{i}−1} for every 1 ≤ i ≤ m .  (9)

The above claim can be verified by noting that

t ≈_{I} (t′_{1}, …, t′_{i}, …, t′_{j}, …, t′_{q}) and t′_{i} ⋯ t′_{j} ≈_{I} (v_{1}, …, v_{k})

implies that

t ≈_{I} (t′_{1}, …, t′_{i−1}, v′_{1}, …, v′_{l}, t′_{j+1}, …, t′_{q}) ,

for some l ≤ j − i + k and v′_{1}, …, v′_{l} ∈ Σ^{∗}, such that v′_{1} ⋯ v′_{l} = v_{1} ⋯ v_{k} and each v′_{q} is a factor of some v_{r}. Hence, we obtain from (8), (9) for suitable words t′′_{1}, …, t′′_{p}:

t = t′′_{1} ⋯ t′′_{p} ,
v ≈_{I} (s_{1}, …, s_{m}, t_{1}, …, t_{m}) ≈_{I} (s_{1}, …, s_{m}, t′_{1}, …, t′_{p})
≈_{I} (s_{1}, …, s_{m}, t′′_{1}, …, t′′_{p}) .

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 + n^{h−1}(h − 1)!] ≤ n^{h}h! ,

which concludes the proof.

Remark 21. We can also use Thm. 20 in order to prove the main result, Thm. 12. Recall that the main difficulty consists in replacing a trace equation of the form xy ≡ z, where x, y, z ∈ Ω. By Thm. 20 we simply replace such an equation xy ≡ z by a disjunction over clauses of the form

\begin{matrix}x = x_{1} ⋯ x_{m} & y = y_{1} ⋯ y_{p} & \\ z = z_{π(1)} ⋯ z_{π(m+p)} & alph(z_{i}) ⊆ A_{i} , \end{matrix}

for all 1 ≤ m ≤ \frac{(n−1)^{2}}{2} + 1, 1 ≤ p ≤ n^{n}n!, π ∈ S_{m+p}^{I} and A_{i} ⊆ Σ. Here x_{i}, y_{j} denote new variables and z_{i} = x_{i} for 1 ≤ i ≤ m, resp. z_{m+j} = y_{j} for 1 ≤ j ≤ p. S_{m+p}^{I} denotes the set of permutations over {1, …, m + p} such that for i < j the inequality π(i) > π(j) implies A_{i} × A_{j} ⊆ I. This reduction of a single trace equation to word equations roughly yields an increase in the number of word equations by (N + 2)!2^{n(N+1)}, where N = n^{n}n! + (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 AC^{0} and TC^{0}. Let f: Σ^{∗} → Σ^{∗} be a function such that |f(w)| = p(|w|) for some polynomial p and every w ∈ Σ^{∗}. Let k ≥ 0. Then f is AC^{k}-computable if there is a family (C_{n})_{n≥0} of polynomial-size circuits of depth O(log^{k}(n)) with AND and OR gates of unbounded fan-in/out and unary NOT gates, such that C_{|w|} computes f(w) for all w ∈ Σ^{∗}. A function f is TC^{k}- 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 MA-JORITY 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 ∈ Σ (analogously for the outputs). Uniformity means that given n ≥ 0 (a fixed coding of) the circuit C_{n} can be easily computed (e.g. in logarithmic space). It is not very hard to verify that AC^{k} ⊆ TC^{k} ⊆ AC^{k+1}, k ≥ 0. For more details about circuit complexity see e.g. [15]. We state the results below without proofs (being sketched in [6]). With Thm. 20 we obtain

Corollary 22. Let (Σ, I) denote an independence alphabet. Then we can compute lex(st) on input s, t ∈ LNF in uniform AC^{0}.

Remark 23. We could apply Cor. 22 in order to compute the function lex in AC^{1}. However, we can do better: the mapping lex: Σ^{∗} → LNF is computable in uniform TC^{0}. This result can be compared with the fact that the equivalence s ≡_{I} t can be verified in uniform TC^{0}, too (see [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. Àlvarez and J. Gabarró. 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èmes combinatoires de commutation et réarrangements. Number 85 in Lecture Notes in Mathematics. Springer, 1969.

5. C. Choffrut. Combinatorics in trace monoids I. In [7].

6. V. Diekert, Yu. Matiyasevich, and A. Muscholl. Solving trace equations using lexicographical normal forms. Technical report, Universität Stuttgart, Fakultät Informatik, Bericht 1997/01, 1997.

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

8. C. Duboc. On some equations in free partially commutative monoids. Theoretical Computer Science, 46:159–174, 1986.

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 Dec. 1996, Institut für Informatik, Universität Stuttgart, Germany.

12. Yu. Matiyasevich. Some decision problems for traces. In S. Adian and A. Nerode, editors, Proc. of the 4th International Symposium on Logical Foundations of Computer Science (LFCS’97), number 1234 in Lecture Notes in Computer Science, pages 248–257, 1997. Springer. Invited lecture. To appear.

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

14. K. U. Schulz. Makanin’s algorithm for word equations — Two improvements and a generalization. In K. U. Schulz, ed., Word Equations and Related Topics, number 572 in Lecture Notes in Computer Science, pp. 85–150, Springer, 1991.

15. H. Straubing. Finite automata, formal logic, and circuit complexity. Birkhäuser, 1994.