BRICS RS-02-41 Bloom & Ésik: Axiomatizing Omega and Omega-op Powers of Words BRICS

Basic Research in Computer Science

Axiomatizing Omega and Omega-op Powers of Words

Stephen L. Bloom Zoltán Ésik BRICS Report Series RS-02-41 ISSN 0909-0878 October 2002 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2002, Stephen L. Bloom & Zoltán Ésik.

BRICS, Department of Computer Science University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/02/41/

Axiomatizing omega and omega-op powers of words

Stephen L. Bloom^{∗}

Department of Computer Science Stevens Institute of Technology Hoboken, NJ 07030

Zoltán Ésik^{†}

Institute for Informatics University of Szeged 6720 Szeged, Hungary

October, 2002

Abstract

In 1978, Courcelle asked for a complete set of axioms and rules for the equational theory of (discrete regular) words equipped with the operations of product, omega power and omega-op power. In this paper we find a simple set of equations and prove they are complete. Moreover, we show that the equational theory is decidable in polynomial time.

1 Introduction

The theory of finite automata and regular languages on finite words has been generalized to various linear and nonlinear structures. In many cases, the study of such extensions was motivated by questions from formal logic. The linear structures studied include omega words [Buch62], (countable) ordinal words [Buch65, Chou78, Woj85, Bed96], and, more recently, all (countable) words on discrete^{1} linear orders, by Bruyère and Carton, cf. [BruyCar, BruyCar2], where there is a unified treatment.

Countable words^{2}, i.e., finite or countably infinite labeled linear orders, were already studied by B. Courcelle in the 1970’s. He singled out a subclass of countable words that we call regular words. These words arise as initial solutions of finite systems of recursion equations. Since each finite system of recursion equations unfolds to a system of regular trees, it follows that the regular words are exactly the frontiers of regular trees. This observation was made explicit by Thomas in [Thom86]. He also gave a characterization of regular words in terms of formal logic. He showed that a nonempty countable word, viewed as the isomorphism class of a labeled linear order, is regular iff it consists of all models of an ℵ_{0}-categorical sentence of a certain monadic second-order logic. In [BlEs02], the authors have shown that a countable word is regular iff it can be defined on an ordinary regular language (which can be chosen to be a prefix code) equipped with the lexicographical order such that the labeling function satisfies a regularity condition.

∗Partially supported by NSF grant 0119916.

†Partially supported by BRICS, Aalborg, Denmark, NSF grant 0119916, and by a grant of the National Foundation of Hungary for Scientific Research.

1“Scattered” linear orders, in the terminology of [BruyCar, BruyCar2].

2“Arrangements” in the terminology of [Cour78].

Courcelle defined the operations of product, omega power and omega-op power, and characterized the least class of words that can be generated from the letters of an alphabet by a property of (regular) trees. It was shown by Heilbrunner in [Heil80] that a word belongs to this class iff it is a nonempty discrete regular word. An infinite collection of operations generating all regular words from single letters, including those having dense suborderings, was also described in [Heil80].

In this paper, our concern is the equational theory of words equipped with the operations of product, omega power and omega-op power. Courcelle [Cour78] asked for a complete set of axioms and rules for this theory. In this paper, we find such a system. The axioms are the identities given in Definition 3.6, and the rules are those of standard equational logic. Our methods also give a polynomial time decision algorithm. (That the equational theory is decidable follows from the result of Thomas [Thom86] to the effect that the equality of the frontiers of regular trees is decidable. However, no elementary upper bound seems to be known for this more general problem.) Moreover, it follows that for any alphabet A, the algebra of discrete regular A-labeled words is freely generated by A in the variety axiomatized by the equations in Definition 3.6.

Our results extend those in [BlCho01] concerning the equational theory of just the operations of product and omega power. However, the arguments and methods used here are quite different. In particular, we have not used automata to achieve the polynomial complexity bound.

1.1 Notation

ω is the linearly ordered set of the nonnegative integers; ω^{op} is the linearly ordered set {…, −2, −1, 0}.

2 Linear words

A linear word, (L, ≤, u, A) consists of a linearly ordered set (L, ≤), an “alphabet” A and a “labeling function” u : L → A. When the alphabet A is fixed, we say for short that u is a word on A, (or an “A-labeled word”) over the linear order (L, ≤). The linear order (L, ≤) is the underlying linear order of u. When L is empty, we have the empty word, written 1, on A (for any set A). If u, v are words on A, we say v is a subword of u if the underlying linear order of v is a subposet of that of u, and the labeling on the subposet agrees with that on the superposet.

If u and v are words over A with underlying linear orders (L_{u}, ≤) and (L_{v}, ≤), respectively, a morphism h : u → v is an order preserving function h : L_{u} → L_{v} which preserves the labeling:

u(x) = v(h(x)), x ∈ L_{u}.

Thus, for any set A, the collection of words on A forms a category. Two words u, v on A are isomorphic when they are isomorphic in this category, i.e., when there are morphisms h : u → v, g : v → u such that u →^{h} v →^{g} u and v →^{g} u →^{h} v are the respective identities. We write u ≅ v when u and v are isomorphic. We usually identify isomorphic words.

We equip the collection of all words on A with several operations. Suppose that u = (L_{u}, ≤, u) and v = (L_{v}, ≤, v) are words. The product u · v is the word over the sum L_{u} + L_{v}, i.e., over the disjoint union of L_{u} and L_{v} ordered so that x < y, for every x ∈ L_{u}, y ∈ L_{v}; for pairs in L_{u} or L_{v}, the order is the original one. For x ∈ L_{u} + L_{v},

(u · v)(x) = \begin{cases}u(x) & if x ∈ L_{u} \\ v(x) & if x ∈ L_{v}. \end{cases}

The omega power of u, denoted u^{ω}, is the word whose underlying order is L_{u} × ω, ordered and labeled as follows:

(x, i) ≤ (y, j) ⟺ i < j or (i = j and x ≤ y)
u^{ω}(x, i) = u(x).

Similarly, the omega-op power u^{ω^{op}} of u is the word whose underlying order is L_{u} × ω^{op}, ordered and labeled as for u^{ω}, but now i, j range over the nonpositive integers.

In the last section, we will also be considering the reverse operation u ↦ u^{r}. The underlying order of u^{r} is (L_{u}, ≥), i.e., the reverse of (L_{u}, ≤). The labeling function of the reverse is the same as that of u.

Remark 2.1 The operations just defined make sense also for “partial words”, i.e., labeled partially ordered sets. For example, the underlying partial order of the product u · v is, as a set of pairs, ≤_{u} ∪ ≤_{v} ∪(L_{u} × L_{v}), where ≤_{u} is the set of ordered pairs (x, y) ∈ L_{u} such that x ≤ y; similarly for ≤_{v}.

Note: the subcollection of all words on A whose underlying linear order is finite or countably infinite is closed under the operations of product, omega and omega-op power. As mentioned in the Introduction, in [Heil80], the least collection of words on A which contains the singletons labeled a ∈ A, closed under product, omega and omega-op powers was shown to be the nonempty discrete regular words, i.e., those nonempty discrete words isomorphic to the frontier of a binary regular tree. (A word is discrete if there is no order embedding of the rationals into its underlying linear order.)

3 Terms

All of our algebras (X, ·,^{ω} ,^{ω^{op}} ) are enrichments of a semigroup (X, ·) by two unary operations x ↦ x^{ω}, and x ↦ x^{ω^{op}}. The basic models are the algebras (AW, ·,^{ω} ,^{ω^{op}} ) of all finite and countable words on a the alphabet A, enriched with the three indicated operations. For each such algebra, we let (AR_{d}, ·,^{ω} ,^{ω^{op}} ) denote the least subalgebra of AW containing the singletons, i.e., the subalgebra of AW consisting of the discrete nonempty regular words.

Proposition 3.1 Suppose that A and B are sets and B is any algebra of words on B equipped with the operations ·,^{ω} ,^{ω^{op}}. Then any function A → B can be extended to a homomorphism AW → B.

Proof. Given h : A → X, for each word u in AW define h^{♯}(u) as the word obtained by substituting a disjoint copy of h(a) for each x ∈ L_{u}, where u(x) = a. It is a routine matter to show that h^{♯} is a homomorphism. □

Definition 3.2 Let A be a fixed set.

1. A term on the alphabet A is either a letter a ∈ A, or t · t′, t^{ω} or t^{ω^{op}}, where t, t′ are terms on A.

2. When t is a term over the alphabet A, we let |t| denote the linear word on A denoted by t. More precisely, |a| is a singleton set, labeled a. Using induction, we define

|t · t′| := |t| · |t′|
|t^{ω}| := |t|^{ω}
|t^{ω^{op}}| := |t|^{ω^{op}}.

3. An equation t = t′ is valid if |t| ≅ |t′|.

4. The height of a term t, denoted h(t), is the number of nested ^{ω} and ^{ω^{op}} operations.

We sometimes add a term 1 of height 0 denoting the empty word. Terms of height zero are called “finite terms”. Those of positive height are “infinite terms”.

As usual, each term over A induces a term function X^{A} → X over any algebra X equipped with the operations ·,^{ω} ,^{ω^{op}}. For a term t, the word |t| is just the value of the function induced by t over the algebra AW when each letter a is evaluated as the singleton word labeled a.

¿From Proposition 3.1 we immediately infer the following fact.

Proposition 3.3 For any terms t, t′ over A, t = t′ is valid iff t = t′ holds in all algebras of words under any evaluation of the letters in A, i.e., when t = t′ holds in the variety generated by all word algebras.

Because we will always interpret the operation sign · as an associative operation, we allow ourselves to write terms such as t_{1} · t_{2} ⋯ t_{k}, for k ≥ 3, with no parentheses.

Definition 3.4 We assume a nonempty “alphabet” A. A primitive term (on A) is either

1. a_{1} ⋯ a_{k}, a_{i} ∈ A, k ≥ 1 (a “finite” primitive term), or

2. a_{1} ⋯ a_{k}(b_{1} ⋯ b_{m})^{ω}, a_{i}, b_{j} ∈ A, k ≥ 0, m ≥ 1 (a “right infinite” primitive term), or

3. (c_{m} ⋯ c_{1})^{ω^{op}}a_{k} ⋯ a_{1}, a_{i}, c_{j} ∈ A, k ≥ 0, m ≥ 1 (a “left infinite” primitive term), or

4. (c_{m} ⋯ c_{1})^{ω^{op}}a_{k} ⋯ a_{1}(b_{1} ⋯ b_{n})^{ω}, a_{i}, b_{j}, c_{l} ∈ A, k ≥ 0, m, n ≥ 1 (a “biinfinite” primitive term).

A proper term is either

• a primitive term, or

• a term of the form t · t′ where t, t′ are proper terms and |t| has no greatest element or |t′| has no least element, or

• a term of the form t^{ω}, or t^{ω^{op}}, where t is a proper term and |t| either has no least or no greatest element.

An extended primitive term is either 1 or a primitive term; an extended proper term is either 1 or a proper term.

Remark 3.5 If r, l are primitive terms such that |r| has a greatest and |l| has a least element, then r · l is primitive. Indeed, r must have the form 3.4.1 or 3.4.3, and l must have the form 3.4.1 or 3.4.2.

Definition 3.6 [The axioms] Let Ax denote the following infinite set of equations, where x, y, z ∈ A are distinct letters.

(x · y) · z = x · (y · z)  (1)
(x · y)^{ω} = x · (y · x)^{ω}  (2)
(x · y)^{ω^{op}} = (y · x)^{ω^{op}} · y  (3)
(x^{n})^{ω} = x^{ω}, n ≥ 2  (4)
(x^{n})^{ω^{op}} = x^{ω^{op}}, n ≥ 2.  (5)

Remark 3.7 In [BedCar98], Bedon and Carton define semigroups equipped with an omega power operation satisfying (2) and (4). These semigroups are a one-sorted version of Wilke algebras ^{3} [Wil91].

Proposition 3.8 Each equation in Ax is valid. □

For terms t and t′, let us write Ax ⊢ t = t′ iff t = t′ is derivable from the equations in Ax by the rules of equational logic. It follows from Proposition 3.8 and Proposition 3.3 that any such equation is valid.

The following theorem is one of the main tools used to prove the completeness of the axioms.

Theorem 3.9 For each finite term t there is a unique finite primitive term a_{1} ⋯ a_{k} such that Ax ⊢ t = a_{1} ⋯ a_{k}.

For each infinite term t there are extended primitive terms l, r and an extended proper term m such that

• Ax ⊢ t = l · m · r.

• |t| has a least element iff l ≠ 1.

• |t| has a greatest element iff r ≠ 1.

• if m ≠ 1, either |l| does not have a greatest element or |m| has no least, and either |m| has no greatest element or |r| has no least; if m = 1, then either |l| has no greatest or |r| has no least.

3Wilke algebras are called “binoids” in [Wil91].

• h(l · m · r) ≤ h(t).

Thus, since l · m · r is proper, for each term t there is a proper term t′ with h(t′) ≤ h(t) and Ax ⊢ t = t′.

Proof. The claim for finite terms is clear, using the associativity axiom. Suppose now that t is an infinite term. If t = (a_{1} ⋯ a_{k})^{ω}, we let l = t and let m = r = 1; if t = (a_{k} ⋯ a_{1})^{ω^{op}}, we let l = m = 1 and let r = t. We continue by induction on the structure of t. Suppose that t = t_{1} · t_{2}. If t_{1} is finite, so that t_{2} is infinite, let l = a_{1} ⋯ a_{k}l_{2}, m = m_{2} and r = r_{2}, where Ax ⊢ t_{2} = l_{2} · m_{2} · r_{2}, by the induction hypothesis. Similarly when t_{2} is finite and t_{1} is infinite. Now assume t = t_{1} · t_{2} and both t_{1}, t_{2} are infinite terms. Then, let

l = l_{1}
m = m_{1} · (r_{1}l_{2}) · m_{2}
r = r_{2}.

Note that we need not worry about the case when r_{1} has a greatest and l_{2} has a least element, by Remark 3.5. Also, Ax ⊢ t = l · m · r, by the associativity axiom (1). If t = (t_{1})^{ω}, and t_{1} is infinite, we let

l = l_{1}
m = (m_{1} · r_{1}l_{1})^{ω}
r = 1.

Ax ⊢ t = l · m · r, by axiom (2). If t = (t_{1})^{ω^{op}} where t_{1} is infinite, we let

l = 1
m = (r_{1}l_{1} · m_{1})^{ω^{op}}
r = r_{1}.

Ax ⊢ t = l · m · r by axiom (3). This completes the proof. □

Proposition 3.10 Suppose that t_{1}, t_{2} are primitive terms. Then

|t_{1}| ≅ |t_{2}| ⟺ Ax ⊢ t_{1} = t_{2}.

In fact, for each primitive term there is a normal form. The normal form of a finite term is itself. For a term of the form a_{1} ⋯ a_{k}(b_{1} ⋯ b_{m})^{ω}, we find the shortest word b_{1} ⋯ b_{i} such that b_{1} ⋯ b_{m} is a power of b_{1} ⋯ b_{i}, and then apply the rewriting rule x(yx)^{ω} ⇝ (xy)^{ω} to a_{1} ⋯ a_{k}(b_{1} ⋯ b_{i})^{ω} as many times as possible. Then |t_{1}| ≅ |t_{2}| iff t_{1} and t_{2} have the same normal form. The normal form of a left infinite primitive term is obtained in the same way. Note that the normal form of a finite, or left or right infinite primitive term is unique modulo associativity. As for bi-infinite primitive terms, a normal form is a term (b_{k} ⋯ b_{1})^{ω^{op}}a_{1} ⋯ a_{m}(c_{1} ⋯ c_{n})^{ω}, where neither b_{k} ⋯ b_{1} nor c_{1} … c_{n} is a nontrivial power of a word, moreover, if m ≠ 0, then a_{1} is different from b_{k} and a_{m} is different from c_{n}. However, the normal form may not be unique. In that case, m = 0 holds for all normal forms, and the normal forms are equivalent modulo the equation

(xy)^{ω^{op}}(zy)^{ω} = (yx)^{ω^{op}}(yz)^{ω},

which is easily derivable from the axioms.

Now fix the alphabet A. A primitive word^{4} is either a finite word on A or a word on A whose underlying linear order is isomorphic to ω, ω^{op} or ω^{op} + ω, which is ultimately periodic (in both directions in the later case). Thus, the nonempty primitive words are those denoted by primitive terms. Thus, for a finite or countable alphabet A, there are only countably many primitive words on A.

For each primitive word u on A, let b_{u} be a new letter in an alphabet B disjoint from the set of all terms on A. Let t_{u} be a primitive term on A such that |t_{u}| = u. Since by Proposition 3.10 all such primitive terms are equivalent with respect to the axioms, in the subsequent arguments we can fix the term t_{u} for each nonempty primitive word u. For example, we can take the lexicographically least. Let σ denote the unique term homomorphism mapping terms over B to terms over A such that

σ(b_{u}) = t_{u}

for each letter b_{u} ∈ B. Let σ also denote the substitution that maps a linear word on B to the corresponding word on A, so that for every term t on B,

|σ(t)| = σ(|t|).

Suppose that u is a linear word on A, with underlying order (L, ≤), and suppose v is a subword of u, with underlying linear order (L′, ≤). We say v is closed with respect to the successor relation if whenever x, y ∈ L and x is the successor in L of y, then x ∈ L′ ⟺ y ∈ L′.

A minimal successor closed subword of a word P is a nonempty subword of P which is closed with respect to the successor relation and which does not contain any proper nonempty subword with the same property.

4In the field of Combinatorics on Words, a “primitive word” is a finite nonempty word which is not a proper power. This is not the way we are using the term.

Proposition 3.11 Any minimal successor closed subword of a word is either finite, or its underlying linear order is isomorphic to ω, ω^{op}, or ω^{op} + ω.

Proposition 3.12 For any term t over A, each minimal successor closed subword of |t| is a primitive word.

Proof. Clear from Theorem 3.9, or by a straightforward induction. □

Now, given a linear word P on A whose minimal successor closed subwords are primitive, let P̂ denote the linear word on B whose points are the minimal successor closed subwords of P, each labeled by the corresponding letter in B. The order in P̂ is inherited from P.

Proposition 3.13 Suppose that P, Q are A-labeled words whose minimal successor closed subwords are primitive. Then, P ≅ Q iff P̂ ≅ Q̂.

Proof. If P̂ ≅ Q̂, then clearly P ≅ Q.

Now let φ : P → Q be an isomorphism. We define an isomorphism φ̂ : P̂ → Q̂, as follows. When M is a minimal subposet of P closed under the successor relation, and x ∈ M, let φ̂(M) denote the minimal subposet of Q containing φ(x) closed under the successor relation. □

Lemma 3.14 Let P_{1} and P_{2} be words whose minimal successor closed subwords are primitive.

• Suppose that P_{1} has no greatest element or that P_{2} has no least. Then

{ \atop P_{1} · P_{2}} = P̂_{1} · P̂_{2}.

• Suppose that P ≠ 1 and P has no least or no greatest. Then

P̂^{ω} = (P̂)^{ω}

and

{ \atop P^{ω^{op}}} = (P̂)^{ω^{op}}.

Proof. For P_{1} · P_{2}: There exist no x ∈ P_{1} and y ∈ P_{2} such that in P_{1} · P_{2}, y is the successor of x. □

Proposition 3.15 For each proper term t on the alphabet A there is a term t̂ over the alphabet B such that σ(t̂) = t and h(t̂) < h(t) when t is infinite. Moreover, if |t| = P, then |t̂| = P̂.

Proof. If t is primitive, then t̂ is a single letter, and σ(t̂) = t, by definition of σ. If t = t_{1} · t_{2} is proper, then t̂ = t̂_{1} · t̂_{2}, by the lemma. Since σ is a homomorphism, using induction, σ(t̂) = t. If t = (t_{1})^{ω} or (t_{1})^{ω^{op}}, then t̂ is (t̂_{1})^{ω} or (t̂_{1})^{ω^{op}}, respectively. Again σ(t̂) = t. □

As mentioned earlier, if Ax ⊢ t = t′, for terms t and t′, then the equation t = t′ is valid. We now prove the converse.

Theorem 3.16 The axioms are complete: any valid equation is derivable from Ax.

Proof. Suppose that t_{1}, t_{2} are terms on A such that |t_{1}| ≅ |t_{2}|. We use induction on

h := max{h(t_{1}), h(t_{2})}

to show that Ax ⊢ t_{1} = t_{2}. When h = 0, the only axiom needed is the associativity axiom. Now suppose that h > 0, so that both t_{1}, t_{2} must be infinite terms. By Theorem 3.9, there are proper terms s_{1}, s_{2} such that Ax ⊢ t_{i} = s_{i}, and h(s_{i}) ≤ h(t_{i}) ≤ h, i = 1, 2. Since |s_{1}| ≅ |s_{2}|, also |ŝ_{1}| ≅ |ŝ_{2}|, by Propositions 3.13 and 3.15. Now h(ŝ_{i}) < h, i = 1, 2. By induction,

Ax ⊢ ŝ_{1} = ŝ_{2}.

But, by Proposition 3.3, for any terms t, t′, and any term morphism φ, if Ax ⊢ t = t′, then Ax ⊢ φ(t) = φ(t′). Thus, in particular,

Ax ⊢ σ(ŝ_{1}) = σ(ŝ_{2}),

i.e.,

Ax ⊢ s_{1} = s_{2},

and thus,

Ax ⊢ t_{1} = t_{2}. □

Corollary 3.17 There is an O(n^{3}) algorithm to decide if an equation t = t′ is valid, where n is the total number of symbols in the terms t, t′.

Proof. Our recursive algorithm first converts the terms t and t′ into proper terms, using the constructive proof of Theorem 3.9. During the conversion, the primitive subterms are brought into normal form and an ordered list of the encountered normal forms is maintained. (We assume a lexicographic order on the normal forms and that in case of ambiguity the lexicographically least normal form is selected.) This can be done in O(n^{2}) time. If t and thus t′ are finite, we just compare the two sides for syntactic equality. If h(t), h(t′) > 0, then, in linear time, we compute the terms t̂ and t̂′ and repeat the procedure. Since h is at most n, and since the heights are reduced by one at each step, the algorithm terminates in O(n^{3}) time. □

Remark 3.18 There is a different argument to show that the complexity bound can be reduced to O(n^{2}).

Corollary 3.19 If t = t′ is valid, then h(t) = h(t′).

3.1 Adding reverse

In a more or less routine manner, we may now obtain an axiomatization of the equational theory of linear words enriched with the operations of product, omega and omega-op power and the reversal operation t ↦ t^{r}. The axioms are (1), (2), (4) together with

(x^{r})^{r} = x  (6)
(x · y)^{r} = y^{r} · x^{r}  (7)
(x^{ω})^{r} = (x^{r})^{ω^{op}}.  (8)

The axioms (3), and (5) are now redundant.

3.2 Adding 1

We may add a constant term 1 to denote the empty word (on any alphabet), and then add the following axioms to those in Definition 3.6.

1 · x = x = x · 1
(1)^{ω} = (1)^{ω^{op}} = 1
1^{r} = 1.

4 All axioms

For the reader’s convenience, we list the totality of the axioms.

(x · y) · z = x · (y · z)
(x · y)^{ω} = x · (y · x)^{ω}
(x · y)^{ω^{op}} = (y · x)^{ω^{op}} · y
(x^{n})^{ω} = x^{ω}, n ≥ 2
(x^{n})^{ω^{op}} = x^{ω^{op}}, n ≥ 2
(x^{r})^{r} = x
(x · y)^{r} = y^{r} · x^{r}
(x^{ω})^{r} = (x^{r})^{ω^{op}}.
1 · x = x = x · 1
(1)^{ω} = (1)^{ω^{op}} = 1
1^{r} = 1.

5 Free Algebras

The first theorem follows immediately from the proof of the Completeness Theorem, Theorem 3.16.

Theorem 5.1 Let V be the variety of all models of Ax in Definition 3.6. For any set A, the algebra freely generated by A in V is the algebra (AR_{d}, ·,^{ω} ,^{ω^{op}} ) of discrete, regular, A-labeled words.

Now, fix a set A and choose a set \overline{A} disjoint from A and a bijection a ↦ \overline{a} from A → \overline{A}.

We have defined the reverse u^{r} of a word in CW as follows: the underlying order of u^{r} is (L_{u}, ≥), the reverse of the underlying order (L_{u}, ≤) of u, and the labeling of points in L_{u} is the same as that in u. The enrichment of the algebra (CW, ·,^{ω} ,^{ω^{op}} ) by this reverse operation is denoted just CW.

However, in the following case, we modify the labeling when applying the reverse operation. Let ((A ∪ \overline{A})R_{d}, ·,^{ω} ,^{ω^{op}} ) denote the algebra of all regular, discrete A ∪ \overline{A}-labeled linear orders, in which the “reversal” operation is redefined as follows.

a^{r} := \overline{a}
(\overline{a})^{r} := a

On the other words in (A ∪ \overline{A})R_{d}, we have

(u · v)^{r} := v^{r} · u^{r}
(u^{ω})^{r} := (u^{r})^{ω^{op}}
(u^{ω^{op}})^{r} := (u^{r})^{ω}.

The last equation follows from the previous one and the fact that (u^{r})^{r} = u.

Theorem 5.2 Let V^{r} be the variety of all models (X, ·,^{ω} ,^{ω^{op}} ,^{r}) of the identities (1), (2), (4), (6), (7), and (8). For any set A, the algebra freely generated by A in V^{r} is (A ∪ \overline{A})R_{d} to X equipped with the above operations. By letting 1 denote the empty word in (A ∪ \overline{A})R_{d}, we obtain the algebra freely generated by A in the variety of all models of the complete set of the identities in Section 4.

□

6 Other models

Aside from the countable word algebras AW, we mention three other classes of models.

1. Uncountable words: For any infinite cardinal ℵ, and any fixed set A, the collection of all words on A over linear orders of cardinality ≤ ℵ satisfies all of the axioms above, with the same definition of the operations.

2. Partial words: As noted in Remark 2.1, the operations u·v, u^{ω}, u^{ω^{op}}, u^{r} are meaningful for labeled partially and not necessarily linearly ordered sets. Further, for any infinite cardinal ℵ, and any fixed set A, the collection of all A-labeled partially ordered sets of cardinality ≤ ℵ satisfies the axioms.

3. Languages of words: For any set A and any infinite cardinal ℵ, the collection of all languages of words on A over linear (or partial) orders of cardinal ≤ ℵ satisfies the axioms; a language of words is, as usual, a subset of words, and the operations on subsets of words are defined as follows:

U · V := {u · v : u ∈ U, v ∈ V }
U^{ω} := \begin{cases}\{u_{1} · u_{2} …: u_{i} ∈ U\} & if 1 ∉ U \\ \{1\} ∪ (U − \{1\})^{ω} & if 1 ∈ U \end{cases}

U^{ω^{op}} := \begin{cases}\{… u_{2} · u_{1} : u_{i} ∈ U\} & if 1 ∉ U \\ \{1\} ∪ (U − \{1\})^{ω^{op}} & if 1 ∈ U \end{cases}
U^{r} := {u^{r} : u ∈ U}
1 := {1}.

Each of these three classes of models generates the same variety as do the countable words, since all free algebras are subalgebras of algebras in each class.

7 Finite Axiomatizability

Using a slight modification of the analogous result in [BlCho01], we can show:

Theorem 7.1 For any finite subset E of the axioms enumerated in Section 4, even the axioms involving the reverse operation ^{r} and the neutral element 1, there is some prime number p and an algebra M such that each equation in E is true in M, but the power identity (x^{p})^{ω} = x^{ω} fails in M.

Thus, by the Compactness Theorem,

Corollary 7.2 There is no finite axiomatization for any of the varieties considered above.

Proof of Theorem 7.1. Let M = ℕ ∪ {1, ⊤, ⊥}, the disjoint union of the nonnegative integers with a three element set. Let p be a prime. Define the operations x · y and x^{ω} on M as follows.

x · y := \begin{cases}x + y & if x, y ∈ ℕ \\ x & if y = 1 \\ y & if x = 1 \\ ⊤ & if exactly one of x, y is ⊤ and the other is in ℕ ∪ \{1\} \\ ⊥ & otherwise. \end{cases}

x^{ω} := \begin{cases}1 & if x = 1 \\ ⊤ & if x ∈ ℕ and p|x \\ ⊥ & otherwise. \end{cases}

x^{ω^{op}} := x^{ω}
x^{r} := x.

It is easy to check that (M, ·, 1) is a commutative monoid. Now we verify some of the axioms. We show that (x · y)^{ω} = x · (y · x)^{ω}. There are three possibilities.

If (x · y)^{ω} = 1, then x = y = 1, so that x · (y · x)^{ω} = 1.

If (x · y)^{ω} = ⊤, then x, y ∈ ℕ and p|(x + y). But then x · (y · x)^{ω} = x · ⊤ = ⊤. Otherwise, (x · y)^{ω} = (y · x)^{ω} = ⊥ and x · ⊥ = ⊥.

Since the reverse operation is the identity function and since the omega power operations is the same as the omega-op power operation, equations (6) and (8) also hold in M. It follows now that (3) holds.

Last, if n < p, and x ∈ ℕ, then x^{n} = nx, so that p|nx iff p|x. Thus, for x ∈ ℕ and n < p, (x^{n})^{ω} = x^{ω}; if x ∈ {⊤, ⊥}, (x^{n})^{ω} = x^{ω} = ⊥, for all n ≥ 1. Thus, if p is a prime larger than all exponents k used in the identities (x^{k})^{ω} = x^{ω} and (x^{k})^{ω^{op}} = x^{ω^{op}}which occur in E, M is a model for E and the identities (1), (2), (3), and all of the reverse axioms and the axioms involving 1. However,

(1^{p})^{ω} = p^{ω}
= ⊤
≠ ⊥
= 1^{ω},

so that the identity (x^{p})^{ω} = x^{ω} fails in M. □

8 Conjectures and Open Problems

The algebras of (countable) words, equipped with the operations of product and an initial fixed point operation, defined by Courcelle in [Cour78], can be shown to form iteration algebras (or iteration theories) [BlEs93]. In fact, over all categories, initial fixed points lead to iteration theories, cf. Ésik and Labella [EsLa98]. We conjecture that the variety generated by algebras of words has a finite axiomatization over the variety of all iteration algebras. Thomas [Thom86] has shown, using methods and results of formal logic, that the equational theory of this variety of iteration algebras is decidable. However, the methods applied in [Thom86] do not provide an elementary upper bound, not even for the equational theory of product, omega power and omega-op power. It would be interesting to find upper and lower bounds.

References

[Bed96] N. Bedon. Finite automata and ordinals. Theoretical Computer Science, 156(1996), 119-144.

[BedCar98] N. Bedon and O. Carton. An Eilenberg theorem for words on countable ordinals. in Latin’98: Theoretical Informatics (C. L. Lucchesi and A. V. Moura, eds.), LNCS 1380, Springer-Verlag, 1998, 53–64.

[BlCho01] S.L. Bloom and C. Choffrut. Long words: the theory of concatenation and ω-power. Theoretical Computer Science, 259(2001), 533–548.

[BlEs93] S.L. Bloom and Z. Ésik. Iteration Theories. Springer, 1993.

[BlEs02] S.L. Bloom and Z. Ésik. Some remarks on regular words. To appear.

[BruyCar] V. Bruyère and O. Carton. Automata on linear orderings. Proceedings Mathematical Foundations of Computer Science, 2001, LNCS 2136, Springer, 2001, 236–247.

[BruyCar2] V. Bruyère and O. Carton. Hierarchy among automata on linear orderings. In: Foundation of Information Technology in the Era of Network and Mobile Computing, Proc. TCS 2002, Kluwer Academic Publishers, 2002, 107–118.

[Buch62] J.R. Büchi. On a decision method in restricted second-order arithmetic. In Int. Congress Logic, Methodology, and Philosophy of Science, Berkeley, 1960, Stanford University Press, 1962, 1–11.

[Buch65] J.R. Büchi. Transfinite automata recursions and weak second order theory of ordinals. In Int. Congress Logic, Methodology, and Philosophy of Science, Jerusalem, 1964, North Holland, 1965, 2–23.

[Chou78] Y. Choueka. Finite automata, definable sets, and regular expressions over ω^{n}-tapes. J. Comp.System Sci., 17(1978), 81–97.

[Cour78] B. Courcelle. Frontiers of infinite trees. Theoretical Informatics and Applications, 12(1978), 319–337.

[EsLa98] Z. Ésik and A. Labella. Equational properties of iteration in algebraically complete categories. Theoretical Computer Science, 195(1998), 61-89.

[Heil80] S. Heilbrunner. An algorithm for the solution of fixed-point equations for infinite words. Theoretical Informatics and Applications, 14(1980), 131–141.

[Thom86] W. Thomas. On frontiers of regular trees. Theoretical Informatics and Applications, vol. 20, 1986, 371–381.

[Wil91] Th. Wilke. An algebraic theory for regular languages of finite and infinite words. Intern. J. Algebra and Comput., 3(1993), 447–489.

[Woj85] J. Wojciechowski. Finite automata on transfinite sequences and regular expressions. Fundamenta Informaticae, 8(1985), 379–396.

Recent BRICS Report Series Publications

RS-02-41 Stephen L. Bloom and Zoltán Ésik. Axiomatizing Omega and Omega-op Powers of Words. October 2002. 16 pp.

RS-02-40 Luca Aceto, Willem Jan Fokkink, and Anna Ingólfsdóttir. A Note on an Expressiveness Hierarchy for Multi-exit Iteration. September 2002. 8 pp.

RS-02-39 Stephen L. Bloom and Zoltán Ésik. Some Remarks on Regular Words. September 2002.

RS-02-38 Daniele Varacca. The Powerdomain of Indexed Valuations. September 2002. 54 pp. Short version appears in Plotkin, editor, Seventeenth Annual IEEE Symposium on Logic in Computer Science, LICS ’02 Proceedings, 2002, pages 299–308.

RS-02-37 Mads Sig Ager, Olivier Danvy, and Mayer Goldberg. A Symmetric Approach to Compilation and Decompilation. August 2002. To appear in Neil Jones’s Festschrift.

RS-02-36 Daniel Damian and Olivier Danvy. CPS Transformation of Flow Information, Part II: Administrative Reductions. August 2002. 9 pp. To appear in the Journal of Functional Programming. This report supersedes the earlier BRICS report RS-01-40.

RS-02-35 Patricia Bouyer. Timed Automata May Cause Some Troubles. August 2002. 44 pp.

RS-02-34 Morten Rhiger. A Foundation for Embedded Languages. August 2002. 29 pp.

RS-02-33 Vincent Balat and Olivier Danvy. Memoization in Type-Directed Partial Evaluation. July 2002. 18 pp. To appear in Batory and Consel, editors, ACM SIGPLAN/SIGSOFT Conference on Generative Programming and Component Engineering, GPCE ’02 Proceedings, LNCS, 2002.

RS-02-32 Mads Sig Ager, Olivier Danvy, and Henning Korsholm Rohde. On Obtaining Knuth, Morris, and Pratt’s String Matcher by Partial Evaluation. July 2002. 43 pp. To appear in Chin, editor, ACM SIGPLAN ASIAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, ASIA-PEPM ’02 Proceedings, 2002.