BRICS RS-00-25 Z. Ésik: Continuous Additive Algebras and Injective Simulations of Synchronization Trees BRICS

Basic Research in Computer Science

Continuous Additive Algebras and

Injective Simulations of Synchronization Trees

Zoltán Ésik

BRICS Report Series RS-00-25 ISSN 0909-0878 September 2000 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2000, 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/00/25/

Continuous additive algebras and injective simulations of synchronization trees

Z. Ésik^{∗}^{†}

Dept. of Computer Science

University of Szeged

P.O.B. 652

6701 Szeged, Hungary

                   esik@inf.u-szeged.hu

September 2000

Abstract

The (in)equational properties of the least fixed point operation on (ω-)continuous functions on (ω-)complete partially ordered sets are captured by the axioms of (ordered) iteration algebras, or iteration theories. We show that the inequational laws of the sum operation in conjunction with the least fixed point operation in continuous additive algebras have a finite axiomatization over the inequations of ordered iteration algebras. As a byproduct of this relative axiomatizability result, we obtain complete infinite inequational and finite implicational axiomatizations. Along the way of proving these results, we give a concrete description of the free algebras in the corresponding variety of ordered iteration algebras. This description uses injective simulations of regular synchronization trees. Thus, our axioms are also sound and complete for the injective simulation (resource bounded simulation) of (regular) processes. Keywords: equational logic, fixed points, synchronization trees, simulation.

∗Partially supported by grant no. FKFP 247/1999 from the Ministry of Education of Hungary and grant no. T30511 from the National Foundation of Hungary for Scientific Research.

†The work reported in the paper was partly carried out while visiting BRICS

1 Introduction

Consider the language of μ-terms given by the syntax

T ::= x | σ(\overbrace{T, …, T}^{n−times}) | T + T | 0 | μx.T,

where x ranges over a countably infinite set of variables, and for each n ≥ 0, σ ranges over a set of n-ary function symbols of a signature Σ. Such terms may be interpreted as (ω-)continuous functions on (ω-)continuous additive algebras equipped with both an additive structure and a (ω-)complete partial order such that addition and the functions induced by the letters of Σ are ω-continuous, the additive neutral element 0 is also the least element with respect to the partial order, and where terms of the form μx.t denote least (pre-)fixed points. We show that under these interpretations the valid (in)equations between μ-terms possess a finite axiomatization over the axioms of ordered iteration algebras (or iteration theories) [9, 19]. In fact, we show that the following set of (in)equations is relatively complete.

x + (y + z) = (x + y) + z  (1)
x + y = y + x  (2)
x + 0 = x  (3)
μx.x = 0  (4)
0 ≤ x  (5)
μx.μy.x + y + z = μx.x + z  (6)

(As usual, the scope of the prefix μx extends to the right as far as possible.) Thus, using known completeness results on iteration algebras, see [9, 17, 19], we obtain complete infinite equational and finite implicational axiomatizations. In fact, it follows that the system consisting of the above (in)equations, the two Conway identities

μx.t[t′/x] = t[μx.t′[t/x]/x]  (7)
μx.t[x/y] = μx.μy.t  (8)

and an equation associated with each finite (simple) group is complete (in the ordered setting). Moreover, the implicational system consisting of (1) – (4), (6), the fixed point equation

μx.t = t[μx.t/x]  (9)

and the least pre-fixed point rule (or fixed point induction) [3, 32]

t[y/x] ≤ y ⇒ μx.t ≤ y  (10)

is also complete. We also show that there is no finite equational axiomatization. Along the way of proving these results, we give a concrete description of the free algebras in the corresponding variety of iteration algebras. This description uses injective simulations [33] of regular synchronization trees [30]. Our results complement those proved in [10] and [20] to the effect that isomorphism classes of regular synchronization trees form the free iteration algebras satisfying equations (1) – (4) and (6) (see also [14] for a recent related result), bisimulation equivalence classes of regular synchronization trees form the free ordered iteration algebras satisfying equations (1) – (4) and

μx.x + y = y,  (11)

and that simulation equivalence classes of regular synchronization trees form the free algebras in the variety of iteration algebras satisfying (1) – (5) and (11). As shown in [20], this latter variety is the same as that generated by the “countinuous semilattice algebras” where + is the operation of taking binary sups and 0 is the least element, and where the letters of Σ are interpreted as continuous functions.

The paper is organized as follows. In Section 2 we define the various models used in the sequel including ω-continuous additive algebras and (ordered) iteration algebras. Section 3 contains the main completeness result Theorem 3.1 and its corollaries. The proof of Theorem 3.1 given here relies on the material proved in the subsequent sections, in particular on the description of the free algebras (Theorem 7.6) and the embedding theorem of Section 8. In Section 4 we define the category of synchronization trees and (functional) simulations, and establish a useful property of injective functional simulations. In Section 5 we recall a general way of constructing iteration algebras from initial algebras over categories. Applied to trees and functional simulations, this construction provides an iteration algebra of synchronozation trees for each signature Σ and set A. In Section 6 we show that finite trees equipped with the partial order defined by injective simulations form the free algebras in a finitely axiomatizable variety of ordered algebras. Section 7 contains the corresponding result for regular trees. It is shown here that for each signature Σ, injective simulation equivalence classes of regular trees, equipped with the simulation order, form the free algebras in the variety of ordered iteration algebras satisfying (1) – (6). In Section 8, we show that every ordered iteration algebra of injective simulation equivalence classes of synchronization trees can be embedded in an ω-continuous additive algebra. Finally, in Section 9, we prove that for nontrivial signatures Σ, the variety of ordered iteration algebras generated by the ω-continuous Σ-algebras and axiomatized by the axioms of ordered iteration algebras and the equations (1) – (6) cannot be defined by a finite number of equation schemes.

2 The models

2.1 Countably complete posets and continuous functions

A poset (P, ≤) is called ω-complete if P has a least element ⊥_{P} and sups ⋁ D of all countable directed sets D ⊆ P (or sups of all ω-chains). It is clear that the direct product ∏_{i∈I} P_{i} of any number of ω-complete posets P_{i}, i ∈ I, equipped with the pointwise order, is ω-complete. In particular, any direct power P^{I} of an ω-complete poset is ω-complete. For ω-complete posets P and Q, a function f : P ⟶ Q is called ω-continuous if it preserves the sup of any countable directed set, or equivalently, the sup of any ω-chain. It follows that any ω-continuous function is monotonic. Clearly, the composite of ω-continuous functions is ω-continuous. When P_{i}, i ∈ I are ω-complete, the projections pr_{j} : ∏_{i∈I} P_{i} ⟶ P_{j} are ω-continuous, as is the target tupling of ω-continuous functions.

Given a poset P and a monotonic function f : P ⟶ P, a pre-fixed point of f is any element a ∈ P with f(a) ≤ a. If f(a) = a, then a is called a fixed point. The least pre-fixed point of f, when exists, is unique, and necessarily a fixed point. The following fact is well-known.

Proposition 2.1 Suppose that P and Q are ω-complete posets and f is an ω-continuous function P ⟶ Q. Then for each b ∈ Q the ω-continuous function f_{b} = f(−, b) : P ⟶ P has a least pre-fixed point denoted f^{†}(b). Moreover, f^{†} is an ω-continuous function Q ⟶ P.

In fact, f^{†}(b) can be constructed as the sup of the ω-chain (f_{b}^{n}(⊥_{P}))_{n≥0}.

2.2 Additive algebras

A signature is a set Σ equipped with a rank function assigning a nonnegative integer rank to each function symbol in Σ. For each n ≥ 0, we will write Σ_{n} for the collection of all symbols of rank n. A Σ-algebra is a set A equipped with an operation σ_{A} : A^{n} ⟶ A, for each n ≥ 0. We will write (A, Σ) or just A to denote a Σ-algebra, and we will sometimes omit the subscript A on the operations. Morphisms of Σ-algebras are defined in the usual way.

When Σ is a signature, let Σ_{+,0} denote the signature that results by adding to Σ the symbol + of rank 2 and the symbol 0 of rank 0. An additive Σ-algebra A = (A, Σ, +, 0) is both a Σ-algebra and a commutative monoid (A, +, 0). An ordered additive Σ-algebra is an additive Σ-algebra A equipped with a partial order ≤ such that the operations, including the sum operation, are monotonic, and such that the inequation (5) holds, so that 0 is the least element of A. Since the sum operation is monotonic, it follows that the inequation

x ≤ x + y  (12)

holds in all ordered additive Σ-algebras. Note that additive Σ-algebras form a variety of Σ_{+,0}-algebras, and ordered additive algebras form a variety of ordered Σ_{+,0}-algebras. A morphism of (ordered) additive algebras is a (monotonic) Σ-algebra morphism which also preserves the sum operation and the constant 0. (For varieties of algebras see any standard text on universal algebra such as [23]. For varieties of ordered algebras see [8].)

Any ordered additive Σ-algebra A may also be equipped with the sum order [29] defined by

a ⊑ b ⇔ ∃c a + c = b.

By (12), it follows that a ≤ b whenever a ⊑ b. The + operation is monotonic with respect to the sum order. However, the other operations may not be monotonic with respect to ⊑.

2.3 ω-continuous additive algebras

An ω-continuous additive Σ-algebra A has three structures:

1. A Σ-algebra structure (A, Σ).

2. A commutative monoid structure (A, +, 0_{A}).

3. An ω-complete partial order structure (A, ≤, ⊥_{A}).

Moreover, it is required that ⊥_{A} = 0_{A} and that the operations σ_{A} as well as the operation + be ω-continuous. Since ⊥_{A} = 0_{A} and ⊥_{A} is least, (5) holds. A morphism of ω-continuous additive algebras is an ω-continuous additive Σ-algebra morphism.

In any ω-continuous additive Σ-algebra A, we may define all countable sums. Indeed, if a_{i} ∈ A for all i ∈ I, where I is countable, define

∑_{i∈I} a_{i} = ⋁_{F} ∑_{i∈F} a_{i},

where the sup is taken over all finite sets F ⊆ I. It is easy to see that for all countable sets I, J such that I is the disjoint union of sets I_{j}, for j ∈ J, and for all families a_{i} ∈ A, i ∈ I,

∑_{i∈I} a_{i} = ∑_{j∈J} ∑_{i∈I_{j}} a_{i}.

Thus, any ω-continuous additive Σ-algebra has an underlying countably complete monoid [29, 27]. Moreover, any morphism of ω-continuous additive Σalgebras preserves all countable sums. Note that any ω-continuous additive Σ-algebra is an ordered additive Σ-algebra. For general facts on continuous algebras see [22, 24].

2.4 Preiteration algebras

Terms, or μ-terms over a signature Σ are defined by the syntax

T ::= x | σ(\overbrace{T, …, T}^{n−times}) | μx.T,

where x ranges over a countably infinite set X of variables, and for each n ≥ 0, σ ranges over Σ_{n}. Thus, the terms defined in the Introduction are in fact terms over the signature Σ_{+,0}. The sets of free and bound variables of a term are defined as usual. We identify any two μ-terms that differ only in the names of the bound variables. Moreover, for any μ-terms t, t_{1}, …, t_{n} and distinct variables x_{1}, …, x_{n}, we write t[t_{1}/x_{1}, …, t_{n}/x_{n}] or t[(t_{1}, …, t_{n})/(x_{1}, …, x_{n})] for the term obtained by simultaneously substituting t_{i} for x_{i}, for each i ∈ [n] = {1, …, n}. Since we may assume that the bound variables in t are different from the variables that have a free occurrence in the terms t_{i}, no free variable in any t_{i} may become bound as the result of the substitution.

Terms over Σ_{+,0} can be interpreted in any ω-continuous additive Σ-algebra A. For each term t, we define an ω-continuous map t_{A} : A^{X} ⟶ A by structural induction.

1. If t is a variable x, then t_{A} = pr_{x} is the corresponding projection A^{X} ⟶ A.

2. If t = σ(t_{1}, …, t_{n}), where σ ∈ Σ_{n}, n ≥ 0, and t_{1}, …, t_{n} are μ-terms, then t_{A} = σ_{A} ∘ ⟨(t_{1})_{A}, …, (t_{n})_{A}⟩, the composite of σ_{A} with the target tupling of the functions (t_{i})_{A}.

3. If t = t_{1} + t_{2}, then t_{A} = + ∘ ⟨(t_{1})_{A}, (t_{2})_{A}⟩.

4. If t = 0, then t_{A} is the constant function A^{X} ⟶ A with value 0_{A}.

5. If t = μx.t′, for some variable x and μ-term t′, then let Y = X − {x}, and let pr_{x} and pr_{Y} denote the corresponding projections A^{X} ⟶ A and A^{X} ⟶ A^{Y}. We define t_{A} = f^{†} ∘ pr_{Y}, where f : A × A^{Y} ⟶ A is the continuous function t′_{A} ∘ ⟨pr_{x}, pr_{Y} ⟩^{−1}, i.e., the composite of t′_{A} with the inverse of the order isomorphism ⟨pr_{x}, pr_{Y} ⟩ : A^{X} ⟶ A × A^{Y}.

Thus, if t = μx.t′, then for each a ∈ A^{X}, (μx.t)_{A}(a) is the least pre-fixed point of the continuous function A ⟶ A,

b ↦ t′_{A}(a_{b}^{x}),

where a_{b}^{x} ∈ A^{X} agrees with a except that it maps x to b.

A preiteration Σ_{+,0}-algebra is a set A together with an assignment of a function t_{A} : A^{X} ⟶ A to each term t over Σ_{+,0} subject to the following rules:

1. For each variable x and a ∈ A^{X}, x_{A}(a) = a(x), i.e., x_{A} is the projection A^{X} ⟶ A corresponding to x.

2. If a, b ∈ A^{X} are such that a(x) = b(x) for all variables x with a free occurrence in t, then t_{A}(a) = t_{A}(b).

3. For all terms t, t_{1}, …, t_{n} and a ∈ A^{X},

(t[t_{1}/x_{1}, …, t_{n}/x_{n}])_{A}(a) = t_{A}(b),

where b(x_{i}) = (t_{i})_{A}, i ∈ [n], and b(x) = a(x), if x ∉ {x_{1}, …, x_{n}}.

4. For all terms t, t′ over Σ_{+,0}, if t_{A}(a) = t′_{A}(a) for all a ∈ A^{X}, then also (μx.t)_{A}(a) = (μx.t′)_{A}(a), for all a ∈ A^{X}, i.e., if t_{A} = t′_{A}, then (μx.t)_{A} = (μx.t′)_{A}.

A morphism A ⟶ B of preiteration Σ_{+,0}-algebras is a function h : A ⟶ B such that the following square commutes for each term t:

[figure: B^{X}; B; t_{B}; A^{X}; A; t_{A}; h^{X}; h]

Here, h^{X} denotes the function a ↦ a′ such that a′(x) = h(a(x)), for all x ∈ X. If A and B are preiteration Σ_{+,0}-algebras such that A is a subset of B and the inclusion of A into B is a morphism, we call A a preiteration subalgebra of B. Moreover, if h is a surjective morphism A ⟶ B, then we call B a quotient of A.

An ordered preiteration Σ_{+,0}-algebra is a preiteration Σ_{+,0}-algebra A which is a partially ordered set such that the function t_{A} induced by any term t is monotonic, and for any terms t, t′, if t_{A} ≤ t′_{A} in the pointwise order, then (μx.t)_{A} ≤ (μx.t′)_{A}. Thus, any ordered preiteration Σ_{+,0}-algebra satisfies the implication

x ≤ y ⇒ t ≤ t[y/x].

(See below for a general treatment of (in)equations and implications.) A morphism of ordered preiteration Σ-algebras is a monotonic preiteration Σ_{+,0}- algebra morphism. If A and B are ordered preiteration Σ_{+,0}-algebras, we call A an ordered preiteration subalgebra of B if A is a preiteration subalgebra of B and the partial order on A is the partial order induced by the order on B, i.e., when the inclusion of A into B is order reflecting. Moreover, we call B a quotient of A if there is a surjective ordered preiteration algebra morphism A ⟶ B. Note that every preiteration Σ_{+,0}-algebra can be regarded as an ordered preiteration Σ_{+,0}-algebra equipped with the discrete partial order which is preserved by any morphism. The following fact is clear.

Proposition 2.2 Every ω-continuous additive Σ-algebra is an ordered preiteration Σ_{+,0}-algebra. If A and B are ω-continuous additive Σ-algebras, and if h : A ⟶ B is an ω-continuous additive Σ-algebra morphism, then h is an ordered preiteration Σ_{+,0}-algebra morphism.

Suppose that A and B are preiteration Σ_{+,0}-algebras and h is a morphism A ⟶ B. The kernel of h, denoted θ_{h}, is defined in the usual way. It is immediate that θ_{h} is an equivalence relation on A that satisfies the following condition: If a, b ∈ A^{X} such that a(x) θ_{h} b(x), for all x ∈ X, then for any μ-term t over Σ_{+,0}, t_{A}(a) θ_{h} t_{A}(b). Moreover, if t_{A}(a) θ_{h} t′_{A}(a), for all a ∈ A^{X}, then (μx.t)_{A}(a) θ_{h} (μx.t′)_{A}(a) for all a ∈ A^{X}. An equivalence relation θ on A with these properties is called a preiteration Σ_{+,0}-algebra congruence, or just congruence, for short. It is clear that the quotient set A/θ can be turned into a preiteration Σ_{+,0}-algebra in a unique way such that the natural map A ⟶ A/θ becomes a morphism. If A and B are ordered preiteration Σ_{+,0}- algebras and h : A ⟶ B is a morphism of ordered preiteration Σ_{+,0}-algebras, then h determines a preorder ≤_{h} on A defined by a ≤_{h} b iff h(a) ≤ h(b). This preorder is compatible in the sense that if a, b ∈ A^{X} such that a(x) ≤_{h} b(x), for all x ∈ X, then for any μ-term t over Σ_{+,0}, t(a) ≤_{h} t(b). Moreover, if a, b ∈ A with a ≤ b, then a ≤_{h} b, and if t_{A}(a) ≤_{h} t′_{A}(a), for all a ∈ A^{X}, then (μx.t)_{A}(a) ≤_{h} (μx.t′)_{A}(a) for all a ∈ A^{X}. If ≤′ is a preorder on A satisfying these conditions, then let θ denote the equivalence relation induced by ≤′ on A. The set A/θ, equipped with the partial order induced by ≤′ on the θ-equivalence classes, also denoted ≤′, can be turned into an ordered preiteration algebra in a unique way such that the natural map A ⟶ A/θ becomes an ordered preiteration Σ_{+,0}-algebra morphism.

Suppose that t and t′ are terms over Σ_{+,0}. We say that the equation (or identity) t = t′ holds in a preiteration Σ_{+,0}-algebra A, or that A satisfies the equation t = t′, if for all a ∈ A^{X},

t_{A}(a) = t′_{A}(a),

i.e., when the functions t_{A} and t′_{A} are equal. Similarly, we say that an inequation t ≤ t′ holds in an ordered preiteration Σ_{+,0}-algebra A, or that A satisfies t ≤ t′, if t_{A} ≤ t′_{A} in the pointwise order of functions. Thus, t = t′ holds in an ordered preiteration Σ_{+,0}-algebra iff both t ≤ t′ and t′ ≤ t hold. More generally, we say that the implication

t_{1} = t′_{1} ∧ … ∧ t_{n} = t′_{n} ⇒ t = t′  (13)

holds in a preiteration Σ_{+,0}-algebra A, where t, t′, t_{i}, t′_{i} are terms over Σ_{+,0}, if for all a ∈ A^{X}, if (t_{i})_{A}(a) = (t′_{i})_{A}(a), for all i ∈ [n], then t_{A}(a) = t′_{A}(a). In a similar way, we can define that an implication

t_{1} ≤ t′_{1} ∧ … ∧ t_{n} ≤ t′_{n} ⇒ t ≤ t′  (14)

holds in an ordered preiteration Σ_{+,0}-algebra.

2.5 Iteration algebras

Some nontrivial (in)equations that hold in all ω-continuous additive Σ-al-gebras are the (in)equations (1) – (9) given in the Introduction. To define the group-equations, we need to extend the μ-notation to term vectors t = (t_{1}, …, t_{n}). Let x = (x_{1}, …, x_{n}) be a vector of distinct variables. When n = 1, μx.t is just the term vector whose unique component is μx_{1}.t_{1}. We identify any term vector of dimension one with its component. If n > 1, let x′ = (x_{1}, …, x_{n−1}), t′ = (t_{1}, …, t_{n−1}) and s = t′[μx_{n}.t_{n}/x_{n}]. (Substitution into a term vector is defined component-wise.) We define

μx.t = (μx′.s, (μx_{n}.t_{n})[μx′.s/x′]).  (15)

The definition is motivated by the Bekić–de Bakker–Scott identity [6, 3]. Thus, for any ω-continuous Σ_{+,0}-algebra A, term vector t = (t_{1}, …, t_{n}) of dimension n, and for any x = (x_{1}, …, x_{n}) and a ∈ A^{X}, (μx.t)_{A}(a) is the least pre-fixed point of the map A^{n} ⟶ A^{n},

b = (b_{1}, …, b_{n}) ↦ t_{A}(a_{b}^{x}),

where of course a_{b}^{x}(x_{i}) = b_{i}, for all i ∈ [n], and a_{b}^{x}(x) = a(x), if x ∉ {x_{1}, …, x_{n}}.

Suppose that t = (t_{1}, …, t_{n}) and t′ = (t′_{1}, …, t′_{n}) are term vectors. We will say that t ≤ t′ holds in an ordered preiteration Σ_{+,0}-algebra if each inequation t_{i} ≤ t′_{i} does. For later use, we note the following fact.

Lemma 2.3 If t ≤ t′ holds in an ordered preiteration Σ_{+,0}-algebra A, then μx.t ≤ μx.t′ also holds in A.

Proof. By induction on n using (15). The basis case n = 1 is part of the assumption that A is an ordered preiteration Σ_{+,0}-algebra. □

Suppose now that G is a finite group of order n with multiplication denoted ∘. Moreover, suppose that the elements of G are the integers in the set [n]. Given a vector x = (x_{1}, …, x_{n}) of distinct variables and an integer i ∈ [n], define

i ^{∘} x = (x_{i∘1}, …, x_{i∘n}).

Thus, i ^{∘} x is obtained by permuting the components of x according to the ith row of the multiplication table of G. The group-identity or group-equation associated with G is the equation

(μx.(t[1 ^{∘} x/x], …, t[n ^{∘} x/x]))_{1} = μy.t[y/x_{1}, …, y/x_{n}],

where t is any μ-term over Σ_{+,0} and y is a (new) variable, and where (μx.(t[1 ^{∘} x/x], …, t[n ^{∘} x/x]))_{1} is the first component of the term vector μx.(t[1 ^{∘} x/x], …, t[n ^{∘} x/x]).

An iteration Σ_{+,0}-algebra is a preiteration Σ_{+,0}-algebra satisfying the equations (7), (8), as well as any group-identity. A morphism of iteration algebras is a preiteration algebra morphism. An ordered iteration Σ_{+,0}-algebra is an iteration Σ_{+,0}-algebra which is an ordered preiteration Σ_{+,0}-algebra. Morphisms of ordered iteration Σ_{+,0}-algebras also preserve the partial order. We call an (ordered) preiteration subalgebra of an (ordered) iteration algebra an (ordered) iteration subalgebra. Note that any quotient of an (ordered) iteration algebra is an (ordered) iteration algebra. and every iteration Σ_{+,0}- algebra may be regarded as an ordered iteration Σ_{+,0}-algebra equipped with the discrete partial order.

We mention a generalization of the group-identities, called the commutative identities. Suppose that ρ_{1}, …, ρ_{n} are mappings [n] ⟶ [n], where n ≥ 1. For each ρ_{i}, let x_{ρ_{i}} = (x_{1ρ_{i}}, …, x_{nρ_{i}}). The commutative identity associated with the ρ_{i} is the equation

(μx.(t[x_{ρ_{1}}/x], …, t[x_{ρ_{n}}/x]))_{1} = μy.t[y/x_{1}, …, y/x_{n}],

where t is any term over Σ_{+,0} and y is a new variable. It is shown in [19] that the commutative identities hold in all iteration algebras. (In fact, the original axiomatization of iteration algebras was based on the Conway identities and the “vector forms” of the commutative identities, cf. [9].)

Proposition 2.4 Any ω-continuous additive Σ-algebra is an ordered iteration Σ_{+,0}-algebra satisfying (1) – (6). Moreover, the least pre-fixed point rule (10) holds in any ω-continuous additive Σ-algebra.

Proof. It is shown in [9, 17] that for any signature Δ, every ω-continuous Δ-algebra is an ordered iteration Δ-algebra. In fact, when Δ = Σ_{+,0}, ordered iteration Δ-algebras satisfying (5) form the variety generated by the ωcontinuous Δ-algebras. (See below for the definition of varieties of (ordered) preiteration algebras.) Applying the easy direction of this general result, we obtain that every ω-continuous additive Σ-algebra is an ordered iteration Σ_{+,0}-algebra satisfying (5). It is also immeadiate that any ω-continuous additive Σ-algebra A satisfies (1) – (4) and the least pre-fixed point rule (10). As for (6), note that for any a ∈ A, both μx.μy.x + y + z and μx.x + z evaluate to the sum of a countable number of copies of a, when z is given the value a. □

The least pre-fixed point rule may be weakened. We will say that an ordered preiteration Σ_{+,0}-algebra satisfies the weak least pre-fixed point rule if for all terms t = t[x] and t′, if the inequation t[t′/x] ≤ t′ holds in A, then so does μx.t ≤ t′, i.e. when (t[t′/x])_{A} ≤ t′_{A} implies (μx.t)_{A} ≤ t′_{A}.

Theorem 2.5 [17] Any ordered preiteration Σ_{+,0}-algebra A satisfying the fixed point identity (9) and the (weak) least pre-fixed point rule is an ordered iteration algebra.

A variety of (ordered) preiteration Σ_{+,0}-algebras is a class V of (ordered) Σ_{+,0}-algebras consisting of the models of some set E of (in)equations between terms over Σ_{+,0}, i.e., such that an (ordered) preiteration Σ_{+,0}-algebra A belongs to V iff A satisfies any (in)equation in E. The set E is called an (in)equational basis, or an (in)equational axiomatization of V. Thus, iteration Σ_{+,0}-algebras form a variety of preiteration Σ_{+,0}-algebras. This variety is axiomatized by the equations (7), (8) and the group-equations corresponding to the finite groups. Similarly, ordered iteration Σ_{+,0}-algebras are axiomatized, in the ordered setting, by the equational axioms of iteration algebras. A variety of (ordered) iteration algebras is a variety of (ordered) preiteration algebras contained in the variety of (ordered) iteration algebras. For a general theory of varieties of iteration algebras we refer to [9]. It is shown in op. cit. that all infinitely generated free algebras exist in any variety of (pre)iteration algebras, but the finitely generated free algebras do not always exist. In fact, for any subset M of the nonnegative integers there is a variety V of iteration algebras such that for any nonnegative integer n, there is an n-generated free algebra in V iff n ∈ M.

3 The completeness results

Our main completeness result is the following theorem.

Theorem 3.1 An inequation holds in all ω-continuous additive Σ-algebras iff it holds in all ordered iteration Σ_{+,0}-algebras satisfying the (in)equations (1) – (6).

Proof. One direction is a restatement of one part of Proposition 2.4. For the opposite direction, we need to show that every inequation t ≤ t′ that holds in all ω-continuous additive Σ_{+,0}-algebras holds in any ordered iteration Σ_{+,0}- algebra A satisfying (1) – (6). But any such A is a quotient of (Σ, A)ISR, the free ordered iteration Σ_{+,0}-algebra on the set A satisfying (1) – (6), see Theorem 7.6. By the Embedding Theorem, Theorem 8.2, (Σ, B)ISR is an ordered iteration Σ_{+,0}-subalgebra of a continuous additive Σ_{+,0}-algebra C. Since t ≤ t′ holds in C, it also holds in A. □

Remark 3.2 The same results holds for continuous additive Σ-algebras having an underlying cpo such that the operations preserve the sup of any directed set. This follows from Theorem 3.1 and the fact that each ω-continuous additive Σ-algebra can be embedded in a continuous additive Σ-algebra.

Corollary 3.3 An inequation holds in all ω-continuous additive Σ-algebras iff it holds in all ordered preiteration Σ_{+,0}-algebras satisfying (1) – (4), (6), the fixed point equation (9), and the least pre-fixed point rule (10).

Proof. Suppose that an inequation t ≤ t′ holds in all ω-continuous additive Σ-algebras. Then, by Theorem 3.1, t ≤ t′ holds in all ordered iteration Σ_{+,0}-algebras satisfying the (in)equations (1) – (6). But by Theorem 2.5, any ordered preiteration Σ_{+,0}-algebra A satisfying (9) and (10) is an ordered iteration algebra. Moreover, by (4) and (9), each such algebra A satisfies the inequation 0 = μx.x ≤ y. It follows that t ≤ t′ holds in any ordered preiteration Σ_{+,0}-algebras satisfying (1) – (4), (6), (9), (10).

Suppose now that t ≤ t′ holds in all ordered preiteration Σ_{+,0}-algebras satisfying (1) – (4), (6), (9), (10). Then, in particular, t ≤ t′ holds in all ω-continuous additive Σ-algebras. □

The same argument proves

Corollary 3.4 An inequation holds in all ω-continuous additive Σ-algebras iff it holds in all ordered preiteration Σ_{+,0}-algebras satisfying (1) – (4), (6), the fixed point equation (9), and the weak least pre-fixed point rule.

One can phrase the above results in several other ways. E.g., one possible formulation of Theorem 3.1 is that the defining (in)equations of ordered iteration Σ_{+,0}-algebras together with (1) – (6) form an axiomatization of the variety generated by the ω-continuous additive Σ-algebras. Corollary 3.3 may be rephrased as the assertion that the variety of ordered preiteration Σ_{+,0}-algebras generated by the continuous additive Σ-algebras and the variety generated by the ordered preiteration Σ_{+,0}-algebras satisfying (1) – (4), (6), the fixed point equation (9) and the least pre-fixed point rule (10) are the same. Syntactic formulations may be obtained by using deductive systems. An equivalent syntactic formulation of Theorem 3.1 is the assertion that an inequation holds in all ω-continuous additive Σ-algebras iff it can be derived from the (in)equations (1) – (6) and those defining ordered iteration algebras using the usual rules of reflexivity and transitivity for manipulating inequalities, the rule of substitution, and the congruence rules

s ≤ s′ ⊢ t[s/x] ≤ t[s′/x]  (16)
t ≤ t′ ⊢ μx.t ≤ μx.t′.  (17)

(Here, we consider each equation t = t′ as an abbreviation for the inequations t ≤ t′ and t′ ≤ t.) In the same way, Corollary 3.3 is equivalent to the assertion that an inequation holds in all ω-continuous additive Σ-algebras iff it can be derived from (1) – (4), (6) and (9) by the above rules and the rule

t[s/x] ≤ s ⊢ μx.t ≤ s.

(This system is irredundant, one may leave out the second congruence rule (17).)

4 Trees

Suppose that Σ is a signature and A is a set disjoint from Σ. We extend the rank function on Σ to Σ ∪ A by defining the rank of each letter in A to be 0. A (Σ, A)-labeled tree S = (V, E, r, λ) consists of a countable set V of vertices, a (countable) set E of (hyper)edges, each having a source in V and a target in V^{n}, for some n ≥ 1, a distinguished vertex r ∈ V, and a labeling function λ : E ⟶ Σ ∪ A. We require that (V, E, r) is a hypertree with root r, so that each vertex v ∈ V is accessible from r by a unique path in the underlying directed tree. We write e : v ⟶ (v_{1}, …, v_{n}) to indicate that e is an edge with source v and target (v_{1}, …, v_{n}). The integer n is called the rank of e. We assume that for each edge e of rank n, eλ ∈ Σ_{n} if n ≠ 1, and eλ ∈ Σ_{0} ∪ A ∪ Σ_{1} if n = 1. Moreover, we require that the target of any edge labeled in Σ_{0} ∪ A is a leaf, i.e., not the source of any edge. Note that each (Σ, A)-labeled tree determines an underlying directed tree obtained by replacing each hyperedge e : v ⟶ (v_{1}, …, v_{n}) by n edges e_{i} : v ⟶ v_{i}, i ∈ [n].

If S = (V, E, r, λ) and S′ = (V′, E′, r′, λ′) are (Σ, A)-labeled trees, a simulation [33] S ⟶ S′ is a relation ρ : V ⟶ V′ satisfying the following conditions.

• The roots are related, i.e., r ρ r′.

• For all e : v ⟶ (v_{1}, …, v_{n}) in S and v′ ∈ V′, if v ρ v′ then there is an edge e′ : v′ ⟶ (v′_{1}, …, v′_{n}) with eλ = e′λ′ and v_{i} ρ v′_{i}, for all i ∈ [n].

It follows that the domain of any simulation S ⟶ S′ is the set V. A functional simulation is a simulation which is a function. An injective functional simulation is a functional simulation which is injective. Injective functional simulations are closely related to the resource simulation of [14, 15]. The following fact is immediate.

Proposition 4.1 If ρ : S ⟶ S′ and ρ′ : S′ ⟶ S′′ are (functional) simulations then the composite ρ′∘ρ is a (functional) simulation S ⟶ S′′. Moreover, if ρ are ρ′ are injective functional simulations, then so is their composition.

Thus (Σ, A)-labeled trees and their (functional) simulations form a category, as do (Σ, A)-labeled trees and injective functional simulations. In either category, the isomorphisms are those simulations which are bijective functions.

Suppose that S = (V, E, r, λ) is a (Σ, A)-labeled tree and v ∈ V. Let V_{v} denote the set of all vertices accessible from v, so that a vertex u is in V_{v} iff there is a directed path from v to u in the underlying directed tree of S. Let E_{v} denote the set of all edges e : u ⟶ (u_{1}, …, u_{n}) such that u ∈ V_{v} (and hence u_{1}, …, u_{n} ∈ V_{v}), and let λ_{v} denote the restriction of λ to E_{v}. The resulting tree S_{v} = (V_{v}, E_{v}, v, λ_{v}) is called the subtree of S rooted at v.

We let (Σ, A)T denote the category of all (Σ, A)-labeled trees and functional simulations. We will sometimes refer to a functional simulation as a morphism. Two subcategories of (Σ, A)T are also of interest: the category (Σ, A)F determined by the finite trees, and the category (Σ, A)R determined by the regular trees. We call a tree regular if it has, up to isomorphism, a finite number of subtrees.

Proposition 4.2 [10] The category (Σ, A)T is countably cocomplete.

Colimits can be constructed in the expected way. For example, if S_{i} = (V_{i}, E_{i}, r_{i}, λ_{i}), i ∈ I are trees, where I is a nonempty countable set, then the coproduct ∑_{i∈I} S_{i} is the disjoint union of the S_{i} with the roots identified. The coproduct injections are the obvious embeddings. Formally, the coproduct is the tree S = (V, E, r, λ), where

V = {r} ∪ ⋃_{i∈I}(V_{i} − {r_{i}})
E = ⋃_{i∈I} E_{i}

and for every e ∈ E_{i}, eλ = eλ_{i}. Moreover, each edge e ∈ E_{i} has the same source and target in S as in S_{i}, except when the source of e in S_{i} is r_{i}. In that case, the source of e in S is the new root r. The empty coproduct, i.e., initial object is the tree ⊥, also denoted 0, with one vertex and no edges.

In addition to coproducts, we will use colimits of ω-chains (S_{n}, f_{n})_{n≥0}, where S_{n} = (V_{n}, E_{n}, r_{n}, λ_{n}), but only in the particular case when the morphisms f_{n} : S_{n} ⟶ S_{n+1} are injective. In fact, we may as well assume that S_{n} ⊆ S_{n+1}, for all n ≥ 0, i.e., that V_{n} ⊆ V_{n+1}, E_{n} ⊆ E_{n+1}, r_{n} = r_{n+1}, and that each edge e ∈ E_{n} has the same source, target and label in S_{n} as in S_{n+1}. Moreover, we may assume that each f_{n} is the inclusion. Then the colimit S = (V, E, r, λ) is the union ∪_{n≥0}S_{n}, where V = ∪_{n≥0}V_{n}, E = ∪_{n≥0}E_{n}, r = r_{0} and each edge e ∈ E_{n} ⊆ E, e has the same sort, target and label in S as in S_{n}. The colimit morphisms are the obvious injections.

Let S = (V, E, r, λ), S′ = (V′, E′, r′, λ′) denote (Σ, A)-labeled trees. We call a functional simulation ρ : S ⟶ S′ normal if for all vertices v_{1}, v_{2} ∈ V, if S_{v_{1}} and S_{v_{2}} are isomorphic and S′_{v_{1}ρ} and S′_{v_{2}ρ} are also isomorphic, then there exist isomorphisms π : S_{v_{2}} ⟶ S_{v_{1}} and π′ : S′_{v_{1}ρ} ⟶ S′_{v_{2}ρ} such that ρ_{v_{2}} = π′ ∘ ρ_{v_{1}} ∘ π. In the next lemma, we write S ≤ S′ to denote that there is an injective simulation S ⟶ S′.

Lemma 4.3 Suppose that S = (V, E, r, λ), S′ = (V′, E′, r′, λ′) are (Σ, A)- labeled trees with S ≤ S′. Then there exists an injective normal functional simulation ρ : S ⟶ S′.

Proof. Let {S_{1} = S, S_{2}, …} and {S′_{1} = S′, S′_{2}, …} be full sets of representatives of isomorphism classes of subtrees of S and S′, respectively. Thus, for each vertex u ∈ V there exist an integer j ≥ 1 and an isomorphism φ_{u} : S_{u} ⟶ S_{j}, and similarly, for each vertex u′ ∈ V′ there exist an integer k ≥ 1 and an isomorphism φ′_{u′} : S′_{u′} ⟶ S′_{k}. For each pair of integers i, j ≥ 1 such that S_{i} ≤ S′_{j}, let ρ_{ij} denote an injective functional simulation S_{i} ⟶ S′_{j}. We define vρ, for v ∈ V, by induction on the depth^{1} of v. It will follow that S_{v} ≤ S′_{vρ}. When the depth is 0, i.e., when v = r, we define vρ = r′. Suppose now that the depth of v is positive. Then there is an edge e : u ⟶ (v_{1}, …, v_{p}) of S such that v appears in (v_{1}, …, v_{p}). Let S_{i} denote the representative of the isomorphism class of the subtree S_{u}, and let S′_{j} denote the representative of the isomorphism class of S′_{uρ}. We define

vρ = vφ_{u}ρ_{ij}φ′_{uρ}.

It is clear that ρ is an injective simulation S ⟶ S′. To prove that ρ is normal, suppose that u_{1}, u_{2} ∈ V such that S_{u_{1}} is isomorphic to S_{u_{2}} and S′_{u_{1}ρ} is ismorphic to S′_{u_{2}ρ}. We need to construct isomorphisms π : S_{u_{2}} ⟶ S_{u_{1}} and π′ : S′_{u_{1}ρ} ⟶ S′_{u_{2}ρ} with ρ_{u_{2}} = π′ ∘ ρ_{u_{1}} ∘ π. We only show how to construct π.

So let v denote a vertex of S_{u_{2}}, i.e., let v ∈ V_{u_{2}}. When v = u_{2}, define vπ = u_{1}. We proceed by induction on the depth of v. Our construction will guarantee that S_{v} is isomorphic to S_{vπ}. In the induction step, there exist an edge w ⟶ (v_{1}, …, v_{n}) such that v is one of the v_{1}, …, v_{n}. Let S_{w} be isomorphic to S_{i}, so that we have the isomorphisms φ_{w} : S_{w} ⟶ S_{i} and φ_{wπ} : S_{wπ} ⟶ S_{i}. We define vπ = vφ_{w}φ_{wπ}^{−1}. □

1The depth of v is the length of the unique path from the root to v in the undelying directed graph.

5 From categories to algebras

Recall from [5] that if C is a category and F is a functor C ⟶ C, then an F -algebra (c, f) consists of an object c and a morphism f : F c ⟶ c. Given F -algebras (c, f) and (c′, f′), an F -algebra morphism (c, f) ⟶ (c′, f′) is a C-morphism g : c ⟶ c′ such that the following square commutes:

[figure: F c′; c′; f′; F c; c; f; F g; g]

Suppose that C is countably cocomplete, so that C has all countable colimits. Moreover, assume that the functor + : C^{2} ⟶ C produces binary coproducts. Since C is countably cocomplete, so is any direct power of C. Call a functor F : C ⟶ D ω-continuous, where C and D are countably cocomplete, if F preserves colimits of ω-diagrams. In particular, +_{C} is a continuous functor C^{2} ⟶ C. The following fact is well-known (see, e.g., [9]).

Proposition 5.1 Suppose that C and D are countably cocomplete categories and F is an ω-continuous functor C ×D ⟶ C. Then for each D-object d, the endofunctor F (−, d) : C ⟶ C has an initial algebra (F^{†}d, μ_{d}). Moreover, the assignment d ↦ F^{†}d is the object map of a unique functor D ⟶ C such that μ = (μ_{d} : d ∈ D) is a natural transformation, in fact a natural isomorphism. Finally, the functor F^{†} is also ω-continuous.

The functor F^{†} can be constructed as follows. Let g : d ⟶ d′ in D and let 0 denote a fixed initial object of C. Then let c_{0} = c′_{0} = 0 and define i_{0} and i′_{0} to be the unique morphisms c_{0} ⟶ F (c_{0}, d) and c′_{0} ⟶ F (c′_{0}, d′), respectively.

For n > 0, define

c_{n} = F (c_{n−1}, d)
c′_{n} = F (c′_{n−1}, d′)
i_{n} = F (i_{n−1}, g)
i′_{n} = F (i′_{n−1}, g).

Thus, i_{n} : c_{n} ⟶ c_{n+1} and i′_{n} : c′_{n} ⟶ c′_{n+1}, for all n ≥ 0. Now F^{†}d is the colimit of the ω-diagram determined by the morphisms i_{n}, and F^{†}d′ is defined in the same way. Let (κ_{n} : c_{n} ⟶ F^{†}d) and (κ′_{n} : c′_{n} ⟶ F^{†}d) denote the appropriate colimit cocones. As for F^{†}g, let f_{0} : c_{0} ⟶ c′_{0} be the identity morphism 0 ⟶ 0, and let

f_{n} = F (f_{n−1}, g),

for all n > 0. It follows by induction that

f_{n+1} ∘ i_{n} = j_{n} ∘ f_{n},

for all n ≥ 0. Thus, there results a unique morphism h : F^{†}d ⟶ F^{†}d′ with

h ∘ κ_{n} = κ′_{n} ∘ f_{n},

for all n ≥ 0. We define F^{†}g to be this morphism h.

Let Σ denote a signature and suppose that for each σ ∈ Σ_{n}, n ≥ 0 there is an ω-continuous functor σ_{C} : C^{n} ⟶ C. Then, to any term t over Σ_{+,0}, we can assign an ω-continuous functor t_{C} : C^{X} ⟶ C in a canonical way. (Recall that X denotes the set of variables.)

1. If t is a variable x, then t_{C} is the corresponding projection functor pr_{x} : C^{X} ⟶ C.

2. If t = σ(t_{1}, …, t_{n}), where σ ∈ Σ_{n} and t_{1}, …, t_{n} are terms, then t_{C} = σ_{C} ∘ ⟨(t_{1})_{C}, …, (t_{n})_{C}⟩, i.e., t_{C} is the composite of σ_{C} and the target tupling of the functors (t_{1})_{C}, …, (t_{n})_{C}.

3. If t = t_{1} + t_{2}, where t_{1} and t_{2} are terms, then t_{C} = +_{C} ∘ ⟨(t_{1})_{C}, (t_{2})_{C}⟩.

4. If t = 0, then t_{C} is the constant functor C^{X} ⟶ C with value 0_{C}, a fixed initial object of C.

5. If t = μx.t′, then let Y = X − {x} and let pr_{x} and pr_{Y} denote the projections C^{X} ⟶ C and C^{X} ⟶ C^{Y}, respectively. Thus, ⟨pr_{x}, pr_{Y} ⟩ is an isomorphism C^{X} ⟶ C × C^{Y} with inverse ⟨pr_{x}, pr_{Y} ⟩^{−1}. We define t_{C} = F^{†} ∘ pr_{Y}, where F is the functor

t′_{C} ∘ ⟨pr_{x}, pr_{Y} ⟩^{−1} : C × C^{Y} ⟶ C.

Proposition 5.2 For any countably cocomplete category C, and for any interpretation of the symbols in Σ by ω-continuous functors, all of the iteration algebra identities hold up to isomorphism, as do the equations (1) – (4) and (6).

Proof. For a proof of the fact that the iteration algebra identities hold, see [9]. The fact that (1) – (4) and (6) hold is obvious. □

Thus, identifying any two isomorphic objects, we obtain an iteration Σ_{+,0}- algebra. For a generalization of Proposition 5.2, see [18].

Corollary 5.3 Suppose that C is a small countably cocomplete category and for each σ ∈ Σ_{n}, n ≥ 0, σ_{C} is an ω-continuous functor C^{n} ⟶ C. Then the object maps of the functors t_{C}, for all terms t over Σ_{+,0}, determine an iteration Σ_{+,0}-algebra on the isomorphisms classes of the objects of C, satisfying the equations (1) – (4) and (6).

The above construction may be applied to the category C = (Σ, A)T of (Σ, A)-labeled trees. The functor +_{(Σ,A)T} : (Σ, A)T^{2} ⟶ (Σ, A)T forms binary coproducts as given above. When φ_{i} : S_{i} ⟶ R_{i}, i = 1, 2, φ_{1} +φ_{2} : S_{1} +S_{2} ⟶ R_{1}+R_{2} takes the root of S_{1}+S_{2} to the root of R_{1}+R_{2} and maps each nonroot vertex v of S_{i} to vφ_{i}, i = 1, 2. The tree 0 was defined above. For each σ ∈ Σ_{n}, we define the functor σ_{(Σ,A)T} : (Σ, A)T^{n} ⟶ (Σ, A)T as follows. Given trees S_{1}, …, S_{n} with distinguished vertices r_{1}, …, r_{n}, respectively, σ(S_{1}, …, S_{n}) is the tree obtained from the S_{i} by taking their disjoint union and adding a new vertex r and a new edge e : r ⟶ (r_{1}, …, r_{n}) labeled σ. Vertex r is the new root. When σ ∈ Σ_{0}, we define σ_{(Σ,A)T} to be the constant functor determined by the tree which has a unique edge, which is labeled σ. On morphisms, σ_{(Σ,A)T} is defined in the expected way. See [9] for details.

Proposition 5.4 [10] Each functor σ_{(Σ,A)T} is ω-continuous.

Corollary 5.5 [10] The isomorphism classes of (Σ, A)-labeled trees form an iteration Σ_{+,0}-algebra satisfying the equations (1) – (4) and (6).

We let (Σ, A)T denote this iteration Σ_{+,0}-algebra. It was shown in [10] that the regular trees determine an iteration Σ_{+,0}-subalgebra of (Σ, A)T. We denote this algebra by (Σ, A)R. Moreover, the finite trees determine an additive Σ-algebra (Σ, A)F.

Corollary 5.6 (Σ, A)R is an iteration Σ_{+,0}-algebra satisfying the equations (1) – (4) and (6). (Σ, A)F is a Σ_{+,0}-algebra satisfying the equations (1) – (3).

The following result gives an algebraic characterization of the iteration Σ_{+,0}- algebra (Σ, A)R. Let us identify each letter a ∈ A with the tree which has a unique vertex and a unique edge, which is labeled a.

Theorem 5.7 [10] The iteration Σ_{+,0}-algebra (Σ, A)R is freely generated by the set A in the variety of all iteration Σ_{+,0}-algebras satisfying the equations (1) – (4) and (6).

The meaning of this result is that for any iteration Σ_{+,0}-algebra satisfying the equations (1) – (4), (6), and for any function h : A ⟶ B, there is a unique iteration Σ_{+,0}-algebra morphism h^{♯} : (Σ, A)R ⟶ B extending h.

Corollary 5.8 An equation holds in all (pre)iteration Σ_{+,0}-algebras derived from small countably complete categories as in Corollary 5.3 iff it holds in all iteration Σ_{+,0}-algebras satisfying (1) – (4) and (6).

Suppose that t is a μ-term over Σ_{+,0} and n is a nonnegative integer. Below we will write nt for the n-fold sum of t with itself, where we take advantage of the associativity of +. When n = 0, we define nt to be the term 0. Moreover, we define ∞t = μx.x + t, where x does not occur in t. We let ∞ + n = n + ∞ = ∞ and n ≤ ∞ for all n ∈ {0, 1, …, ∞}. For later use, we note two simple facts.

Corollary 5.9 The following equation holds in any iteration Σ_{+,0}-algebra satisfying (1) – (4) and (6):

ny + my = (n + m)y  (18)

where n, m are nonegative integers or ∞. When n, m ≠ ∞, (18) holds in all additive Σ-algebras.

Proof. Equation (18) holds in all algebras (Σ, A)R. □

Corollary 5.10 For all n ≤ m, the inequation

ny ≤ my  (19)

holds in all ordered iteration Σ_{+,0}-algebras satisfying (1) – (6). When n, m ≠ ∞, (19) holds in all ordered additive Σ-algebras.

Proof. If n ≤ m, then there exits some k with n + k = m. Thus, by Corollary 5.9, ny + ky = (n + k)y = my holds. But then ny ≤ my also holds, by (12). □

5.1 The injective simulation preorder

We will consider a preorder on trees. Suppose that S and T are (Σ, A)-labeled trees. We define S ≤ T if there is an injective functional simulation S ⟶ T. Moreover, we define S ≡ T if both S ≤ T and T ≤ S hold. The relation ≤ is called the injective simulation preorder and ≡ the injective simulation equivalence.

Example 5.11 There exist nonisomorphic regular trees S, T with S ≡ T. For one example, let σ ∈ Σ_{1}, and let S = σ(0)+∞σ(σ(0)) and T = ∞σ(σ(0)).

The following facts are obvious.

Lemma 5.12 Suppose that σ ∈ Σ_{n} and S_{i} ≤ R_{i}, for i ∈ [n]. Then σ(S_{1}, …, S_{n}) ≤ σ(R_{1}, …, R_{n}). In fact, if φ_{i} : S_{i} ⟶ R_{i}, i ∈ [n] are injective, then so is σ(φ_{1}, …, φ_{n}) : σ(S_{1}, …, S_{n}) ⟶ σ(R_{1}, …, R_{n}).

Lemma 5.13 If S_{1} ≤ S_{2} and R_{1} ≤ R_{2}, then S_{1} +S_{2} ≤ R_{1} +R_{2}. Moreover, if φ_{i} : S_{i} ⟶ R_{i}, i = 1, 2 are injective, then so is φ_{1} + φ_{2} : S_{1} + S_{2} ⟶ R_{1} + R_{2}.

Proposition 5.14 For all μ-terms t over Σ_{+,0} and for all families of (Σ, A)- labeled trees S = (S_{y})_{y∈X} and R = (R_{y})_{y∈X} with S_{y} ≤ R_{y} for y ∈ X, it holds that t_{(Σ,A)T} (S) ≤ t_{(Σ,A)T} (R). Moreover, if φ = (φ_{y})_{y∈X} such that each functional simulation φ_{y} : S_{y} ⟶ R_{y}, y ∈ X is injective, then so is t_{(Σ,A)T} (φ) : t_{(Σ,A)T} (S) ⟶ t_{(Σ,A)T} (R).

Proof. We argue by induction on the structure of t. Our claim is obvious when t is a variable or t = 0. If t is of the form σ(t_{1}, …, t_{n}), or t_{1} + t_{2}, the result follows by the previous lemmas. Assume finally that t = μx.t′, for some variable x and term t′. Let F denote the functor (Σ, A)T ⟶ (Σ, A)T defined by

f : U ⟶ V ↦ t′(S_{f}^{x}) : t′(S_{U}^{x}) ⟶ t′(S_{V}^{x}).

Here, S_{f}^{x} denotes the assignment that takes x to f and any variable y ≠ x to the identity S_{y} ⟶ S_{y}. Then t(S) is the colimit of the ω-diagram i_{n} : U_{n} ⟶ U_{n+1}, where U_{0} = 0 is the initial tree, U_{n+1} = F U_{n} and i_{n+1} = F i_{n}. Of course, i_{0} is the unique morphism U_{0} ⟶ U_{1}. In the same way, t(R) is the colimit of the ω-diagram j_{n} : V_{n} ⟶ V_{n+1} constructed in the same way using the functor G : (Σ, A)T ⟶ (Σ, A)T

f : U ⟶ V ↦ t′(R_{f}^{x}) : t′(R_{U}^{x}) ⟶ t′(R_{V}^{x}).

Since i_{0} and j_{0} are injective, it follows by the induction assumption that each of the morphisms i_{n} and j_{n} is also injective. Assume that φ_{y} : S_{y} ⟶ R_{y} is an injective functional simulation, for each y. Then let g_{0} denote the identity functional simulation 0 ⟶ 0, and let

g_{n+1} = t′(φ_{g_{n}}^{x}), n ≥ 0.

By the induction assumption we have that these morphisms are also injective. Since

g_{n+1} ∘ i_{n} = j_{n+1} ∘ g_{n},

for all n ≥ 0, there results a mediating morphism g : t(S) ⟶ t(R). We may as well assume that the i_{n} and j_{n} are inclusions, in which case t(S) is the union of the U_{n} and t(R) the union of the V_{n}, moreover, for any vertex u of U_{n}, n ≥ 0, we have g(u) = g_{n}(u). Thus, g is injective, proving that t(φ) is also injective. □

Proposition 5.15 Let s, t denote μ-terms over Σ_{+,0}. Suppose that for all families R = (R_{y})_{y∈X} of (regular) (Σ, A)-labeled trees we have s(R) ≤ t(R). Then also (μx.t)(R) ≤ (μx.t′)(R), for all families R of regular (Σ, A)-labeled trees and for all x ∈ X.

Proof. For a family R = (R_{y})_{y∈X} of regular trees, let F denote the functor (Σ, A)T ⟶ (Σ, A)T, defined on objects by S ↦ s(R_{S}^{x}). On morphisms, F is defined in a similar way. Let G denote the corresponding functor using term t. Then F^{†} = (μx.s)(R_{y}/y) is the colimit of the ω-diagram F^{n}(i_{0}) : F^{n}(0) ⟶ F^{n+1}(0), where 0 is the initial tree and i_{0} denotes the unique functional simulation 0 ⟶ F (0). Also, G^{†} = (μx.t)(R_{y}/y) is the colimit of the ω-diagram G^{n}(j_{0}) : G^{n}(0) ⟶ G^{n+1}(0) defined in the same way. By Proposition 5.14, each F^{n}(i_{0}) and G^{n}(j_{0}) is injective, so that we may assume as before that each F^{n}(i_{0}) and G^{n}(j_{0}) is an inclusion, and that F^{†} and G^{†} are the unions of the F^{n}(0) and the G^{n}(0), respectively. Suppose that S is a finite tree with S ≤ F^{†}. Then there is some n such that S ≤ F^{n}(0). But it follows from our assumption on s and t that F^{n}(0) ≤ G^{n}(0), so that S ≤ G^{n}(0) and S ≤ G^{†}. Since F^{†} and G^{†} are regular, by Lemma 8.1, proved independently, we have F^{†} ≤ G^{†}. □

By the previous facts, the injective simulation equivalence classes of regular (Σ, A)-labeled trees form an iteration Σ_{+,0}-algebra. Let (Σ, A)ISR denote this iteration Σ_{+,0}-algebra. In fact, identifying any tree with its isomorphism class, ≤ induces a compatible preorder on (Σ, A)R, so that (Σ, A)ISR is the quotient of (Σ, A)R under the natural map taking a tree T to its injective simulation equivalence class T/≡. Equipped with the partial order induced by ≤, (Σ, A)ISR is an ordered iteration Σ_{+,0}-algebra. In fact, we have:

Proposition 5.16 (Σ, A)ISR is an ordered iteration Σ_{+,0}-algebra satisfying (1) – (6).

Proof. We have already noted that (Σ, A)ISR is an ordered iteration Σ_{+,0}- algebra which is a quotient of (Σ, A)R. Thus, by Corollary 5.6, (1) – (4) and (6) hold in (Σ, A)ISR. The inequation (5) is obvious. □

Let (Σ, A)ISF denote the subalgebra of (Σ, A)ISR determined by the finite trees. Clearly, (Σ, A)ISF is an ordered additive Σ-algebra.

6 Finite trees

In this section we show that the injective simulation equivalence classes of finite (Σ, A)-labeled trees form the free ordered additive Σ-algebra on A. In fact, we show that two finite trees are injective simulation equivalent iff they are isomorphic. Thus, (Σ, A)ISF is just (Σ, A)F equipped the partial order induced by injective simulations. First we consider the unordered case.

Proposition 6.1 [10] The algebra (Σ, A)F of isomorphism classes of finite (Σ, A)-labeled trees is freely generated by A in the variety of additive Σ-algebras.

Proposition 6.2 If S and S′ are finite (Σ, A)-labeled trees with S ≡ S′ then S and S′ are isomorphic.

Proof. Let φ and ψ be injective morphisms S ⟶ S′ and S′ ⟶ S, respectively. Then the composite ψ ∘ φ is necessarily an isomorphism S ⟶ S, and φ ∘ ψ is an isomorphism S′ ⟶ S. But then φ and ψ are also isomorphisms. □

Remark 6.3 In the same way, for any “finitely branching” (Σ, A)-labeled trees S, T, if S ≡ T then S is isomorphic to T.

We use the above results to prove

Proposition 6.4 The algebra (Σ, A)ISF, equipped with the partial order ≤, is freely generated by A in the variety of ordered additive Σ-algebras.

Proof. We already know that (Σ, A)ISF is an ordered additive Σ-algebra. By Proposition 6.2, (Σ, A)ISF may be represented as the ordered additive Σ-algebra of isomorphism classes of finite trees, equipped with the partial order ≤. We may as well identify each tree with its isomorphism class and regard the elements of (Σ, A)ISF as finite (Σ, A)-labeled trees.

Suppose that B is an ordered additive Σ-algebra and h is a function A ⟶ B. By Proposition 6.1, h extends to a unique additive Σ-algebra morphism h^{♯} : (Σ, A)ISF ⟶ B. We need to show that h^{♯} preserves the partial order. Let S and S′ be finite trees with S ≤ S′. We argue by induction on the depth of S to show that h^{♯}(S) ≤ h^{♯}(S′). When S = 0, our claim holds by (5). Suppose now that the depth of S′ is positive. We can write S as

S = ∑_{i∈I} σ_{i}(S_{i1}, …, S_{in_{i}}),

where I is a finite nonempty set, and for each i ∈ I, σ_{i} is a symbol in Σ(A)_{n_{i}} and S_{i1}, …, S_{in_{i}} are finite trees of depth less than the depth of S. Since S ≤ S′, we can also write

S′ = T + ∑_{i∈I} σ_{i}(S′_{i1}, …, S′_{in_{i}}),

where T and the S′_{ij}, j ∈ [n_{i}], i ∈ I are finite trees such that S_{ij} ≤ S′_{ij}, for all i, j. Thus, using the induction hypothesis and the fact that the operations are monotonic, as well as (12),

h^{♯}(S) = ∑_{i∈I} σ_{i}(h^{♯}(S_{i1}), …, h^{♯}(S_{in_{i}}))
≤ ∑_{i∈I} σ_{i}(h^{♯}(S′_{i1}), …, h^{♯}(S′_{in_{i}}))
≤ h^{♯}(T) + ∑_{i∈I} σ_{i}(h^{♯}(S′_{i1}), …, h^{♯}(S′_{in_{i}}))
= h^{♯}(S′). □

Corollary 6.5 Additive Σ-algebras and ordered additive Σ-algebras satisfy the same equations.

7 Regular trees

Let Σ denote a signature and let A be a set. In this section we prove that the algebra (Σ, A)ISR of injective simulation equivalence classes of regular (Σ, A)-labeled trees, equipped with the injective simulation order, is freely generated by A in the variety of ordered iteration Σ_{+,0}-algebras satsifying (1)

– (6).

Given (Σ, A)-labeled trees S and S′ and a functional simulation ρ : S ⟶ S′, for any vertex u of S let ρ_{u} denote the functional simulation S_{u} ⟶ S′_{uρ} induced by ρ, so that ρ_{u} is the restriction of ρ to the vertices of S_{u}.

A (Σ, A)-normal representation of dimension n in the variables x_{1}, …, x_{n}, y_{1}, …, y_{p} is an ordered pair D = (t, a), where t = (t_{1}, …, t_{n}) is an ndimensional vector of terms over Σ_{+,0} in the free variables x_{1}, …, x_{n}, y_{1}, …, y_{p}, and where a = (a_{1}, …, a_{p}) ∈ A^{p}. Moreover, each term t_{i} is primitive, i.e., a finite sum of terms of the form kσ(x_{j_{1}}, …, x_{j_{m}}) or ky_{j}, where k ≠ 0, σ ∈ Σ_{m}, m ≥ 0, j_{1}, …, j_{m} ∈ [n] and j ∈ [p]. (It is allowed that k = ∞, and we take advantage of the associativity and commutativity of +.) Let us denote x = (x_{1}, …, x_{n}) and y = (y_{1}, …, y_{p}). The behavior of D, denoted |D| is the first component of (μx.t)_{(Σ,A)R}(a/y). Thus, the behavior of D is a regular tree in (Σ, A)R. The term μx.t itself will be called normal of dimension n. The variables y_{j} are called the parameters.

Each regular tree T ∈ (Σ, A)R is known to be the behavior of a normal representation D = (t, a). To construct D, let T_{1}, …, T_{n} be an enumeration of the subtrees of T with T = T_{1}, and let a_{1}, …, a_{p} be an enumeration of those elements of A which appear as labels of some edges of T. We define t = (t_{1}, …, t_{n}) and a = (a_{1}, …, a_{p}), where each t_{i} corresponds to T_{i} in the following manner. Each edge e : v ⟶ (v_{1}, …, v_{m}) whose source is the root of T_{i} is labeled by some symbol σ ∈ Σ, or some component of a. Suppose that e is labeled σ ∈ Σ_{m}, m > 0. Then let T_{j_{1}}, …, T_{j_{m}} denote the subtrees rooted at the vertices v_{1}, …, v_{m}, respectively, and let k denote the total number of edges v ⟶ (v′_{1}, …, v′_{m}) labeled σ ∈ Σ_{m} such that the subtrees rooted at the vertices v′_{1}, …, v′_{m} are isomorphic to the trees T_{j_{1}}, …, T_{j_{m}}, respectively. (If there are an infinite number of such edges, then k = ∞.) Then kσ(x_{j_{1}}, …, x_{j_{m}}) is a summand of t_{i}. If σ ∈ Σ_{0}, then kσ is a summand of t_{i}, where k is the number of those edges with source v labeled σ. Similarly, for each a_{j}, ky_{j} is a summand of t_{i}, where k is determined in the same way. The term t_{i} is the sum of all such summands. We call the normal representation D constructed above the minimal representation of T. (Note that the minimal representation is unique only up to a rearrangement of the components of t and a and renaming of the variables.)

Example 7.1 Suppose that σ ∈ Σ_{1} and that T is a regular tree with nonisomorphic subtrees T_{1}, T_{2}, where T_{1} is T, T_{2} is the tree 0, and where there are 4 edges leaving the root. Two of the edges, labeled σ, lead to vertices whose corresponding subtrees are isomorphic to T, a third edge, also labeled σ, leads to a vertex with no outgoing edge, and the last edge is labeled a ∈ A. Then the normal representation for T is

(μ(x_{1}, x_{2}).(2σ(x_{1}) + σ(x_{2}) + a, 0), a).

It is known that for each i, the ith component of (μx.t)(a) is the tree T_{i}. In particular, we have:

Proposition 7.2 [9] For the normal representation D = (t, a) of the tree T ∈ (Σ, A)R, it holds that |D| = T.

Given normal terms μx.t and μy.t′, of dimension n and m respecively, and a function ρ : [n] ⟶ [m], where x = (x_{1}, …, x_{n}), y = (y_{1}, …, y_{m}), t = (t_{1}, …, t_{n}) and t′ = (t′_{1}, …, t′_{m}), we define ρ ∘ t′ to be the term vector (t′_{1ρ}, …, t′_{nρ}). Moreover, we define

t ∘ ρ = (t_{1}[y_{1ρ}/x_{1}, …, y_{nρ}/x_{n}], …, t_{n}[y_{1ρ}/x_{1}, …, y_{nρ}/x_{n}]).

Recall that when t = (t_{1}, …, t_{n}), t′ = (t′_{1}, …, t′_{n}) and A is a preiteration Σ_{+,0}-algebra, we say that t = t′ holds in A if each t_{i} = t′_{i} does. We use a similar convention for inequations t ≤ t′.

Lemma 7.3 Suppose that S and S′ are trees with S ≤ S′. Then there exist normal representations (μx.t, a) and (μy.t′, a) for S and S′ and a function ρ : [n] ⟶ [m], where n denotes the dimension of μx.t and m denotes the dimension of μy.t′, such that 1ρ = 1 and

t ∘ ρ ≤ ρ ∘ t′

holds in all ordered preiteration Σ_{+,0}-algebras satisfying (1), (2), (3), (18) and (19).

Proof. Let {S_{1} = S, S_{2}, …, S_{k}} and {S′_{1} = S′, S′_{2}, …, S′_{m}} denote full sets of representatives of isomorphism classes of subtrees of S and S′, respectively. By Lemma 4.3, there is an injective normal morphism φ : S ⟶ S′. Let I denote the set of all ordered pairs (i, j), i ∈ [k], j ∈ [m] such that there is a vertex u of S such that S_{u} is isomorphic to S_{i} and S′_{uφ} is isomorphic to S′_{j}. Let n denote the number of elements of the set I and let us fix an enumeration of I starting with the pair (1, 1). Call an edge e : u ⟶ (v_{1}, …, v_{p}) of S an

(i, j) ⟶ ((i_{1}, j_{1}), …, (i_{p}, j_{p}))

type edge, where i, i_{1}, …, i_{p} ∈ [k] and j, j_{1}, …, j_{p} ∈ [m], if S_{u} is isomorphic to S_{i}, S_{uφ} is isomorphic to S′_{j}, and for each ℓ, S_{v_{ℓ}} is isomorphic to S_{i_{ℓ}} and S′_{v_{ℓ}φ} is isomorphic to S′_{j_{ℓ}}. Note that (i, j) is necessarily in I as are the ordered pairs (i_{1}, j_{1}), …, (i_{p}, j_{p}).

We define the term μx.t. The components of the vector x correspond to the elements of I in a bijective manner according to the fixed enumeration of I. Let x_{ij} denote the variable corresponding to the ordered pair (i, j), and let t_{ij} denote the corresponding component of t. Moreover, let a_{1}, …, a_{q} be all the letters of A that appear in S or S′, in some fixed enumeration, and let z_{1}, …, z_{q} be variables corresponding to these letters. (We assume that these variables are different from the components of x.) To define t_{ij}, consider a vertex u of S such that S_{u} is isomorphic to S_{i} and S′_{uφ} is isomorphic to S′_{j}. For each σ ∈ Σ_{p}, p > 0, which appears as the label of an outgoing edge of u, the root of S_{u}, and for each sequence α = ((i_{1}, j_{1}), …, (i_{p}, j_{p})) ∈ I^{p}, let s = s(σ, (i, j) ⟶ α) denote the number of edges e : u ⟶ (v_{1}, …, v_{p}) labeled σ and having type (i, j) ⟶ ((i_{1}, j_{1}), …, (i_{p}, j_{p})). When σ_{0} ∈ Σ_{0}, let s(σ_{0}, i) denote the total number of edges with source u labeled σ_{0}. Moreover, for each ℓ ∈ [q], let s_{iℓ} denote the number of edges with source u labeled a_{ℓ}. We define

t_{ij} = ∑_{σ,α} s(σ, (i, j) ⟶ α)σ(x_{i_{1}j_{1}}, …, x_{i_{p}j_{p}}) + ∑_{σ_{0}} s(σ_{0}, i)σ + ∑_{ℓ} s_{iℓ}z_{ℓ}.

As for μy.t′, we take the minimal normal representation of S′. Thus, the components of y and t′ correspond to the subtrees of S′, so that y = (y_{1}, …, y_{m}) and t′ = (t′_{1}, …, t′_{m}) with y_{j} and t′_{j} corresponding to S′_{j}, for each j ∈ [m]. Moreover, each t′_{j} is given by

t′_{j} = ∑_{σ,β} s′(σ, j ⟶ β)σ(y_{j_{1}}, …, y_{j_{p}}) + ∑_{σ_{0}} s′(σ_{0}, j) + ∑_{ℓ} s′_{ℓ}z_{ℓ}.

Here, σ ∈ Σ_{p}, p > 0 ranges over the symbols which appear as labels of outedges of the root of S′_{j}, β = (j_{1}, …, j_{p}) ∈ [m]^{p}, and where s′(σ, j ⟶ β) is the number of outedges of the root of S′_{j} labeled σ of type j ⟶ (j_{1}, …, j_{p}), i.e., whose targets determine a sequence of vertices whose corresponding subtrees are isomorphic to S′_{j_{1}}, …, S′_{j_{p}}, respectively. Moreover, σ_{0} ranges over those symbols in Σ_{0} that appear as labels of outedges of the root of S′_{j}, s′(σ_{0}, j) is the corresponding multiplicity, and for each ℓ ∈ [q], s′_{jℓ} is the number of outedges of the root of S′_{j} labeled a_{ℓ}.

By Proposition 7.2, we have that |(μy.t′, a)| = S′. Define the function ρ :

[n] ⟶ [m] such that it maps any integer in [n] corresponding to an ordered pair (i, j) in the fixed enumeration of the set I to the integer j. Suppose that (i, j) ∈ I. Since S_{i} ≤ S_{j}, it is clear that for any σ ∈ Σ_{p} with p > 0 and j_{1}, …, j_{p},

∑_{i_{1},...,i_{p}} s(σ, (i, j) ⟶ (i_{1}, j_{1}), …, (i_{p}, j_{p})) ≤ s′(σ, j ⟶ (j_{1}, …, j_{p})).

And for all σ_{0} ∈ Σ_{0} and ℓ ∈ [q],

s(σ_{0}, i) ≤ s′(σ_{0}, j),

and

s_{iℓ} ≤ s′_{jℓ},

It follows that t ∘ ρ ≤ ρ ∘ t′ holds modulo (1), (2), (3), (18) and (19) and the monotonicity of +, i.e., t ∘ ρ ≤ ρ ∘ t′ holds in any ordered preiteration Σ_{+,0}-algebra satisfying the (in)equations (1), (2), (3), (18) and (19).

To complete the proof, we still need to show that |(μx.t, a)| = S. But consider the minimal normal representation (μx′′.t′′, a) for S. Here x′′ = (x′′_{1}, …, x′′_{k}), t′′ = (t′′_{1}, …, t′′_{k}) such that for each i, x′′_{i} and t′′_{i} correspond to S_{i}, i.e., the ith component of (μx′′.t′′)(a) is isomorphic to S_{i}. If τ denotes the function [n] ⟶ [k] corresponding to the assignment I ⟶ [k], (i, j) ↦ i, then we clearly have t∘τ = τ ∘t′′ modulo (1), (2), (3) and (18). Thus, by Lemma 7.5, for each (i, j) in I, the (i, j)th component of (μx.t)(a) is isomorphic to the ith component of (μx′′.t′′)(a). □

Lemma 7.4 Let μx.t and μy.t′ be normal terms of dimension n and m, respectively. Suppose that there is a function ρ : [n] ⟶ [m] with t ∘ ρ ≤ ρ ∘ t′ modulo (1), (2), (3), (18) and (19). Then there is a normal term μx.s of dimension n such that t ≤ s and s ∘ ρ = ρ ∘ t′ hold modulo (1), (2), (3), (18) and (19).

Proof. Assume that t = (t_{1}, …, t_{n}) and t′ = (t′_{1}, …, t′_{m}). For each i ∈ [n] there is a term t′′_{i} with (t_{i} + t′′_{i}) ∘ ρ = t′_{iρ} modulo (1), (2), (3) and (18). Moreover, t′′_{i} is the sum of primitive terms. Define s_{i} = t_{i} + t′′_{i} and s = (s_{1}, …, s_{n}). Then t ≤ s modulo (1), (2), (3), (18) and (19). □

Lemma 7.5 Suppose that μx.t and μy.t′ are normal terms of dimension n and m in the parameters z = (z_{1}, …, z_{p}). Let ρ denote a function [n] ⟶ [m]. If t ∘ ρ = ρ ∘ t′, modulo (1), (2), (3) and (18), then for any a ∈ A^{p} and i ∈ [n], the ith component of (μx.t)(a) is isomorphic to the (iρ)th component of (μy.t′)(a). Thus, if 1ρ = 1, then trees represented by (μx.t, a) and (μy.t′, a) are isomorphic.

Proof. We know that (μx.t)(a) is the colimit of the the ω-diagram (i_{k} : s_{k} ⟶ s_{k+1})_{k≥0}, where s_{0} is the n-tuple (0, …, 0), s_{k+1} = t(s_{k}, a/x, z), i_{k+1} = t(i_{k}, a/x, z), k ≥ 0. Also, (μy.t′)(a) is the colimit of an ω-diagram (i′_{k} : s′_{k} ⟶ s′_{k+1})_{k≥0} constructed in the same way. But since t ∘ ρ = ρ ∘ t′, modulo the associativity and commutativity of + and (18), we have that s_{k} = ρ ∘ s′_{k}, for all k ≥ 1, i.e., for any i ∈ [n], the ith component of s_{k} is the same as the (iρ)th component of s′_{k}. In the same way, i_{k} = ρ ∘ i′_{k}. It follows that (μx.t)(a) = ρ ∘ (μx.t′)(a). □

Theorem 7.6 For each signature Σ and set A, the ordered iteration Σ_{+,0}- algebra (Σ, A)ISR is freely generated by A in the variety of ordered iteration Σ_{+,0}-algebras satisfying the (in)equations (1) – (6).

Proof. We already know that (Σ, A)ISR is an ordered iteration Σ_{+,0}-algebra satisfying (1) – (6), cf. Proposition 5.16. Suppose that B is another ordered iteration Σ_{+,0}-algebra satisfying the equations (1) – (6). Let φ be a function A ⟶ B. By Theorem 5.7, there is an iteration Σ_{+,0}-algebra morphism \overline{φ} : (Σ, A)R ⟶ B extending φ. We show that for all trees S, S′ in (Σ, A)R, if S ≤ S′, then \overline{φ}(S) ≤ \overline{φ}(S′). By Lemma 7.3 there exist normal representations (μx.t, a) and (μy.t′, a) of dimensions n and m in the parameters z = (z_{1}, …, z_{p}) with |(μx, t, a)| = S, |(μy.t′, a)| = S′ and such that for some ρ : [n] ⟶ [m] with 1ρ = 1, t ∘ ρ ≤ ρ ∘ t′ holds modulo (1), (2), (3), (18), (19). Moreover, by Lemma 7.4, there is a normal representation (μx.s, a) of dimension n such that t ≤ s modulo the same inequations, and s ∘ ρ = ρ ∘ t′ modulo (1), (2), (3) and (18). By Lemma 7.5, |(μx.s, a)| = S′. Thus, denoting b = (b_{1}, …, b_{p}) with b_{i} = a_{i}\overline{φ}, i ∈ [p], by Lemma 2.3,

\overline{φ}(S) = \overline{φ}((μx.t)_{(Σ,A)R}(a))
= (μx.t)_{B}(b)
≤ (μx.s)_{B}(b)
= \overline{φ}((μx.s)_{(Σ,A)R}(a))
= \overline{φ}(S′).

It is now easy to complete the proof. For each ≡-equivalence class S/ ≡ ∈ (Σ, A)R/ ≡, define φ^{♯}(S/ ≡) = \overline{φ}(S). By the above argument, φ^{♯} is a welldefined ordered iteration Σ_{+,0}-algebra morphism (Σ, A)ISR ⟶ B extending φ. The uniqueness of φ^{♯} is obvious. □

8 An embedding theorem

In this section we show that for each set A, (Σ, A)ISR can be embedded in an ω-continuous additive Σ-algebra. By Proposition 6.4, (Σ, A)ISF is freely generated by A in the variety of all ordered additive Σ-algebras. It is known, cf. [8, 24], that for each signature Δ and each variety V of ordered Δalgebras, the ω-continuous algebras in V and their ω-continuous morphisms form a reflective subcategory of V. Moreover, for each B ∈ V, there is an order reflecting morphism from B into the free ω-continuous algebra generated by B. The free ω-continuous algebra on B may be constructed as the completion of B by ω-ideals generated by countable directed subsets (or ω-chains) of B. We show that when Δ is Σ_{+,0} and V is the variety of ordered additive Σ-algebras, the ordered iteration Σ_{+,0}-algebra (Σ, A)ISR embeds in the completion of (Σ, A)ISF.

Lemma 8.1 Suppose that S and T are (Σ, A)-labeled trees such that T is regular and F ≤ T holds for all finite trees F with F ≤ S. Then S ≤ T.

Proof. Our claim is obvious when S is finite, so that below we assume that S is infinite. Let F_{0}, F_{1}, … be an enumeration of finite trees F_{i} ⊆ S with the property that every vertex of S appears in all but a finite number of the F_{i}. By our assumption, for each i there is an injective functional simulation φ_{i} : F_{i} ⟶ T. We show how to construct an injective functional simulation φ : S ⟶ T. When v is the root of S, define vφ to be the root of T. Suppose now that φ has been defined on all vertices of S of depth not exceeding d such that φ is injective on these vertices and for every vertex u of depth ≤ d, T_{uφ} is isomorphic to T_{uφ_{i}} for all i in an infinite set I of nonnegative integers. Suppose that u has depth d. For simplicity, in the argument below we will assume that each edge leaving u is labeled in Σ_{1}. The generalization of the argument is left to the reader. Let v_{0}, v_{1}, v_{2}, … be an enumeration of the successors of u. We define the pairwise different successors v_{0}φ, v_{1}φ, v_{2}φ … of uφ such that for each k there exists an infinite set I_{k} ⊆ I with the following property:

For all j < k and i ∈ I_{k}, the edges u ⟶ v_{j}, uφ ⟶ v_{j}φ and uφ_{i} ⟶ v_{j}φ_{i} have the same label and T_{v_{j}φ} is isomorphic to T_{v_{j}φ_{i}}.

When k = 0, let I_{0} = I. Suppose that k > 0 and that we have already defined v_{0}φ, …, v_{k−1}φ and I_{k}. Since v_{k} is a vertex of all but a finite number of the trees F_{i}, i ∈ I, there is an infinite set I′ ⊆ I_{k} such that v_{k}φ_{i} is defined for all i ∈ I′. Since T is regular, we can select an infinite set I_{k+1} ⊆ I′ such that the trees T_{v_{k}φ_{i}}, i ∈ I_{k+1} are all isomorphic and the edges uφ_{i} ⟶ v_{k}φ_{i}, i ∈ I_{k+1} have the same label. Let i_{0} ∈ I_{k+1}. The vertices v_{0}φ_{i_{0}}, …, v_{k}φ_{i_{0}} are all distinct because φ_{i_{0}} is injective. Since T_{uφ} is isomorphic to T_{uφ_{i_{0}}} and for each j = 0, …, k − 1, T_{v_{j}φ} is isomorphic to T_{v_{j}φ_{i_{0}}}, and the edges uφ ⟶ v_{j}φ and uφ_{i_{0}} ⟶ v_{j}φ_{i_{0}} have the same label, there exists a successor v′ of uφ such that v′ ∉ {v_{0}φ, …, v_{k−1}φ}, T_{v′} is isomorphic to T_{v_{k}φ_{0}} and uφ ⟶ v′ and uφ_{i_{0}} ⟶ v_{k}φ_{i_{0}} are labeled by the same letter. Define v_{k}φ = v′. □

Let I(A) denote the collection of all ω-ideals of injective simulation equivalence classes of finite (Σ, A)-labeled trees, i.e., sets of the form

(U] = {F ∈ (Σ, A)ISF : ∃T ∈ U F ≤ T },

where U is any countable directed set of finite trees in (Σ, A)ISF. In fact, it is easy to see that a set is in I(A) iff it is a countable ideal which is also a directed set with respect to the injective simulation order. Given σ ∈ Σ_{m} and I_{1} = (U_{1}], …, I_{m} = (U_{m}], we define

σ(I_{1}, …, I_{m}) = ({σ(F_{1}, …, F_{m}) : F_{i} ∈ U_{i}}].

Moreover, we define 0 = {0} = ({0}] and

I_{1} + I_{2} = ({F_{1} + F_{2} : F_{i} ∈ U_{i}}],

for all I_{1} = (U_{1}] and I_{2} = (U_{2}] in I(A). It can be shown that the operations are well-defined and that I(A), equipped with the subset order is an ωcontinuous additive Σ-algebra.

Theorem 8.2 For each set A, there exist an ω-continuous additive Σ-algebra B and an injective order reflecting iteration Σ_{+,0}-algebra morphism (Σ, A)ISR ⟶ B.

Proof. Let B = I(A) and consider the map A ⟶ B taking each letter a into {a} = ({a}]. Since B is an ordered iteration Σ_{+,0}-algebra satisfying (1) – (6), by Theorem 7.6 this map extends to an ordered additive iteration Σ_{+,0}-algebra morphism h. We need to show that for any two regular trees S, T, if Sh ⊆ T h, then S ≤ T. But it is easy to see that Sh is the set of all finite trees ≤ S, and similarly for T. Thus, by Lemma 8.1, S ≤ T. □

9 Further results

In this section we outline some further results. Firs we consider decidability and nonfinite axiomatizability.

Suppose that t ≤ t′ is an inequation between μ-terms t, t′ over Σ_{+,0}, where Σ is a finite signature. Let T and T′ denote the corresponding regular trees in (Σ, X)R. Thus, T is the value of the function t_{(Σ,X)R} induced by T when each variable x is assigned the corresponding tree having a single edge which is labeled x. By our previous results, the inequation t ≤ t′ holds in ωcontinuous additive Σ-algebras iff T ≤ T′. This latter property is easily seen to be decidable. Thus we have

Proposition 9.1 When Σ is finite, it is decidable whether an inequation between μ-terms over Σ holds in all ω-continuous additive Σ-algebras.

Since each term is finite, the assumption on the finiteness of Σ is not important. It can be shown that the problem is in fact in NP.

We have seen that for each Σ, the variety generated by ω-continuous additive Σ-algebras can be axiomatized by an infinite number of equation schemes.

Theorem 9.2 Suppose that Σ contains a symbol of positive rank. Then the variety of ordered iteration algebras generated by the ω-continuous additive Σ-algebras cannot be axiomatized by a finite number of equation schemes.

Proof. It is sufficient to prove this fact in the case that Σ contains a single symbol, say σ, and σ has rank 1.

Let Reg_{a} denote the collection of all regular subsets of a^{∗}. We may turn Reg_{a} into an ω-continuous additive Σ-algebra by defining

L_{1} + L_{2} = L_{1} ∪ L_{2}
0 = ∅
σ(L) = aL = {au : u ∈ L}

and

L_{1} ≤ L_{2} ⇔ L_{1} ⊆ L_{2},

for all L_{1}, L_{2} ∈ Reg_{a}.

The result now follows from two observations. First, it is proved in [2, 16] that the variety of ordered iteration algebras generated by Reg_{a} cannot be defined by a finite number of equation schemes. (Actually, this is proved in [2, 16] in an equivalent form using the regular operations of set union, concatenation and Kleene star.) Second, it follows from results proved in [34, 19, 16] that the valid inequations of Reg_{a} can be axiomatized, relatively to the equations of ω-continuous Σ-algebras, by a finite number of equation schemes. □

When Σ is an arbitrary signature, define

σ(L_{1}, …, L_{n}) = \{ \begin{matrix}aL_{1} & if n > 0 \\ ∅ & otherwise, \end{matrix}

for all σ ∈ Σ_{n}, n ≥ 0, and L_{1}, …, L_{n} ∈ Reg_{a}. The same argument shows that when Σ ≠ Σ_{0}, no variety of ordered iteration Σ_{+,0}-algebras containing the algebra Reg_{a} has an axiomatization by a finite number of equation schemes.

It is natural to ask how our results change when the operations induced by the letters in Σ are commutative, so that all equations

σ(x_{1}, …, x_{n}) = σ(x_{1π}, …, x_{nπ})  (20)

hold, where σ ∈ Σ_{n} and π is any permutation [n] ⟶ [n]. It can be seen that the variety of ordered preiteration Σ_{+,0}-algebras generated by the ωcontinuous additive Σ-algebras stisfying equations (20) can be axiomatized by the inequations that hold in ω-continuous additive Σ-algebras and the equations (20). The free algebras in this variety can be described by injective simulations of the variant of (regular) synchronization trees where each hyperedge has an unordered n-tuple as its target.

References

[1] L. Aceto, W.J. Fokkink and A. Ingólfsdóttir, A menagerie of nonfinitely based process semantics over BPA*: from ready simulation to completed traces, Math. Struct. Comput. Sci., 8(1998), 193-230.

[2] L. Aceto, W.J. Fokkink and A. Ingólfsdóttir, On a question of A. Salomaa: The equational theory of regular expressions over a singleton alphabet is not finitely based, Theoret. Comput. Sci., 209(1998), 163-178.

[3] J.W. De Bakker and D. Scott, A theory of programs, IBM Seminar, Vienna, 1969.

[4] J. Balcazar, J. Gabarro and M. Santha, Deciding bisimilarity is Pcomplete, Formal Aspects of Computing, 4(1992), 638–648.

[5] M. Barr and Ch. Wells, Category Theory for Computing Science, Prentice-Hall International Series in Computer Science. Prentice-Hall International, New York, 1990.

[6] H. Bekić, Definable operations in general algebras, and the theory of automata and flowcharts, Technical Report, IBM Laboratory, Vienna, 1969.

[7] D. Benson and J. Tiuryn, Fixed points in free process algebras, Theoret. Comput. Sci., 63(1989), 275–294.

[8] S.L. Bloom, Varieties of ordered algebras, J. Comput. System Sci., 13(1976), 200–212.

[9] S.L. Bloom and Z. Ésik, Iteration Theories, Springer–Verlag, 1993.

[10] S.L. Bloom, Z. Ésik and D. Taubner, Iteration theories of synchronization trees, Information and Computation, 102(1993), 1–55.

[11] S.L. Bloom and Z. Ésik, The equational logic of fixed points, Theoret. Comput. Sci., 179(1997), 1–60.

[12] J.H. Conway, Regular Algebra and Finite Machines, Chapman and Hall, London, 1971.

[13] F. Corradini, R. De Nicola and A. Labella, Tree morphisms and bisimulations, in: Proc. MFCS’98 Workshop on Concurrency, ENTCS, 18(1998).

[14] F. Corradini, R. De Nicola and A. Labella, A finite axiomatization of nondeterministic regular expressions, Theoret. Inform. Appl., 33(1999), 447–465.

[15] F. Corradini, R. De Nicola and A. Labella, Models of nondeterministic regular expressions. J. Comput. Sys. Sci., 59(1999), 412–449.

[16] S. Crvenković, I. Dolinka, Z. Ésik, A note on equations for commutative regular languages, Inform. Process. Lett., 70(1999), 265–267.

[17] Z. Ésik, Completeness of Park induction, Theoret. Comput. Sci., 177(1997), 217–283.

[18] Z. Ésik and A. Labella, Equational properties of iteration in algebraically complete categories. Mathematical foundations of computer science (Cracow, 1996). Theoret. Comput. Sci., 195(1998), 61–89.

[19] Z. Ésik, Group axioms for iteration, Inform. and Comput., 148(1999), 131–180.

[20] Z. Ésik, Axiomatizing the least fixed point operation and binary supremum, in: proc. CSL 2000, LNCS 1862, Springer–Verlag, 2000, 302–316.

[21] W. Fokkink and H. Zantema, Basic process algebra with iteration: Completeness of its equational axioms. Computer Journal, 37(1994), 259– 267.

[22] J. Goguen, J. Thatcher, E. Wagner, and J. Wright, Initial algebra semantics and continuous algebras, J. ACM, 24(1977), 68–95.

[23] G. Gratzer, Universal Algebra. Second edition, Springer-Verlag, New York-Heidelberg, 1979.

[24] I. Guessarian, Algebraic Semantics, LNCS 99, Springer–Verlag, 1981.

[25] P.C. Kanellakis and S.A. Smolka, CCS expressions, finite state processes and three problems of equivalence, Inform. and Comput., 86(1990), 43– 68.

[26] D. Kozen, A completeness theorem for Kleene algebras and the algebra of regular events, Inform. and Comput., 110(1994), 366–390.

[27] D. Krob, Monoides et semi-anneaux complets, Semigroup Forum, 36(1987), 323–339,

[28] D. Krob, Complete systems of B-rational identities, Theoret. Comput. Sci., 89(1991), 207–343.

[29] E.G. Manes and M.A. Arbib, Algebraic Approaches to Program Semantics, Springer-Verlag, 1986.

[30] R. Milner, A complete inference system for a class of regular behaviours, J. Comput. Syst. Sci., 28(1984), 439–466.

[31] R. Milner, Communication and Concurrency, Prentice-Hall, 1989.

[32] D.M.R. Park, Fixpoint induction and proofs of program properties, in: Machine Intelligence 5, D. Michie and B. Meltzer, Eds., Edinburgh Univ. Press, 1970, 59–78.

[33] D.M.R. Park, Concurrency and automata on infinite sequences, in: Proc. GI Conference, P. Deussen, Ed., LNCS 104, Springer–Verlag, 1981, 167–183.

[34] V.N. Redko, On algebra of commutative events, Ukrainian Math. J., 16(1964), 185–195 (in Russian).

[35] A. Salomaa, Two complete axiom systems for the algebra of regular events. J. Assoc. Comput. Mach., 13(1966), 158–169.

[36] P. Sewell, Nonaxiomatisability of equivalences over finite state processes, Ann. Pure Appl. Logic, 90(1997), 163–191.

Recent BRICS Report Series Publications

RS-00-25 Zoltán Ésik. Continuous Additive Algebras and Injective Simulations of Synchronization Trees. September 2000. 41 pp.

RS-00-24 Claus Brabrand and Michael I. Schwartzbach. Growing Languages with Metamorphic Syntax Macros. September 2000.

RS-00-23 Luca Aceto, Anna Ingólfsdóttir, Mikkel Lykke Pedersen, and Jan Poulsen. Characteristic Formulae for Timed Automata. September 2000. 23 pp.

RS-00-22 Thomas S. Hune and Anders B. Sandholm. Using Automata in Control Synthesis — A Case Study. September 2000. 20 pp. Appears in Maibaum, editor, Fundamental Approaches to Software Engineering: First International Conference, FASE ’00 Proceedings, LNCS 1783, 2000, pages 349–362.

RS-00-21 M. Oliver Möller and Rajeev Alur. Heuristics for Hierarchical Partitioning with Application to Model Checking. August 2000. 30 pp.

RS-00-20 Luca Aceto, Willem Jan Fokkink, and Anna Ingólfsdóttir. 2-Nested Simulation is not Finitely Equationally Axiomatizable. August 2000. 13 pp.

RS-00-19 Vinodchandran N. Variyam. A Note on NP ∩ coNP/poly. August 2000. 7 pp.

RS-00-18 Federico Crazzolara and Glynn Winskel. Language, Semantics, and Methods for Cryptographic Protocols. August 2000. ii+42 pp.

RS-00-17 Thomas S. Hune. Modeling a Language for Embedded Systems in Timed Automata. August 2000. 26 pp. Earlier version entitled Modelling a Real-Time Language appeared in Gnesi and Latella, editors, Fourth International ERCIM Workshop on Formal Methods for Industrial Critical Systems, FMICS ’99 Proceedings of the FLoC Workshop, 1999, pages 259–282.

RS-00-16 Jiří Srba. Complexity of Weak Bisimilarity and Regularity for BPA and BPP. June 2000. 20 pp. To appear in Aceto and Victor, editors, Expressiveness in Concurrency: Fifth International Workshop EXPRESS ’00 Proceedings, ENTCS, 2000.