BRICS RS-02-19 Bloom & Ésik: An Extension Theorem with an Application to Formal Tree Series BRICS

Basic Research in Computer Science

An Extension Theorem with an Application to Formal Tree Series

Stephen L. Bloom Zoltán Ésik BRICS Report Series RS-02-19 ISSN 0909-0878 April 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/19/

An extension theorem with an application to formal tree series

Stephen L. Bloom^{∗}

Department of Computer Science

Stevens Institute of Technology

Hoboken, NJ 07030

Zoltán Ésik^{†}

Institute for Informatics

University of Szeged

Szeged, Hungary

Abstract

A grove theory is a Lawvere algebraic theory T for which each hom-set T (n, p) is a commutative monoid; composition on the right distrbutes over all finite sums: (∑_{i∈F} f_{i})·h = ∑_{i∈F} f_{i} ·h. A matrix theory is a grove theory in which composition on the left and right distributes over finite sums. A matrix theory M is isomorphic to a theory of all matrices over the semiring S = M(1, 1). Examples of grove theories are theories of (bisimulation equivalence classes of) synchronization trees, and theories of formal tree series over a semiring S. Our main theorem states that if T is a grove theory which has a matrix subtheory M which is an iteration theory, then, under certain conditions, the fixed point operation on M can be extended in exactly one way to a fixedpoint operation on T such that T is an iteration theory. A second theorem is a Kleene-type result. Assume that T is a iteration grove theory and M is a sub iteration grove theory of T which is a matrix theory. For a given collection Σ of scalar morphisms in T we describe the smallest sub iteration grove theory of T containing all the morphisms in M ∪ Σ.

∗Partially supported by NSF grant 0119916.

†Partially supported by NSF grant 0119916 and BRICS.

1 Introduction

In many areas of theoretical and applied computer science, one is interested in solving systems of fixed point equations:

x_{1} = t_{1}(x_{1}, …, x_{n}, y_{1}, … y_{p})
⋮  (1)
x_{n} = t_{n}(x_{1}, …, x_{n}, y_{1}, … y_{p}).

where, for each i ∈ [n], t_{i} is a function t_{i} : A^{n+p} → A, for some structure A. The structure may be a poset of some kind, and the functions may be order-preserving or continuous. Of course, there are other possible settings in which fixed points are of interest: one is when t_{i} is a row matrix with n+p entries in some semiring, S. One example from language theory is when S is the idempotent semiring of all subsets of a free monoid Σ^{∗}, with union as sum and complex concatenation as product. Another, is when t_{i} is a pair (a, v), consisting of a 1 by n + p row matrix over a semiring S, and an element v in an S-module. Continuing the language example, with the same semiring, the power set of Σ^{∗}, the module might be the collection of all subsets of infinite words on Σ. Another setting is when t_{i} is a functor D^{n+p} → D, where D is some category.

Depending on the context, some questions about such systems are

• Does the system have any solution?

• Is there a canonical (least, initial, etc.) solution?

• Is there a unique solution?

• If there are solutions, what do all solutions look like?

• What are the properties of solutions?

We take as our framework for discussing fixed point equations the (onesorted) categories known as Lawvere algebraic theories [30], categories whose objects are nonnegative integers, and n+p is the coproduct of n, p. In the case that the t_{i} denote order preserving functions A^{n+p} → A^{n} on a poset A, a function A^{p} → A^{n} is a morphism n → p (note the reversal of direction to translate from products to coproducts). In the matrix example, an n×p matrix over S becomes a morphism n → p.

Now, in an algebraic theory, we interpret the entire right side of the system of fixed point equations (1) as a morphism t : n → n + p, since each t_{i} determines a morphism 1 → n + p and the coproduct property produces a corresponding morphism t = ⟨t_{1}, …, t_{n}⟩ : n → n + p. Thus, a solution of the system is itself a morphism ξ : n → p which satisfies the “fixed point equation”

ξ = t · ⟨ξ, 1_{p}⟩.

If we write a solution ξ as ⟨ξ_{1}, …, ξ_{n}⟩, then, for a theory of functions on powers of a set A, each ξ_{i} is a function A^{n+p} → A and

ξ_{1}(y) = t_{1}(ξ_{1}(y), ξ_{2}(y), …, ξ_{n}(y), y)
⋮
ξ_{n}(y) = t_{n}(ξ_{1}(y), ξ_{2}(y), …, ξ_{n}(y), y),

where we write y for y_{1}, …, y_{p}.

Algebraic theories T in which every system of fixed point equations has a canonical solution are modeled as theories enriched by a function ^{†} : T (n, n + p) → T (n, p), for each n, p ≥ 0, such that, for each morphism t : n → n + p,

t^{†} = t · ⟨t^{†}, 1_{p}⟩.

Thus, the operation t ↦ t^{†} produces a canonical solution to the system determined by the morphism t.

There has been a good deal of effort by both mathematicians and computer scientists devoted to the question of whether fixed points to certain systems exist at all. The names Brouwer [13], Banach [1], Tarski [41], Kleene [23], and Scott [37] come to mind. The properties of the fixed point operation in theories which occur naturally in the theory of computation have been studied, mainly in the setting of language theory ([23, 35, 36, 14, 26]). One example of an equational property (other than the fixed point property itself) of the fixed point operation is the “composition identity”:

(f · ⟨g, 0_{n} ⊕ 1_{p}⟩)^{†} = f · ⟨(g · ⟨f, 0_{m} ⊕ 1_{p}⟩)^{†}, 1_{p}⟩,

all f : n → m + p, g : m → n + p. As a result of a long series of papers, there seems to be agreement that there is essentially one equational theory which captures all of the equations valid in every computationally interesting theory. These equations may be described in any of several equivalent ways:

• all equations valid in theories of complete partially ordered sets and continuous functions;

• all equations valid in theories of continuous functors on ω- complete categories;

• all equations valid in theories of labelled trees;

• all models of a certain set of axioms.

The models for these equations are called iteration theories. The reason for the qualification “essentially one” above is that certain iteration theories, such as a theory of matrices over the semiring of binary relations on some set, are special only in that they have a unique morphism 1 → 0. Thus, in addition to the axioms mentioned, they also satisfy x = y, all x, y : 1 → 0.

The best set of axioms known for iteration theories is due to Esik, [22]. His axioms are divided into two parts: the “Conway identities”, which contain only two axiom schemes, the parameter and double dagger identities, in addition to the composition identity above, and an identity for each finite (simple) group. Each of the axioms is readily seen to hold in any particular setting. However, the completeness of these axioms is not at all obvious.

The parameter identity is

(f · (1_{n} ⊕ g))^{†} = f^{†} · g,

for all f : n → n + p, g : p → q. The double dagger identity is

f^{††} = (f · (⟨1_{n}, 1_{n}⟩ ⊕ 1_{p}))^{†},

all f : n → n+n+p. (A brief account of theories and the axiomatization iteration theories is given in the appendix.)

There is a class of iteration theories in which the “nontrivial” systems of fixed point equations have unique solutions: these theories were introduced by Elgot in [19] under the term “(ideal) iterative theories”. In such a theory, a morphism 1 → n either is one of the coproduct injections i_{n} : 1 → n, i ∈ [n], or is ideal; if f : 1 → n is ideal, so is f · g, for any g : n → p. A morphism f : n → p is ideal if each component i_{n} · f is. For each ideal morphism f : n → n + p in an iterative theory, there is a unique ξ = f^{†} such that

ξ = f · ⟨ξ, 1_{p}⟩.  (2)

One class of examples of ideal iterative theories are the “contraction theories”. If A is a complete metric space, the least theory containing all proper contractions A^{n} → A is an iterative theory.

One might legitimately consider fixed point equations for ideal morphisms as equations in which the variables to solve for occur only in “guarded positions”. Thus, iterative theories might be described roughly as theories in which systems of guarded equations have unique fixed points. In iterative theories, the nonideal morphisms are somehow trivial, and can be dealt with as in [5, 6]. Models in which “guarded statements” of the required form have unique fixed points have been featured in many places, for example in the metric semantics of de Bakker and his collaborators, see, e.g., [16, 17, 18], in the work of Milner, e.g., [32], and in the classical paper axiomatizing the regular sets, by Salomaa, [35].

What about morphisms n → n + p in iterative theories which are not ideal? For example, consider the case n = 1, p = 0 and f = 1_{1}, the identity morphism. The corresponding fixed point equation is the trivial equation in the variable ξ : 1 → 0,

ξ = 1_{1} · ξ,

which has all morphisms 1 → 0 as solutions. In [5, 6] it is shown that for each choice of a solution to this one fixed point equation, there is a unique extension of the fixed point operation to all morphisms such that the resulting theory is an iteration theory.

The theme of extending the fixed point operation from subtheories in which the solution is unique to the entire theory - while preserving its properties - was continued in several settings: for matrix theories in [8], and for matricial theories in [9]. A matrix theory is one in which a morphism n → p is an n×p matrix over a fixed semiring. As an application of the matrix extension theorem in [8], it was shown that if the theory of matrices over the semiring S is a Conway or an iteration theory, then so is the theory of matrices over the semiring of all formal power series over S. In Section 3 we review that result.

In the current paper, we continue playing the same tune, but in a different setting. We consider what we have called “grove theories” in [7], motivated by an analogous use of the term in [3]. The detailed statement of our main theorem will be given in Section 5 below.

An example of a grove theory involves a different kind of tree: the synchronization trees. In Section 6, we use the extension theorem to show that the theory of synchronization trees is an iteration theory. It then follows that synchronization trees modulo bisimulation equivalence and other behavioral equivalences form iteration theories. This result is known, but our original argument made use of 2-categories and continuity arguments, see [7].

In Section 7, we discuss a new example in more detail, the theory of formal tree series [4, 29] over a semiring. We first formulate this theory and then use the grove extension theorem to show that if the semiring S is a Conway or iteration semiring, then for each signature Σ, so is the theory of formal Σ-trees over S.

2 Preliminaries

We denote the set {1, 2…. , n} by [n]. The composite of morphisms f : A → B and g : B → C is written in diagrammatic order:

f · g = A [figure: f] B [figure: g] C.

We give a review of Lawvere algebraic theories and various tree theories in the Appendix. In particular, the axioms for Conway and iteration theories are presented there.

3 The Matrix Extension Theorem

A matrix theory T is a pointed theory, i.e., a theory with a distinguished morphism 0_{1,0} : 1 → 0, such that each hom-set T (n, p) is a

commutative monoid, with neutral element 0_{n,p} = \overbrace{⟨0_{1,0}, …, 0_{1,0}⟩}^{n} ·0_{p} such that

(f + g) · h = f · h + g · h
k · (f + g) = k · f + k · g,
0_{r,n} · f = 0_{r,p}
f · 0_{p,q} = 0_{n,q}

for all f, g : n → p, h : p → q and k : r → n in T. A morphism T → T′ of matrix theories is a theory morphism which preserves the monoid structure on each hom-set.

In [20] it is shown that if T is a matrix theory, then T is isomorphic to a theory of matrices Mat_{S} over the semiring S = T (1, 1). A morphism n → p in Mat_{S} is an n×p matrix over S. Composition of morphisms is matrix multiplication, and the additive structure is defined in the expected way.

In matrix theories which are preiteration theories, one may define a “star” operation on the square matrices by

a^{∗} := [a, 1_{n}]^{†},

where a is n → n. Using this operation, the Conway identities take the form of familiar identities for regular expressions, which is the reason for the terminology. The double dagger identity becomes the “star sum” identity:

(a + b)^{∗} = (a^{∗}b)^{∗}a^{∗},  (3)

where a, b : n → n, and the composition identity becomes the “product star” identity:

(ab)^{∗} = 1_{n} + a(ba)^{∗}b,  (4)

where a : n → m and b : m → n. The parameter identity holds automatically. See [14] and [8]. Also, in any Conway matrix theory, the dagger operation is related to the star operation by:

[a, b]^{†} = a^{∗}b,

when a : n → n and b : n → p. A Conway, respectively iteration matrix theory is a matrix theory which is a Conway theory, respectively, an iteration theory. A morphism of Conway (or iteration) matrix theories is both a matrix theory morphism and a Conway theory morphism.

If S is a semiring such that Mat_{S} is a Conway or iteration theory, then we call S a Conway, or an iteration semiring. The collection of all Conway (or iteration) semirings forms a variety of algebras whose signature is that of semirings enriched with a unary star operation. See [7].

In [8], the following “extension theorem” was proved. Suppose that S is a subsemiring of the semiring R. Suppose further that there is an ideal I of R such that R is the direct sum of S and I, in that any element x of R can be written uniquely as x = s + a, where s ∈ S and a ∈ I.

Theorem 3.1 (Matrix Extension Theorem) If Mat_{S} is an Conway (resp. iteration) theory, and if for each a ∈ I, b ∈ R there is a unique ξ ∈ R such that ξ = aξ + b in R, then, there is a unique extension of the dagger operation on Mat_{S} to Mat_{R} so that Mat_{R} becomes a Conway (resp. iteration) theory.

It follows from this result that if the theory of matrices over the semiring S is a Conway or iteration theory, then so is the theory of matrices over the semiring of formal power series over S with variables in the set X.

Indeed, a formal power series r over the semiring S with variables in X is a function r : X^{∗} → S. In this case, the semiring S is isomorphic to the collection of functions r : X^{∗} → S such that r(u) = 0 for all nonempty words u ∈ X^{∗}, and the ideal I is the collection of all functions a : X^{∗} → S with a(λ) = 0, where λ is the word of length zero.

4 Grove theories

A grove theory T is a pointed theory such that each hom-set T (n, p) = (T (n, p), +, 0_{n,p}) is a commutative monoid with neutral element 0_{n,p} such that

(f + g) · h = f · h + g · h
0_{r,n} · f = 0_{r,p}
i_{n} · (f + g) = i_{n} · f + i_{n} · g, i ∈ [n]
i_{n} · 0_{n,p} = 0_{1,p}, i ∈ [n],

for all f, g : n → p, h : p → q in T. (The last two equations say that sums of vector morphisms are defined componentwise, as are the neutral elements.) If T, T′ are grove theories, a morphism φ : T → T′ is a theory morphism that is a monoid morphism T (n, p) → T′(n, p), for each n, p ≥ 0. T is a sub grove theory of T′ if T is a subtheory of T′, and the monoid T (n, p) is a submonoid of T′(n, p), for each n, p ≥ 0.

Each matrix theory is a grove theory, but not conversely.

In any grove theory, for a nonnegative integer n, define the morphism n : 1 → 1 as

n := \overbrace{1_{1} + … + 1_{1}}^{n} .

The following fact is easy to prove by induction.

Proposition 4.1 In any grove theory T, and any nonnegative integer n,

n · (f + g) = n · f + n · g
n · 0_{1,p} = 0_{1,p},

all f, g : 1 → p in T.

Suppose that T is a grove theory and T_{0} is a subtheory of T. We say that T_{0} is additively closed if T_{0}(n, p) is a submonoid of T (n, p), for each n, p ≥ 0.

Corollary 4.2 The matrix theory Mat_{N} of matrices over the semiring of nonnegative integers is initial in the class of grove theories and matrix theories.

A Conway or iteration grove theory is a grove theory which is also a Conway or iteration theory. Thus, any Conway or iteration matrix theory is a Conway or iteration grove theory. A morphism of Conway or iteration grove theories is a grove theory morphism which is also a Conway or iteration theory morphism.

We let N_{∞} denote the semiring consisting of the nonnegative integers with an “infinite” element adjoined; the addition and multiplication are defined in the expected way. This semiring is a Conway and iteration semiring when the star operation is defined by

x^{∗} := \begin{cases}1 & x = 0 \\ ∞ & otherwise. \end{cases}

The corresponding matrix theory is a Conway and iteration theory. In Mat_{N_{∞}}, the equation 1^{∗} = 2^{∗} holds; in the dagger version,

(1_{2} + 2_{2})^{†} = (2 · 1_{2} + 2_{2})^{†}.  (5)

Proposition 4.3 The matrix theory Mat_{N_{∞}} is initial in the class of Conway and iteration grove theories satisfying (5) It is also initial in the class of Conway and grove matrix theories satisfying this equation.

We now turn to the statement of the main result.

5 The grove extension theorem

The hypotheses take a while to state, but they are similar to those needed for the matrix extension theorem. First we need a definition.

Definition 5.1 Suppose that T is a grove theory and M is a sub grove theory of T which is a matrix theory. A collection T_{0} of morphisms of T is an M-ideal if T_{0}

• contains all zero morphisms 0_{n,p};

• is closed under addition, i.e., if f, g : n → p ∈ T_{0}, then f + g ∈ T_{0};

• is closed under right composition with any T -morphism, i.e., if f : n → p is T_{0} and g : p → q is any morphism, then f · g : n → q is in T_{0};

• is closed under left-composition with any M-morphism.

5.1 The hypotheses

Assume that T is a grove theory and M is a sub grove theory of T that is a matrix theory. Further, we assume that

H1. T_{0} is an M-ideal of T.

H2. Every f : n → p in T can be written uniquely as

f = a + f_{0}

for some a ∈ M, f_{0} ∈ T_{0}. We say: T is the direct sum of M and T_{0}.

H3. If a ∈ M and f, g ∈ T have appropriate sources and targets, then

a · (f + g) = a · f + a · g.

H4. M is a Conway theory, so that there is a ^{∗}-operation on the square matrices satisfying

(ab)^{∗} = 1_{n} + a(ba)^{∗}b, a : n → m, b : m → n
(a + b)^{∗} = (a^{∗}b)^{∗}a^{∗}, a, b : n → n.

In particular, S = M(1, 1) is a Conway semiring.

H5. For every f_{0} : n → n+p in T_{0} and b : n → p in M, there is a unique solution to the equation

ξ = ((0_{n} ⊕ b) + f_{0}) · ⟨ξ, 1_{p}⟩,

and the solution is written

((0_{n} ⊕ b) + f_{0})^{∇}.

Theorem 5.2 (The grove extension theorem) Under the above hypotheses, there is a unique way to define a dagger operation

\xymatrix{^{†} : T (n, n + p) \ar[r] & T (n, p),}

on each hom-set T (n, n + p) extending that on M such that T becomes a Conway theory. Further, if M satisfies the weak functorial implication, so does T; if M is an iteration theory, so is T.

The proof of this theorem is in Section 8. The “weak functorial implication” is defined in the Appendix.

We can revise the assumptions needed for the grove extension theorem to apply only to “scalar morphisms”, i.e., those with source 1.

Proposition 5.3 Suppose that T is a grove theory and S ⊆ T (1, 1) is a Conway semiring. Then M = Mat_{S} is a sub grove theory of T which is a Conway theory. Suppose that I_{0} is a collection of scalar morphisms of T with the following properties:

1. s ∈ S, f : 1 → p ∈ I_{0}, g : p → q ∈ T ⟹ s · f · g ∈ I_{0}.

2. f, g : 1 → p ∈ I_{0} ⟹ f + g ∈ I_{0}.

3. 0_{1,p} ∈ I_{0}, all p ≥ 0.

4. For any g : 1 → p in T there is a unique a : 1 → p ∈ M and f : 1 → p ∈ I_{0} such that g = f + a.

5. For any f, g : 1 → p ∈ T and any s ∈ S, s · (f + g) = s · f + s · g.

6. For any b : 1 → p ∈ M and any f : 1 → 1 + p in I_{0}, there is a unique ξ : 1 → p ∈ T such that

ξ = ((0_{1} ⊕ b) + f) · ⟨ξ, 1_{p}⟩.

Then there is a unique way to define a dagger operation

\xymatrix{^{†} : T (n, n + p) \ar[r] & T (n, p),}

on each hom-set T (n, n + p) extending that on M such that T becomes a Conway theory. Further, if M satisfies the weak functorial implication, so does T; if M is an iteration theory, so is T.

Proof. We define T_{0}(n, p) as the collection of all morphisms f = ⟨f_{1}, …, f_{n}⟩ such that f_{i} ∈ I_{0}, for each i ∈ [n]. Then, the only point which may not be clear is that for b : n → p in Mat_{S}, and f : n → n + p in T_{0}, there is a unique solution to the Elgot fixed point equation for (0_{n} ⊕ b) + f. But this fact follows from the inductive argument in [11], which shows that “scalar iterative theories” are also iterative theories. This shows that the hypotheses of the grove extension theorem hold.

□

We now discuss two applications of the theorem.

6 The theory of synchronization trees

Let A be a nonempty set. The theory ST (A) of synchronization trees over A has been studied in [7]. We recall that a morphism 1 → p in this theory is a tree t = (V, v_{0}, E, ℓ), where

1. V is a finite or countable set;

2. (V, v_{0}, E) is a rooted tree - i.e., E ⊆ V ×V, v_{0} ∈ V and, for each v ∈ V there is a unique path v_{0}, v_{1}, …, v_{k} = v from v_{0} to v.

3. ℓ : E → A ∪ [p] is a “labeling function”.

4. if ℓ(u, v) ∈ [p], then v is a leaf, and (u, v) is an “exit edge”.

A morphism s : p → q is a p-tuple of trees 1 → q. If t : 1 → p and s = (s_{1}, …, s_{p}) are synchronization trees, the composite t · s is the tree obtained from t by deleting any exit edge (u, v) labeled i ∈ [p] and making u the root of a copy of the tree s_{i}; if t, s : 1 → p are synchronization trees, t+s : 1 → p is the tree obtained from the disjoint union of the two sets of vertices and edges by identifying the roots of s, t and otherwise making no further identifications. Composition and sum is extended to n-tuples of trees pointwise. (See [7] for all details.)

The tree 0_{1,p} : 1 → p is the unique tree with only one vertex, the root, and no edges. The morphism 0_{n,p} is the n-tuple of the trees 0_{1,p}.

In [7], it was shown that ST (A) is a grove theory.

Proposition 6.1 Each collection of trees n → p in ST (A) is a complete metric space, where the distance between two trees n → p is the maximum of the distances between their components i_{n}·t, i_{n}·t′. For trees t, t′ : 1 → p, define the distance d(t, t′) to be 0 if t = t′, or 1/2^{n}, where n is the minimum depth for which the trees t|n and t′|n are distinct. The tree t|n is t “cut off” at level n; prune all vertices and edges at distance more than n from the root.

Let Ex be the subtheory of ST (A) determined by the trees 1 → p all of whose edges are exit edges; thus, for each i in [p], there are either finitely many exit edges labeled i or countably many such edges. Let N_{∞} denote the semiring of the nonnegative integers with a point at infinity adjoined.

For any synchronization tree t : 1 → p in Ex, let m_{i} denote the number of edges in the tree labeled i whose source is the root, for i ∈ [p]. We may thus identify such a tree t with the 1×p matrix m(t) = [m_{1}, …, m_{p}] over N_{∞}. This identification respects both the theory sum and composition operations, as is easy to show. Thus, Ex is isomorphic to the theory of all matrices over the semiring N_{∞}, Mat_{N_{∞}}.

Now let T_{0} be the collection of all morphisms f = ⟨f_{1}, …, f_{n}⟩ : n → p in ST (A) such that each component f_{i} is a tree with the following property. No edge whose source is the root is labeled by an integer in [p]. These trees have been called “guarded” in [7].

It is straightforward to check that the hypotheses listed in Proposition 5.3 hold. In particular, if f : n → n + p is in T_{0} and b : n → p is in Ex, then there is a unique tree which is a solution of the iteration equation for (0_{n} ⊕ b) + f : n → n + p, namely the equation

ξ = ((0_{n} ⊕ b) + f) · ⟨ξ, 1_{p}⟩.

Indeed, the tree 0_{n} ⊕ b + f induces a proper contraction map C on the set of trees t : n → p in ST (A), where

C(t) := ((0_{n} ⊕ b) + f) · ⟨t, 1_{p}⟩.

The distance between C(t) and C(t′) is at most 1/2 the distance between t and t′. Thus, by the Banach fixed point theorem [1], C has a unique fixed point.

Thus, as a corollary to the grove extension theorem, we obtain

Theorem 6.2 There is a unique way to define ^{†} on ST (A) extending the corresponding operation on Ex, so that ST (A) is a Conway theory. And since Ex is in fact an iteration theory, so is ST (A). Moreover, the weak functorial implication holds in ST (A).

The fact that ST (A) is an iteration theory was proved in a totally different way in [7], using 2-categorical notions, initiality and continuity arguments.

7 Theories of formal tree series

Recall that T_{Σ}(X_{n}) denotes the set of finite Σ-trees whose leaves are labeled by letters in X_{n} ∪ Σ_{0} and whose interior nodes with k successors are labeled by letters in Σ_{k}. The height, ht(t), of a tree t in T_{Σ}(X_{n}) is defined as usual.

Assume S is a commutative semiring.

Definition 7.1 A formal Σ-tree series s : 1 → p over S is a function

s : T_{Σ}(X_{p}) [figure] S.

We let S⟨⟨ Σ^{p} ⟩⟩ denote the set of all formal Σ-tree series 1 → p over S. We write the value of s ∈ S⟨⟨ Σ^{p} ⟩⟩ on the tree t as (s, t). The support of s is {t ∈ T_{Σ}(X_{p}) : (s, t) ≠ 0}.

The following fact is well-known.

Proposition 7.2 The set S⟨⟨ Σ^{p} ⟩⟩ is a complete metric space, where for s, s′ ∈ S⟨⟨ Σ^{p} ⟩⟩, the distance function is defined as follows.

d(s, s′) := \begin{cases}0 & s = s′ \\ 1/2^{n} & n = min\{ht(t) : (s, t) ≠ (s′, t)\}. \end{cases}

Each set S⟨⟨ Σ^{p} ⟩⟩ may be enriched with a commutative addition operation, defined by:

(s_{1} + s_{2}, t) := (s_{1}, t) + (s_{2}, t), t ∈ T_{Σ}(X_{p}).

Proposition 7.3 (S⟨⟨ Σ^{p} ⟩⟩, +, 0_{p}) is a commutative monoid, where 0_{p} is the constant function with value 0 ∈ S. □

Definition 7.4 For any tree t ∈ T_{Σ}(X_{p}), let η(t) ∈ S⟨⟨ Σ^{p} ⟩⟩ be the series defined by:

(η(t), u) := \begin{cases}1 & u = t \\ 0 & otherwise. \end{cases}

We will need the following construction below.

Definition 7.5 Suppose that t ∈ T_{Σ}(X_{n}) has exactly k leaves labeled by variables in X_{n}. (There may be other leaves labeled by letters in Σ_{0}.) Say these leaves are labeled, from left to right, by x_{i_{1}}, …, x_{i_{k}}. Let t′ in T_{Σ}(X_{k}) be the tree obtained from t by relabeling these leaves x_{1}, …, x_{k}, respectively, and let f denote both the function f : [k] → [n] which maps j ∈ [k] to i_{j} ∈ [n], (and the corresponding base morphism k → n). Then

t = 1 [figure: t′] k [figure: f] n.

When k = 0, t′ is the same tree as t, and f = 0_{n}.

Definition 7.6 For any tree u ∈ T_{Σ}(X_{p}), let D_{n}(u) denote the set of all trees t ∈ T_{Σ}(X_{n}) such that

u = t′ · ⟨u_{1}, …, u_{k}⟩

for some trees u_{1}, …, u_{k} ∈ T_{Σ}(X_{p}), where t′ is constructed from t as in Definition 7.5.

We note that D_{n}(u) is a finite set, which is nonempty when n > 0. In particular, for i ∈ [p],

D_{n}(x_{i}) = {x_{1}, …, x_{n}},  (6)

since if x_{i} = t′ · ⟨u_{1}, …, u_{k}⟩, we have k = 1, t′ = x_{1} and u_{1} = x_{i}. Thus, if t = x_{j}, f(1) = j. Further, for a fixed u ∈ T_{Σ}(X_{p}) and t ∈ D_{n}(u), there is a unique set of trees u_{1}, …, u_{k} such that u = t′ · ⟨u_{1}, …, u_{k}⟩.

We define next the theory S⟨⟨ Σ ⟩⟩ of formal Σ-tree series over S.

Definition 7.7 A morphism 1 → p in S⟨⟨ Σ ⟩⟩ is a function in S⟨⟨ Σ^{p} ⟩⟩; a morphism n → p is an n-tuple ⟨s_{1}, …, s_{n}⟩ of morphisms 1 → p. For s ∈ S⟨⟨ Σ^{n} ⟩⟩, s_{i} ∈ S⟨⟨ Σ^{p} ⟩⟩, i ∈ [n], and u ∈ T_{Σ}(X_{p}), we define

(s · ⟨s_{1}, …, s_{n}⟩, u) := ∑_{t∈D_{n}(u)}(s, t) · (s_{f(1)}, u_{1}) ⋯ (s_{f(k)}, u_{k}), (7)

where t = t′ · f, as in Definition 7.5, and D_{n}(u) is defined in Definition 7.6, and u, t′, u_{1}, …, u_{k} are related as in that Definition. The composite of ⟨s_{1}, …, s_{n}⟩ with r : n → q is defined by:

⟨s_{1}, …, s_{n}⟩ · r := ⟨s_{1} · r, …, s_{n} · r⟩.

For i ∈ [n], the coproduct injection i_{n} : 1 → n is the series η(x_{i}) in S⟨⟨ Σ^{n} ⟩⟩.

When the semiring is the Boolean semiring, this composition is known as the “OI” substitution, [21].

In order to make S⟨⟨ Σ ⟩⟩ into a grove theory, we extend the addition operation to all hom-sets pointwise: for morphisms s, r : n → p in S⟨⟨ Σ ⟩⟩, with s = ⟨s_{1}, …, s_{n}⟩ and r = ⟨r_{1}, …, r_{n}⟩, we define

s + r := ⟨s_{1} + r_{1}, …, s_{n} + r_{n}⟩
0_{n,p} := ⟨0_{p}, …, 0_{p}⟩.

We omit the proof that S⟨⟨ Σ ⟩⟩ is a theory, and note only

Proposition 7.8 S⟨⟨ Σ ⟩⟩ is a grove theory.

Indeed, since the sum of two n-tuples of morphisms 1 → p is defined pointwise, we need only check that S⟨⟨ Σ^{p} ⟩⟩ is a commutative monoid, and composition on the right distributes over sum. Both facts are easy to verify. □

We will use the next fact several times.

Lemma 7.9 Suppose s : 1 → n, s_{i} : 1 → p, in S⟨⟨ Σ ⟩⟩, for each i ∈ [n]. Then, for each variable x_{j} ∈ X_{p},

(s · ⟨s_{1}, …, s_{n}⟩, x_{j}) = ∑_{i∈[n]}(s, x_{i}) · (s_{i}, x_{j}).

Proof. Indeed, by (7),

(s · ⟨s_{1}, …, s_{n}⟩, x_{j}) = ∑_{t∈D_{n}(x_{j})}(s, t) · (s_{f(1)}, u_{1}) ⋯ (s_{f(k)}, u_{k}),

where f, k are related to t by Definition 7.5. But then t ∈ X_{n}, by (7.6), so that k = 1, t′ = x_{1}, and u_{1} = x_{j}. If t = x_{i}, f(1) = i and

(s · ⟨s_{1}, …, s_{n}⟩, x_{j}) = ∑_{i∈[n]}(s, x_{i}) · (s_{i}, x_{j}). □

For any g = ⟨s_{1}, …, s_{n}⟩ : n → p in S⟨⟨ Σ ⟩⟩, let μ(g) denote the n×p matrix in Mat_{S}, such that

μ(g)_{i,j} := (s_{i}, x_{j}).

Proposition 7.10 For f : n → p and g : p → q in S⟨⟨ Σ ⟩⟩,

μ(f · g) = μ(f) · μ(g).

If f, g : n → p in S⟨⟨ Σ ⟩⟩,

μ(f + g) = μ(f) + μ(g).

Proof. It is enough to prove both statements for the case n = 1. The result for composition follows from Lemma 7.9, and for addition by definition of f + g. □

Now let M(n, p) consist of all morphisms ⟨s_{1}, …, s_{n}⟩ : n → p in S⟨⟨ Σ ⟩⟩ such that, for each i ∈ [n], the support of s_{i} is a subset of X_{p}.

Proposition 7.11 M is a sub grove theory of S⟨⟨ Σ ⟩⟩, i.e., 0_{n,p} ∈ M(n, p); if g_{1}, g_{2} ∈ M(n, p), then g_{1} + g_{2} ∈ M(n, p), and if h ∈ M(p, q), g_{1} · h ∈ M(n, q), for each n, p, q ≥ 0. Also, η(x_{i}) ∈ M(1, p), for each i ∈ [p].

Proof. It is enough to prove these facts when n = 1. Now if t ∉ X_{p}, (g_{1} + g_{2}, t) = (g_{1}, t) + (g_{2}, t) = 0, so that M(1, p) is closed under addition. To show that M is closed under composition , write g_{1} = s, h = ⟨s_{1}, …, s_{p}⟩. Then, for any u ∈ T_{Σ}(X_{q}),

(s · h, u) = ∑_{t∈D_{n}(u)}(s, t) · (s_{f(1)}, u_{1}) ⋯ (s_{f(k)}, u_{k}),

as usual. But unless t ∈ X_{n}, the value (s, t) is 0. Thus, for t = x_{i} ∈ X_{n}, t′ = x_{1}, k = 1, f(1) = i and u = u_{1}, so that (s · h, u) = ∑_{i∈[n]}(s, x_{i}) · (s_{i}, u). But unless u ∈ X_{q}, we have (s_{i}, u) = 0. Thus, the support of s · h is a subset of X_{q}. □

Corollary 7.12 M is isomorphic to the matrix theory Mat_{S}.

Proof. This follows from Proposition 7.10 and from the fact that the restriction of μ to M is a bijection M → Mat_{S}. □

Proposition 7.13 If a : n → p in M and s, s′ : p → q in S⟨⟨ Σ ⟩⟩, then

a · (s + s′) = a · s + a · s′.

Proof. We assume n = 1. Since the support of a is a subset of X_{p}, for any u ∈ T_{Σ}(X_{q}), and any r = ⟨r_{1}, …, r_{p}⟩ : p → q, by (7),

(a · r, u) = ∑_{i∈[p]}(a, x_{i}) · (r_{i}, u).

The result follows immediately. □

Let T_{0}(1, p) denote the set of morphisms f_{0} : 1 → p in S⟨⟨ Σ ⟩⟩ such that

i ∈ [p] ⟹ (s, x_{i}) = 0.

Let T_{0}(n, p) be those morphisms n → p such that each component is in T_{0}(1, p).

We note the following obvious fact.

Proposition 7.14 Any f : n → p in S⟨⟨ Σ ⟩⟩ can be written uniquely as f = a + g, where a : n → p in M and g : n → p in T_{0}. □

Proposition 7.15 Suppose that f, g ∈ T_{0}(n, p). Then f + g ∈ T_{0}(n, p). If a ∈ M(k, n), then a · f ∈ T_{0}(k, p). If h : p → q in S⟨⟨ Σ ⟩⟩, then f · h ∈ T_{0}(n, q). The constant function in S⟨⟨ Σ^{p} ⟩⟩ with value 0 belongs to T_{0}(1, p).

Proof. We prove closure of T_{0} under left composition with morphisms in M. It is enough to assume k = 1, so let s : 1 → n in M and g = ⟨s_{1}, …, s_{n}⟩ in T_{0}(n, p). By Lemma 7.9, for each x_{j} ∈ X_{q},

(s · g, x_{j}) = ∑_{i∈[n]}(s, x_{i}) · (s_{i}, x_{j}).

But, for each i ∈ [n], s_{i} ∈ T_{0}(1, q), so that (s_{i}, x_{j}) = 0. Hence (s·g, x_{j}) = 0.

The fact that T_{0} is closed under right composition with any morphism is proved in the same way, using Lemma 7.9 again. □

Proposition 7.16 If g ∈ T_{0}(1, 1 + p) and b : 1 → p in M, then there is a unique ξ : 1 → p ∈ S⟨⟨ Σ ⟩⟩ such that

ξ = ((0_{1} ⊕ b) + g) · ⟨ξ, 1_{p}⟩.

Proof. Recall that S⟨⟨ Σ^{p} ⟩⟩ is a complete metric space. We claim that the function C : S⟨⟨ Σ^{p} ⟩⟩ → S⟨⟨ Σ^{p} ⟩⟩ defined by

C(s) := ((0_{1} ⊕ b) + g) · ⟨s, 1_{p}⟩

is a proper contraction on the complete metric space S⟨⟨ Σ^{p} ⟩⟩. It then follows from the Banach fixed point theorem that C has a unique fixed point, which is the statement of the proposition.

Let r ∈ S⟨⟨ Σ^{1+p} ⟩⟩ be defined as

r = (0_{1} ⊕ b) + g.

Note that M(0_{1} ⊕ b) is the matrix

[0, (b, x_{1}), …, (b, x_{p})].

We compute the value of r on each x_{j} ∈ X_{1+p}.

(r, x_{j}) = \begin{cases}(g, x_{1}) = 0 & j = 1 \\ (b, x_{j−1}) + (g, x_{j}) = (b, x_{j−1}) & j > 1 \end{cases}

since g ∈ T_{0}(1, 1 + p).

Now C(s) = r · ⟨s, s_{2}, …, s_{1+p}⟩, where, for j ∈ [p], s_{1+j} = η(x_{j}). Thus, by Lemma 7.9, for j ∈ [p],

(C(s), x_{j}) = (r, x_{1}) · (s, x_{j}) + ∑_{i∈[p]}(b, x_{i}) · (η(x_{i}), x_{j})
= ∑_{i∈[p]}(b, x_{i}) · (η(x_{i}), x_{j})
= (b, x_{j}).

since (r, x_{1}) = 0. For an atomic tree σ_{0} · 0_{p}, with σ_{0} ∈ Σ_{0}, (C(s), u) = (g, σ_{0} · 0_{1+p}). Thus, for any s_{1}, s_{2} in S⟨⟨ Σ^{p} ⟩⟩, C(s_{1}) and C(s_{2}) agree on all trees in T_{Σ}(X_{p}) of depth 0. For a tree u ∈ T_{Σ}(X_{p}) of depth at least 1,

(C(s), u) = ∑_{t∈D_{1+p}(u)}(r, t) · (s_{f(1)}, u_{1}) ⋯ (s_{f(k)}, u_{k}),

where u = t′ · ⟨u_{1}, …, u_{k}⟩, t = t′ · f, as always. Let A be the collection of all trees in D_{1+p}(u) that have at least one leaf labeled x_{1}, and let B = D_{1+p}(u) − A. Then let

C_{A}(s, u) = ∑_{t∈A} C_{t}(s, u)
C_{B}(s, u) = ∑_{t∈B} C_{t}(s, u),

where, for t ∈ D_{1+p}(u),

C_{t}(s, u) := (r, t) · (s_{f(1)}, u_{1}) ⋯ (s_{f(k)}, u_{k}).

Then (C(s), u) = C_{A}(s, u)+C_{B}(s, u). Note that for any s, s′ in S⟨⟨ Σ^{p} ⟩⟩ and any t ∈ B,

C_{t}(s, u) = C_{t}(s′, u),

since for trees t ∈ B, f(i) > 1, for all i ∈ [k], so that the functions s_{f(i)} are in the set {η(x_{1}), …, η(x_{p})}. Let β be this common value C_{B}(s, u). So, (C(s), u) = β + C_{A}(s, u). If C(s, u) ≠ C(s′, u), there must be at least one tree t in A with C_{t}(s, u) ≠ C_{t}(s′, u). Assume that t is one such tree. We know ht(t) > 0. Assume further, for ease of notation, that f^{−1}(1) = {1, 2, …, j}, for some j, 1 ≤ j ≤ k. Then

C_{t}(s, u) = (r, t) · (s, u_{1}) ⋯ (s, u_{j})(s_{f(j+1)}, u_{j+1}) ⋯ (s_{f(k)}, u_{k})
C_{t}(s′, u) = (r, t) · (s′, u_{1}) ⋯ (s′, u_{j})(s_{f(j+1)}, u_{j+1}) ⋯ (s_{f(k)}, u_{k})

Hence, (s, u_{i}) ≠ (s′, u_{i}), for at least one i ∈ [j]. Since

u = t′ · ⟨u_{1}, …, u_{k}⟩

and ht(t′) = ht(t) > 0,

d(C(s), C(s′)) ≤ \frac{1}{2}d(s, s′). □

Since we have verified the hypotheses of the Proposition 5.3, by the grove extension theorem, we get the following result.

Corollary 7.17 If S is a Conway or iteration semiring, there is a unique extension of the fixed point operation on M to all of S⟨⟨ Σ ⟩⟩ so that S⟨⟨ Σ ⟩⟩ is a Conway or iteration theory.

The proof of the grove extension theorem gives some more information as to the value of s^{†}, for s : 1 → 1 + p in S⟨⟨ Σ ⟩⟩.

Indeed, suppose we write s = [a, b] + g, where [a, b] : 1 → 1 + p in Mat_{S} and g ∈ T_{0}. Then we know, from this proof, that s^{†} = (a^{∗} · (0_{1} ⊕ b + g))^{†}. But

a^{∗} · (0_{1} ⊕ b + g) = 0_{1} ⊕ (a^{∗}b) + (a^{∗} · g),

and a^{∗} · g is in T_{0}. Thus, by the Banach fixed point theorem, s^{†} is the metric limit lim_{n} s_{n}, where

s_{0} := 0_{p}
s_{n+1} := (0_{1} ⊕ (a^{∗}b) + (a^{∗}g)) · ⟨s_{n}, 1_{p}⟩
= a^{∗}b + (a^{∗}g) · ⟨s_{n}, 1_{p}⟩

We could have chosen any element in S⟨⟨ Σ^{p} ⟩⟩ as s_{0}. In the case that S is a continuous, naturally ordered semiring, 0_{p} is the least in S⟨⟨ Σ^{p} ⟩⟩, so that, with s_{0} = 0_{p}, s^{†} = sup_{n} s_{n}, as well. □

8 Proof of the main theorem

We repeat here the hypotheses of the grove extension theorem.

We assume T is a grove theory, M is a sub grove theory of T which is a matrix theory, and

H1. T_{0} is an M-ideal in T.

H2. Every f : n → p in T can be written uniquely as

f = a + f_{0}, a ∈ M, f_{0} ∈ T_{0}

H3. If a ∈ M and f, g ∈ T have appropriate sources and targets, then

a · (f + g) = a · f + a · g.

H4. M is a Conway theory, so that there is a ^{∗}-operation on the square matrices satisfying

(ab)^{∗} = 1_{n} + a(ba)^{∗}b, a : n → m, b : m → n
(a + b)^{∗} = (a^{∗}b)^{∗}a^{∗}, a, b : n → n.

In particular, S = M(1, 1) is a Conway semiring. Of course, M has a ^{†} operation derived from ^{∗} as usual: if a is an n×n matrix and b is n×p, then

[a b]^{†} = a^{∗}b : n  [figure] p.

H5. For every f_{0} : n → n+p in T_{0} and b : n → p in M, there is a unique solution to the equation

ξ = ((0_{n} ⊕ b) + f_{0}) · ⟨ξ, 1_{p}⟩,

and we denote the solution by

ξ = ((0_{n} ⊕ b) + f_{0})^{∇}.

Theorem 8.1 (Grove extension theorem) Under the above hypotheses, there is a unique way to define a dagger operation ^{†} on T extending that on M and the operation ^{∇} such that T becomes a Conway theory. Further, if M satisfies the weak functorial identity, so does T; if M is an iteration theory, so is T.

Proof.

Uniqueness. First, we show that there is at most one such extension.

Suppose that T has such a dagger operation making it a Conway theory. Then if g = ((0_{n} ⊕ b) + f_{0}), for f_{0} : n → n + p in T_{0} and b : n → p in M, by the fixed point identity,

g^{†} = ((0_{n} ⊕ b) + f_{0}) · ⟨g^{†}, 1_{p}⟩.

Thus

((0_{n} ⊕ b) + f_{0})^{†} = ((0_{n} ⊕ b) + f_{0})^{∇}.

So any fixed point operation ^{†} must extend ^{∇}.

We prove a proposition that will be used elsewhere.

Proposition 8.2 Assume that T is a Conway grove theory with a Conway matrix subtheory M. Then, for any f_{0} : n → n + p in T and [a, b] : n → n + p in M,

(f_{0} + [a, b])^{†} = (a^{∗} · ((0_{n} ⊕ b) + f_{0}))^{†}.

Lemma 8.3 With the same assumptions on T, M, if a : n → n in M and g : n → n + p in T,

(a ⊕ 0_{n+p} + 0_{n} ⊕ g)^{†} = a^{∗}g : n  [figure] n + p

Proof. Since ^{†} extends the dagger operation on M,

(a ⊕ 0_{n+p} + 0_{n} ⊕ 1_{n} ⊕ 0_{p})^{†} = [a, 1_{n}, 0_{n,p}]^{†}
= [a^{∗}, 0_{n,p}]
= a^{∗} ⊕ 0_{p}.

Then, since

(a ⊕ 0_{n+p} + 0_{n} ⊕ g) = (a ⊕ 0_{n+p} + 0_{n} ⊕ 1_{n} ⊕ 0_{p}) · (1_{n} ⊕ ⟨g, 0_{n} ⊕ 1_{p}⟩),

we have, using the parameter identity,

(a ⊕ 0_{n+p} + 0_{n} ⊕ g)^{†} = ((a ⊕ 0_{n+p} + 0_{n} ⊕ 1_{n} ⊕ 0_{p})^{†} · ⟨g, 0_{n} ⊕ 1_{p}⟩
= (a^{∗} ⊕ 0_{p}) · ⟨g, 0_{n} ⊕ 1_{p}⟩
= a^{∗} · g. □

We now complete the proof of Proposition 8.2. Suppose that f = ([a, b]+ f_{0}) : n → n + p in T, f_{0} ∈ T, and [a, b] : n → n + p in M. Then

f = (a ⊕ 0_{p}) + ((0_{n} ⊕ b) + f_{0}).

If g = ((0_{n} ⊕ b) + f_{0}), then,

f^{†} = ((a ⊕ 0_{p}) + g)^{†}
= (((a ⊕ 0_{n+p}) + (0_{n} ⊕ g)) · ⟨1_{n}, 1_{n}⟩ ⊕ 1_{p}))^{†}
= ((a ⊕ 0_{n+p}) + (0_{n} ⊕ g))^{††},

using the double dagger identity,

= (a^{∗} · g)^{†},

by Lemma 8. This fact proves Proposition 8.2.

Now if f_{0} ∈ T_{0}, by Proposition 8.2,

(a^{∗} · g)^{†} = (a^{∗} · g)^{∇}.

Indeed, since T_{0} is an M-ideal, a^{∗} · f_{0} ∈ T_{0}. Also,

a^{∗} · g = a^{∗} · ((0_{n} ⊕ b) + f_{0})
= (0_{n} ⊕ a^{∗}b) + (a^{∗} · f_{0}),

by H3. Thus, (a^{∗} · g)^{†} = (a^{∗} · g)^{∇}, showing that ^{†} is determined by ^{∗} and ∇. □

Existence.

We use the formula derived above to define ^{†}. So, given f = ([a, b]+f_{0}) : n → n + p, with [a, b] ∈ M and f_{0} ∈ T_{0}, we define

f^{†} := (a^{∗} · g)^{∇},

where

g := (0_{n} ⊕ b) + f_{0} : n  [figure] n + p.

Since f can be written as [a, b] + f_{0} in exactly one way, f ↦ f^{†} is well defined.

Lemma 8.4 The dagger operation extends the dagger operation on M.

Proof. Choose f_{0} = 0_{n,n+p} ∈ T_{0}. Then, by definition, if f = [a, b]+f_{0} = [a, b] : n → n + p, then

g = (0_{n} ⊕ b) + f_{0} = 0_{n} ⊕ b,

so that

a^{∗} · g = 0_{n} ⊕ a^{∗}b, and
f^{†} = (0_{n} ⊕ a^{∗}b)^{∇}
= a^{∗}b,

which is the dagger operation in M. □

Lemma 8.5 The dagger operation extends ^{∇}.

Suppose that f = 0_{p} ⊕ b + f_{0}, so that a = 0_{n,n}. Then, since 0_{n,n}^{∗} = 1_{n},

f^{†} = (0_{n,n}^{∗} · f)^{∇}
= f^{∇}. □

¿From now on, we drop the use of ^{∇}, so that

((a ⊕ 0_{p}) + f)^{†} = (a^{∗} · f)^{†},

whenever a : n → p ∈ M and f = (0_{n} ⊕ b) + f_{0} : n → n + p, with b : n → p in M and f_{0} ∈ T_{0}.

To save space, we write f ∈ T̂_{0} if f = (0_{n} ⊕ b) + f_{0} : n → n + p, as above.

Lemma 8.6 For a : n → n in M and f : n → n + p ∈ T̂_{0},

(a^{∗} · f)^{†} = a^{∗} · (f · (a^{∗} ⊕ 1_{p}))^{†}.

Thus,

((a ⊕ 0_{p}) + f)^{†} = a^{∗} · (f · (a^{∗} ⊕ 1_{p}))^{†}.

Proof. By hypotheses H1 and H3, a^{∗} · f ∈ T̂_{0}. Thus, it is enough to show that a^{∗} · (f · (a^{∗} ⊕ 1_{p}))^{†} is a solution of the fixed point equation for a^{∗} · f.

a^{∗} · f · ⟨a^{∗} · (f · (a^{∗} ⊕ 1_{p}))^{†}, 1_{p}⟩ = a^{∗} · f · (a^{∗} ⊕ 1_{p}) · ⟨(f · (a^{∗} ⊕ 1_{p}))^{†}, 1_{p}⟩
= a^{∗} · (f · (a^{∗} ⊕ 1_{p}))^{†},

since the fixed point identity holds for morphisms in T_{0}.

In order to show that, equipped with this dagger operation T is a Conway theory, we will show that it satisfies the parameter, composition and double dagger identities (see [7], Chapter 6.2). For use in the argument, we show first that it satisfies the fixed point identity.

Proposition 8.7 The operation ^{†} satisfies the fixed point identity.

Proof. Suppose that a : n → n in M and f : n → n + p in T̂_{0}. We want to show

((a ⊕ 0_{p}) + f)^{†} = ((a ⊕ 0_{p}) + f) · ⟨((a ⊕ 0_{p}) + f)^{†}, 1_{p}⟩,

in other words, that

([a, 0] + f) · ⟨(a^{∗} · f)^{†}, 1_{p}⟩ = (a^{∗} · f)^{†}.

But,

([a, 0] + f) · ⟨(a^{∗} · f)^{†}, 1_{p}⟩ = a(a^{∗} · f)^{†} + f · ⟨(a^{∗} · f)^{†}, 1_{p}⟩,

since composition on the right distributes over sums,

= a(a^{∗} · f)^{†} + f · ⟨a^{∗} · (f · (a^{∗} ⊕ 1_{p}))^{†}, 1_{p}⟩

by Lemma 8.6,

= a(a^{∗} · f)^{†} + f · (a^{∗} ⊕ 1_{p}) · ⟨(f · (a^{∗} ⊕ 1_{p}))^{†}, 1_{p}⟩
= a(a^{∗} · f)^{†} + (f · (a^{∗} ⊕ 1_{p}))^{†}
= aa^{∗} · (f · (a^{∗} ⊕ 1_{p}))^{†} + (f · (a^{∗} ⊕ 1_{p}))^{†}
= (aa^{∗} + 1_{n}) · (f · (a^{∗} ⊕ 1_{p}))^{†}
= a^{∗} · (f · (a^{∗} ⊕ 1_{p}))^{†}
= (a^{∗} · f)^{†},

again, by Lemma 8.6. Note that the morphism f · (a^{∗} ⊕ 1_{p}) belongs to T̂_{0}. We used the fact that by assumptions H5 and H4, the fixed point identity holds for morphisms in M and T̂_{0}.

Proposition 8.8 The composition identity holds.

Proof. For notational simplicity, we prove this in the parameter-free case. We will show that

((a + f) · (b + g))^{†} = (a + f) · ((b + g) · (a + f))^{†},  (8)

where a : n → m, b : m → n in M and f : n → m, g : m → n in T̂_{0}. The left hand side of (8) is

((ab)^{∗}(f · (b + g) + ag))^{†}

and since the morphism (ab)^{∗}(f · (b + g) + ag) is in T̂_{0}, it is enough to show that the right hand side of (8) is a solution of the iteration equation for this morphism.

Let h abbreviate the morphism ((b + g)(a + f))^{†}, so that

h = ((ba)^{∗}(g · (a + f) + bf))^{†}.

8 Proof of the main theorem 28 Then,

(ab)^{∗}(f · (b + g) + ag)(a + f) · h = (ab)^{∗}f · (b + g)(a + f) · h
+(ab)^{∗}ag(a + f) · h
= (ab)^{∗}f · h + (ab)^{∗}ag(a + f) · h
= a(ba)^{∗}bf · h + f · h + a(ba)^{∗}g(a + f) · h
= a(ba)^{∗}(bf + g(a + f))((ba)^{∗}(bf + g(a + f))^{†}
+f · h
= a((ba)^{∗}(bf + g(a + f))^{†} + f · h
= a · h + f · h
= (a + f)((b + g)(a + f))^{†}. □

Proposition 8.9 The parameter identity holds. First, we need the following fact. Lemma 8.10 If f : n → n+p is in T̂_{0}, so is f ·(1_{n}⊕g), for any g : p → q. Proof. Indeed, if f = (0_{n} ⊕ b) + f_{0}, as always, then f_{0} · (1_{n} ⊕ g) is in T_{0}, since T_{0} is closed under right composition with any morphism. Also,

f · (1_{n} ⊕ g) = ((0_{n} ⊕ b) + f_{0}) · (1_{n} ⊕ g)
= (0_{n} ⊕ (bg)) + (f_{0} · (1_{n} ⊕ g)).

Now, writing g = (a + g_{0}), where a : p → q in M and g_{0} : p → q in T_{0}, we have

bg = b · (a + g_{0})
= b · a + b · g_{0},

by H3. Now b · a ∈ M and b · g_{0} ∈ T_{0}. Thus, we have

f · (1_{n} ⊕ g) = (0_{n} ⊕ b′) + f′_{0}, where
b′ = b · a
f′_{0} = b · g_{0} + f_{0} · (1_{n} ⊕ g),

completing the proof. □

Now suppose that a : n → n in M, f : n → n + p in T̂_{0} and g : p → q in T. We want to show that

(([a, 0] + f) · (1_{n} ⊕ g))^{†} = (([a, 0] + f)^{†} · g.

But

(([a, 0] + f) · (1_{n} ⊕ g))^{†} = ([a, 0] + f · (1_{n} ⊕ g))^{†}
= (a^{∗} · f · (1_{n} ⊕ g))^{†}.

Now, since the parameter identity holds for unique fixed points, ([7], Chapter 5) and since the morphism a^{∗} · f · (1_{n} ⊕ g) is in T̂_{0},

(a^{∗}f · (1_{n} ⊕ g))^{†} = (a^{∗}f)^{†} · g
= (([a, 0] + f)^{†} · g,

as was to be shown. □

We now turn to the double dagger identity.

Proposition 8.11 The double dagger identity holds.

Proof. We consider only the parameterless case. Let g = [a, b] + f : n → n + n, where [a, b] ∈ M and f ∈ T_{0}. Let ρ = ⟨1_{n}, 1_{n}⟩. We want to show that

(g · ρ)^{†} = g^{††}.  (9)

But,

(g · ρ)^{†} = (([a, b] + f) · ρ)^{†}
= (a + b + (f · ρ))^{†}
= ((a + b)^{∗} · (f · ρ))^{†}.

Suppose that we can prove

((a + b)^{∗} · f · ρ) · g^{††} = g^{††},  (10)

then, since (a + b)^{∗} · (f · ρ) ∈ T_{0}, we have

((a + b)^{∗} · f · ρ)^{†} = g^{††},

8 Proof of the main theorem 30

showing that (9) holds. So we now prove (10).

g^{†} = ([a, b] + f)^{†}
= ([a, 0] + ([0, b] + f))^{†}
= (a^{∗}([0, b] + f))^{†}
= ([0, a^{∗}b] + a^{∗} · f)^{†}.

But, by the fixed point identity proved above,

([0, a^{∗}b] + a^{∗} · f)^{†} = ([0, a^{∗}b] + a^{∗} · f) · ⟨([0, a^{∗}b] + a^{∗} · f)^{†}, 1_{n}⟩
= ([0, a^{∗}b] + a^{∗} · f) · ⟨g^{†}, 1_{n}⟩
= a^{∗}b + a^{∗} · f · ⟨g^{†}, 1_{n}⟩.

Thus,

g^{††} = ((a^{∗}b)^{∗}a^{∗} · f · ⟨g^{†}, 1_{n}⟩)^{†}
= ((a + b)^{∗} · f · ⟨g^{†}, 1_{n}⟩)^{†}.  (11)

We now complete the proof of (10).

(a + b)^{∗} · f · ρ · g^{††} = (a + b)^{∗} · f · ⟨g^{††}, g^{††}⟩
= (a + b)^{∗} · f · ⟨g^{†}, 1_{n}⟩ · g^{††},

by the fixed point identity for g^{†},

= (a + b)^{∗} · f · ⟨g^{†}, 1_{n}⟩ · ((a + b)^{∗} · f · ⟨g^{†}, 1_{n}⟩)^{†}
= ((a + b)^{∗} · f · ⟨g^{†}, 1_{n}⟩)^{†}
= g^{††},

by two applications of (11). □ This completes the proof that with the extension, T is a Conway theory.

Proposition 8.12 Suppose that the weak functorial implication holds in M. Then it also holds in T.

Proof. Suppose that the diagram below commutes, where ρ : n → 1 is the unique base morphism, a : n → n, b : 1 → 1 in M, and f, g are in T̂_{0}.

[figure: 1; 1 + p; (b⊕0_{p})+g; n; 1; ρ; n; n + p; (a⊕0_{p})+f; n + p; 1 + p; ρ⊕1_{p}]

Since T is the direct sum of M and T_{0}, we have

a · ρ = ρ · b
f · (ρ ⊕ 1_{p}) = ρ · g.

Since the weak functorial implication holds in M,

a^{∗} · ρ = ρ · b^{∗}.

Since the weak functorial implication holds for unique fixed points,

f^{†} = ρ · g^{†}.

In fact,

a^{∗} · f · (ρ ⊕ 1_{p}) = a^{∗} · ρ · g
= ρ · b^{∗} · g,

so that

(a^{∗} · f)^{†} = ρ · (b^{∗} · g)^{†},

completing the proof. □

Last, we show that if M is an iteration theory, so is T.

Proposition 8.13 If M satisfies the group equation associated with the finite group G, then so does T.

Proof. Let h : 1 → n+p be any morphism and suppose that G is a group of order n (whose underlying set is [n]). Let h_{G} denote the morphism n → n + p:

⟨h · (ρ_{1}^{G} ⊕ 1_{p}), …, h · (ρ_{n}^{G} ⊕ 1_{p})⟩

where the morphisms ρ_{i}^{G} : n → n are the base morphisms determined by the group operation i, j ↦ i • j of G:

ρ_{i}^{G}(j) := i • j.

We use the same notation for morphisms in M: If a = [a_{1}, …, a_{n}] : 1 → n in M,

a_{G} = [ \begin{matrix}a_{ρ_{1}^{G}(1)} & … & a_{ρ_{1}^{G}(n)} \\ & … \\ a_{ρ_{n}^{G}(1)} & … & a_{ρ_{n}^{G}(n)} \end{matrix} ]

It is known from [26] that

(a_{G})^{∗} = b_{G},

for some b = [b_{1}, …, b_{n}] in M.

So assume that a : 1 → n in M and f : 1 → n + p in T̂_{0}. Let \overline{a} denote the sum of the entries in a, so that \overline{a} = a · ρ, where ρ : n → 1 is base. Let \overline{f} = f · (ρ ⊕ 1_{p}).

We want to show that

((a_{G} ⊕ 0_{p}) + f_{G})^{†} = ρ · ((\overline{a} ⊕ 0_{p}) + \overline{f})^{†}.  (12)

The left hand side is

((a_{G})^{∗}f_{G})^{†} = (b_{G} · f_{G})^{†}.

But b_{G} · f ∈ T̂_{0}, and

b_{G} · f_{G} · ρ = b_{G} · ρ · \overline{f}
= ρ · \overline{b} · \overline{f},

where \overline{b} is the sum of the entries of b_{G}. Since the weak functorial implication holds for unique fixed points ([7], Chapter 5), we have

(b_{G} · f_{G})^{†} = ρ · (\overline{b} · \overline{f})^{†},

i.e.,

((a_{G})^{∗}f_{G})^{†} = ρ · (\overline{b} · \overline{f})^{†}.

But since the group identity holds in M, \overline{b} is just \overline{a}^{∗}. Thus,

((a_{G})^{∗}f_{G})^{†} = ρ(\overline{a}^{∗}\overline{f})^{†}
= ρ · ((\overline{a} ⊕ 0_{p}) + \overline{f})^{†},

proving (12). □

The proof of the grove extension theorem is complete.

9 A Kleene Theorem

Assume that T is a Conway grove theory and M is a sub Conway grove theory of T which is a matrix theory. For a given collection Σ of scalar morphisms in T we will describe the smallest sub Conway grove theory of T containing all the morphisms in M ∪ Σ.

In more detail, we are assuming that

1. T is a Conway grove theory and M is a sub Conway theory of T that is a matrix theory. Thus, M has a^{∗}-operation on the p×p matrices, for each p ≥ 1, satisfying the star sum and product identities (3) and (4) in Section 3 above. The hom-set M(1, 1) is a Conway semiring, which we denote by S.

2. If a ∈ M and f, g ∈ T have appropriate sources and targets, then

a · (f + g) = a · f + a · g.

Let Σ be a collection of scalar morphisms in T.

Definition 9.1 A morphism f : 1 → n + p is primitive of weight n if f is a finite sum of morphisms of the sort

s · σ · ρ (type 1)
0_{n} ⊕ (s · τ) (type 2),

where s ∈ S, σ : 1 → k ∈ Σ, ρ : k → n + p and τ : 1 → p are base. A morphism f = ⟨f_{1}, …, f_{q}⟩ : q → p is primitive of weight n if each component is primitive of weight n.

Note that any 1×p matrix in M is primitive of type 2, (when n = 0), so, in effect, all morphisms in M are primitive (of type 2).

We list some easy consequences of these definitions.

Proposition 9.2 1. If f : r → n + p is primitive of weight n, so is γ · f : m → n + p, for any base morphism γ : m → r.

2. If f : 1 → n + p is primitive of weight n of type 1, then f · γ : 1 → n + q is primitive of type 1, for any base γ : n + p → n + q.

3. If f : 1 → n + p is primitive of of weight n of type 2, then f · (1_{n} ⊕ 0_{m} ⊕ γ) : 1 → n + m + q is primitive of weight n + m of type 2, for any base γ : p → q.

4. If g : m → n + p is primitive of weight n, and b : m → m is in M, then b · g is primitive of weight n. Indeed, if m = 1, b = [s], say, and g = g_{1} + … + g_{r}, then b · g = s · g_{1} + … + s · g_{r}, since left composition with M-morphisms distributes over sums. And if g_{i} is primitive of any type, so is s · g_{i}.

5. If f : m → n + p is primitive of weight n, then 0_{q} ⊕ f is primitive of weight q + n.

6. If 0_{q} ⊕ f : m → q + n + p is primitive of weight q + n, then f is primitive of weight n.

Definition 9.3 A normal description k → p of weight n is a pair

D = (α, f),

where f : n → n + p is primitive of weight n, and α : k → n is base. The behavior of the normal description D : k → p is the morphism

|D| := α · f^{†}.

Below, we will often write a primitive morphism f of weight n as

f = \overline{f} + (0_{n} ⊕ a),

where \overline{f} is of type 1 and a : n → p ∈ M.

A normal description D = (α, f) : k → p of weight n might be viewed as an “automaton” with n internal states, and p exit states; the values of α pick out the k start states among the internal states, and the behavior of D is the morphism in T determined by this automaton.

The rest of this section contains a proof of the following “Kleene” type theorem.

Theorem 9.4 The smallest sub Conway grove theory of T containing M and Σ consists of the behaviors of normal descriptions.

Proof. Let D denote the collection of all morphisms of the form |D|, for a normal description D.

First, it is clear that any sub Conway grove theory of T that contains S ∪ Σ will contain each morphism in D. Thus, we need show only that this collection of morphisms is itself a sub Conway grove theory of T.

D is closed under composition.

Suppose that D = (α, f) : k → p has weight n and E = (β, g) : p → q has weight m. Write

f = \overline{f} + (0_{n} ⊕ a)
g = \overline{g} + (0_{m} ⊕ b),

where a : n → p and b : m → q in M. Then, define the normal description D · E as

D · E := (α ⊕ 0_{m}, h),

where h : n + m → n + m + q is defined as follows:

h := ⟨h_{1}, h_{2}⟩, where
h_{1} = \overline{f} · (1_{n} ⊕ β ⊕ 0_{q}) + (0_{n} ⊕ (a · β · g))
h_{2} = 0_{n} ⊕ g.

Note that a · β · g is primitive, by Proposition 9.2. Thus, by Proposition 9.2, D · E : k → q is a primitive normal description, of weight n + m. Claim:

|D · E| = |D| · |E|.

Proof. First, note that for any morphisms F : n → n + m + q and G : m → m + q in a Conway theory,

⟨F, 0_{n} ⊕ G⟩^{†} = ⟨F^{†} · ⟨G^{†}, 1_{q}⟩, G^{†}⟩

by the pairing identity,

= ⟨(F · (1_{n} ⊕ ⟨G^{†}, 1_{q}⟩)^{†}, G^{†}⟩,

by the parameter identity. Thus, when F = h_{1} : n → n + m + q and G = g : m → m + q, so h_{2} = 0_{n} ⊕ g,

(1_{n} ⊕ 0_{m}) · h^{†} = ((\overline{f} · (1_{n} ⊕ β ⊕ 0_{q}) + 0_{n} ⊕ a · β · g) · (1_{n} ⊕ ⟨g^{†}, 1_{q}⟩))^{†}
= (\overline{f} · (1_{n} ⊕ β · g^{†} + 0_{n} ⊕ a · β · g^{†})^{†}
= ((\overline{f} + 0_{n} ⊕ a) · (1_{n} ⊕ β · g^{†}))^{†}
= (\overline{f} + 0_{n} ⊕ a)^{†} · β · g^{†}
= f^{†} · β · g^{†}.

Thus,

|D · E| = (α ⊕ 0_{m}) · h^{†}
= α · (1_{n} ⊕ 0_{m}) · h^{†}
= α · f^{†} · β · g^{†}
= |D| · |E|.

D is closed under ^{†}.

Suppose that D = (α, f) : k → k + p has weight n, so that α : k → n is base and f = \overline{f} + 0_{n} ⊕ [a, b] : n → n + k + p, where a : n → k, b : n → p in M.

Define |D^{†}| as (α, g), where

g = (a · α)^{∗} · (\overline{f} · (⟨1_{n}, α⟩ ⊕ 1_{p}) + (0_{n} ⊕ b))
= ((a · α)^{∗} · \overline{f} · (⟨1_{n}, α⟩ ⊕ 1_{p})) + (0_{n} ⊕ (a · α)^{∗} · b).

We have used the fact that M has a ^{∗} operation, and composition on the left with M-morphisms distributes over sums.

We claim

|D^{†}| = |D|^{†}.

Indeed,

|D|^{†} = (α · (\overline{f} + (0_{n} ⊕ [a, b]))^{†})^{†}
= α · ((\overline{f} + (0_{n} ⊕ [a, b]))^{†} · (α ⊕ 1_{p}))^{†},

by the composition identity,

= α · ((\overline{f} + (0_{n} ⊕ [a, b])) · (1_{n} ⊕ α ⊕ 1_{p}))^{††},

by the parameter identity,

= α((\overline{f} + 0_{n} ⊕ [a, b]) · (1_{n} ⊕ α ⊕ 1_{p}) · (⟨1_{n}, 1_{n}⟩ ⊕ 1_{p}))^{†},

by the double dagger identity,

= (α · (\overline{f} + (0_{n} ⊕ [a, b])) · (⟨1_{n}, α⟩ ⊕ 1_{p}))^{†}
= α · ((\overline{f} · (⟨1_{n}, α⟩ ⊕ 1_{p}) + [a · α, b])^{†}
= α · ((a · α)^{∗} · (\overline{f} · (⟨1_{n}, α⟩ ⊕ 1_{p}) + (0_{n} ⊕ b))^{†}
= α · g^{†}
= |D^{†}|. □

D is closed under +.

Suppose that D = (α, f) and E = (β, g) are normal descriptions n → p of weights w, s respectively. Define the normal description D + E = (γ, h) : n → p of weight w + s + n as follows:

h := ⟨h_{1}, h_{2}, h_{3}⟩, where
h_{1} := f · (1_{w} ⊕ 0_{s} ⊕ 0_{n} ⊕ 1_{p})
h_{2} := g · (0_{w} ⊕ 1_{s} ⊕ 0_{n} ⊕ 1_{p})
h_{3} := α · h_{1} + β · h_{2}
γ := 0_{w} ⊕ 0_{s} ⊕ 1_{n}.

Then, by two uses of the pairing identity,

h^{†} = ⟨f^{†}, g^{†}, α · f · ⟨f^{†}, 1_{p}⟩, β · g · ⟨g^{†}, 1_{p}⟩⟩
= ⟨f^{†}, g^{†}, α · f^{†} + β · g^{†}⟩,

so that |D + E| = γ · h^{†} = |D| + |E|. □

D is closed under pairing.

Suppose that D = (α, f) and E = (β, g) are normal descriptions n → p of weights w, s respectively. Define the normal description ⟨D, E⟩ = (γ, h) : n → p of weight w + s as follows:

h := ⟨h_{1}, h_{2}⟩, where
h_{1} := f · (1_{w} ⊕ 0_{s} ⊕ 1_{p})
h_{2} := g · (0_{w} ⊕ 1_{s} ⊕ 1_{p})
γ := ⟨α · (1_{w} ⊕ 0_{s}), β · (0_{w} ⊕ 1_{s})⟩

Then, by the pairing identity,

h^{†} = ⟨f^{†}, g^{†}⟩,

so that

|⟨D, E⟩| = γ · h^{†}
= ⟨α · f^{†}, β · g^{†}⟩
= ⟨|D|, |E|⟩. □

D contains all morphisms in M.

For [a, b] : n → p in M, let D be the description (α, f), where

α = 1_{n}
f = 0_{n} ⊕ [a, b].

Then, by the left zero identity,

|D| = α · (0_{n} ⊕ [a, b])^{†}
= [a, b].

It follows that all base morphisms are in D.

D contains all morphisms in Σ.

For σ : 1 → k, let D be the description (α, f), where

α = 1_{1}
f = σ · (0_{1} ⊕ 1_{k})
= 0_{1} ⊕ σ.

Then, by the left zero identity, σ = |D|. □

We have shown that the behaviors form a subtheory of T containing M ∪ Σ, closed under +,^{†}. Since Conway grove theories are defined by equations, any subtheory of a Conway grove theory closed under sum and † will also be a Conway grove theory. This completes the proof. □

10 Acknowlegment

The results of this paper were obtained during the second author’s visit at BRICS and the Department of Computer Science, Aalborg University. This author is indepted to the members of the DSS group for their hospitality.

References 39

References

[1] S. Banach, Sur les operations dans les ensembles abstraits et leur applications aux équations intégrales, Fundamenta Mathematica, 22(1922), 133–181.

[2] H. Bekic̆, Definable operations in general algebras, and the theory of automata and flowcharts, Technical Report, IBM Laboratory, Vienna, 1969.

[3] D. Benson and J. Tiuryn, Fixed points in free process algebras, Theoretical Computer Science 63(1989), 275–294.

[4] J. Berstel, and C. Reutenauer. Recognizable formal power series on trees. Theoretical Computer Science, 18(1982), 115–148.

[5] S.L. Bloom, C.C. Elgot and J.B. Wright, Solutions of the iteration equation and extension of the scalar iteration operation, SIAM J. Computing, 9(1980), 26–45.

[6] S.L. Bloom, C.C. Elgot and J.B. Wright, Vector iteration of pointed iterative theories, SIAM J. Computing, 9(1980), 525–540.

[7] S.L. Bloom and Z. Ésik, Iteration Theories: The Equational Logic of Iterative Processes, EATCS Monographs on Theoretical Computer Science, Springer–Verlag, 1993.

[8] S.L. Bloom and Z. Ésik, Matrix and matricial iteration theories, Part I, J. of Computer and System Sciences, 46(1993), 381–408.

[9] S.L. Bloom and Z. Ésik, Matrix and matricial iteration theories, Part II, J. of Computer and System Sciences, 46(1993), 409–439.

[10] S.L. Bloom and Z. Ésik, The equational logic of fixed points. Theoretical Computer Science 179(1997), 1–60.

[11] S.L. Bloom, S. Ginali and J. Rutledge, Scalar and vector iteration, J. Computer and System Sciences, 14(1977), 251–256.

[12] S. Bozapalidis. Convex algebras, convex modules and formal power series on trees. J. Autom. Lang. Comb. 1 (1996), no. 3, 165–180.

[13] L.E.J. Brouwer, Uber Abbildung von Mannigfaltigkeiten, Math. Annalen, 71(1910), 97–115.

[14] J.C. Conway, Regular Algebra and Finite Machines, Chapman and Hall, London, 1971.

[15] J.W. De Bakker and D. Scott, A theory of programs, Technical report, IBM Vienna, 1969.

[16] J.W. de Bakker and J.I. Zucker, Processes and the denotational semantics of concurrency, Information and Control, 54(1982), 70–120.

[17] J.W. de Bakker and J.N. Kok, Comparative Metric Semantics, Theoretical Computer Science 75(1-2), 1990, 14–43.

[18] J.W. de Bakker and J.H.A. Warmerdam. Four domains for concurrency. Theoretical Computer Science, 90(1), 1991, 127–149.

[19] C.C. Elgot, Monadic computation and iterative algebraic theories, in: Logic Colloquium 1973, Studies in Logic, J.C. Shepherdson, editor, volume 80, North Holland, Amsterdam, 1975, 175–230.

[20] C.C. Elgot, Matricial theories, J. of Algebra, 42(1976), 391–421.

[21] J. Engelfriet and E.M. Schmidt. IO and OI. I. J. Comput. System Sci. 15 (1977), 328–353.

[22] Z. Ésik, Group axioms for iteration. Information and Computation, 148(1999), 131–180.

[23] S.C. Kleene, Representation of events in nerve nets and finite automata. In C.E. Shannon and J. McCarthy, editors, Automata Studies, Princeton U. Press, Princeton, NJ, 1956. 3–41.

[24] P. Freyd, Algebraically complete categories, in: Category Theory, Como 1990, LNM vol. 1488, Springer–Verlag, 1991, 95–104.

[25] P. Freyd, Remarks on algebraically compact categories, in: Applications of Categories in Computer Science, London Math. Society Lecture Notes Series, vol. 77, Cambridge University Press, 1992, 95–106.

[26] D. Krob, Complete systems of B-rational identities, Theoretical Computer Science, 89(1991), 207–343.

[27] A. Bonnier-Rigny and D. Krob. A complete system of identities for oneletter rational expressions with multiplicities in the tropical semiring. Theoret. Comput. Sci. 134 (1994), no. 1, 27–50.

[28] W. Kuich. Automata and languages generalized to ω-continuous semirings, Theoret. Comp. Sci., 79(1991), 137–150.

[29] W. Kuich. Formal power series over trees. In Proc. 3rd International Conf. Developments in Language Theory (S. Bozapalidis, ed), Aristotle University of Thessaloniki, 1998, 61–101.

[30] F.W. Lawvere. Functorial semantics of algebraic theories. In: Proceedings of the National Academy of Sciences USA, 50(1963), 869–873.

[31] D.J. Lehmann and M.B. Smyth. Algebraic specification of data types: a synthetic approach. Math. Systems Theory, 14 (1981), no. 2, 97–139.

[32] R. Milner. A complete inference system for a class of regular behaviors. J. Comp. System Sci., 28 (1984), 439–466.

[33] D. Niwinski, On fixed-point clones, in: Proc. ICALP ’86, LNCS 226, Springer–Verlag, 1986, 464–473.

[34] G.D. Plotkin, Domains, Lecture Notes, Department of Computer Science, University of Edinburgh, 1983.

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

[36] A. Salomaa, On regular expressions and regular canonical systems, Math. Syst. Theory, 2(1968), 341–355.

[37] D.S. Scott. Data types as lattices. SIAM J. Computing, 5(3), 522–587 (1976).

[38] A.K. Simpson, A characterisation of the least fixed point operator by dinaturality, Theoretical Computer Science, 118(1993), 301–314.

[39] M.B. Smyth and G.D. Plotkin, The category theoretic solution of recursive domain equations, SIAM Journal of Computing, 11(1982), 761–783.

[40] A. Simpson and G. Plotkin. Complete Axioms for Categorical Fixedpoint operations. In: Proceedings of the 15th Annual IEEE Logic in Computer Science Colloq., 30-41, (2000).

[41] A. Tarski, A lattice-theoretical fixed point theorem and its applications. Pacific J. Math., 5(1955), 285–309.

11 Appendix: Theories and Trees

This section is intended as a quick review of the basic notions. We have lifted a great deal from our tutorial paper [10].

A Lawvere algebraic theory T, or just theory for short, is a category whose objects are the nonnegative integers in which the object n is the copower of the object 1 with itself n-times. (Sometimes Lawvere theories are defined dually with n being the nth power of the object 1.) See [30].

We may elaborate the definition somewhat by specifying the copower injections i_{n} : 1 → n, for i ∈ [n]. Thus, the official definition of theory is the following.

Definition 11.1 A theory T is a category whose objects are the nonnegative integers, which has, for each n ≥ 0, n “distinguished morphisms” i_{n} : 1 → n, i ∈ [n], with the property that for any p ≥ 0 and any family of morphisms g_{i} : 1 → p, i ∈ [n], there is a unique morphism g : n → p such that

i_{n} · g = g_{i}, i ∈ [n].

The uniquely determined morphism g is denoted ⟨g_{1}, …, g_{n}⟩, and is called the “tupling” of the g_{i}. Note that tupling determines a bijection

\overbrace{T (1, p)× … ×T (1, p)}^{n} → T (n, p),

so that one may specify a morphism f : n → p by giving its components i_{n} · f : 1 → p, i ∈ [n]. We assume that when i = n = 1, the distinguished morphism i_{n} is the identity morphism 1 → 1, so that ⟨g⟩ = g, for any g : 1 → p. In any theory we write the identity morphism p → p as 1_{p} : p → p. Note that 1_{p} = ⟨1_{p}, …, p_{p}⟩, the tupling of the p distinguished morphisms 1 → p.

The coproduct property implies that the object 0 is an initial object: there is a unique morphism 0 → n, for each n ≥ 0. We denote this morphism by

\xymatrix{0_{n} : 0 \ar[r] & n.}

In any theory, a morphism with source 1 is called a scalar morphism.

If T and T′ are theories, a theory morphism T → T′ is a functor which preserves the objects and distinguished morphisms. It follows that any theory morphism preserves tupling. (Morphisms n → p in some theory T might also legitimately be called “theory morphisms”, but we call them T -morphisms, or just “morphisms”.)

There is an “initial theory” Tot, the theory of all total functions [n] → [p], n, p ≥ 0. If T is any theory, there is a unique theory morphism Tot → T under which the function f : [n] → [p] is mapped to the T -morphism

\overline{f} := ⟨f(1)_{p}, …, f(n)_{p}⟩ : n  [figure] p.

The morphisms \overline{f} determined by functions are called base morphisms.

A theory is trivial if each hom-set T (n, p) has at most one morphism. If T is not trivial, the unique theory morphism from Tot is injective and we usually assume without comment that Tot is a subtheory of every theory.

It is useful to introduce the names

\xymatrix{κ : n \ar[r] & n + p}
\xymatrix{λ : p \ar[r] & n + p}

for the base morphisms which correspond to the inclusion function [n] → [n + p] and translated inclusion function [p] → [n + p]. Using these base morphisms, we introduce two derived operations on theories: pairing, which is a function

\xymatrix{T (n, p)×T (m, p) \ar[r] & T (n + m, p)}
f, g ↦ ⟨f, g⟩

for all n, m, p ≥ 0, and separated sum, which is an operation

\xymatrix{T (n, p)×T (m, q) \ar[r] & T (n + m, p + q)}
f, g ↦ f ⊕ g.

The definition of pairing is the following. For f : n → p, g : m → p in T, i ∈ [n + m],

i_{n+m} · ⟨f, g⟩ := \{ \begin{matrix}i_{n} · f & if i ∈ [n] \\ j_{m} · g & if i = n + j, j ∈ [m]. \end{matrix}

The definition of separated sum makes use of κ : p → p+q, λ : q → p+q, when f : n → p, g : m → q.

i_{n+m} · (f ⊕ g) := \{ \begin{matrix}i_{n} · f · κ & if i ∈ [n] \\ j_{m} · g · λ & if i = n + j, j ∈ [m]. \end{matrix}

There is an interesting calculus of theory terms built from the operations of pairing and separated sum. For example, the following equations are valid in all theories, when sources and targets are appropriate:

κ · ⟨f, g⟩ = f
λ · ⟨f, g⟩ = g
⟨κ · f, λ · f⟩ = f
⟨f, ⟨g, h⟩⟩ = ⟨⟨f, g⟩, h⟩
⟨f, g⟩ · h = ⟨f · h, g · h⟩  (13)
f ⊕ (g ⊕ h) = (f ⊕ g) ⊕ h
(f ⊕ g) · ⟨h, k⟩ = ⟨f · h, g · k⟩
(f ⊕ g) · (h ⊕ k) = (f · h) ⊕ (g · k)

Node Labeled Trees. Suppose that Σ = Σ_{n}, n ≥ 0, is a ranked set, and X = {x_{1}, …, x_{n}, …} is a countably infinite set of “variables” disjoint from each set Σ_{n}. We write X_{p} for the set {x_{1}, …, x_{p}}.

A (possibly infinite) Σ-tree t : 1 → p is a rooted, finitely branching tree whose leaves are labeled by letters in X_{p} ∪ Σ_{0}, and whose interior nodes of outdegree n ≥ 1 are labeled by letters in Σ_{n}. Any such tree may be modeled as a partial function t : [ω]^{∗} → ∪_{n≥0}Σ_{n} ∪ X_{p}, where [ω] denotes the positive integers, subject to the following conditions:

• The domain of t is a nonempty, prefix closed subset of [ω]^{∗}.

• If t(u) ∈ Σ_{n}, for some u ∈ [ω]^{∗} and n ≥ 0, then for any i ∈ [ω], t(ui) is defined iff i ∈ [n].

• If t(u) ∈ X_{p}, then t(ui) is not defined for any i ∈ [ω].

Let Σ TR(1, p) denote the set of all such trees. The subset of trees in Σ TR(1, p) with a finite domain is denoted T_{Σ}(X_{p}). The tree 1 → p whose root is a leaf labeled x_{i}, i ∈ [p] is denoted i_{p}.

One may compose a tree t in Σ TR(1, p) with a p-tuple of trees (g_{1}, …, g_{p}) in Σ TR(1, n) obtaining the tree denoted

t · ⟨g_{1}, …, g_{p}⟩

in Σ TR(1, n) by attaching a copy of the tree g_{i} to each leaf of t labeled x_{i}, i ∈ [p]. Note that

t · ⟨1_{p}, …, p_{p}⟩ = t
i_{p} · ⟨g_{1}, …, g_{p}⟩ = g_{i}, i ∈ [p].

We let Σ TR(n, p) denote the collection of n-tuples of trees in Σ TR(1, p).

The Σ-trees form a theory Σ TR, with n-tuples of Σ-trees in Σ TR(1, p) as morphisms n → p. A letter σ ∈ Σ_{n} is identified with the “atomic tree”

η(σ) : 1 [figure] n

whose root is labeled σ; the n-successors of the root are leaves, labeled in order x_{1}, …, x_{n}.

For i ∈ [p], the letter x_{i} is identified with the tree η(x_{i}), consisting only of a root labeled x_{i}.

The theory operation of tupling ⟨g_{1}, …, g_{n}⟩ when applied to the n-tuple (g_{1}, …, g_{n}) in Σ TR(1, p) produces the n-tuple (g_{1}, …, g_{n}), now considered a morphism g : n → p. The composite of ⟨t_{1}, …, t_{k}⟩ : k → n with this g is forced by (13) above to be defined as

⟨t_{1}, …, t_{k}⟩ · g = ⟨t_{1} · g, …, t_{k} · g⟩, t_{i} : 1  [figure] n, g : n  [figure] p.

Note that if t and the g_{i} have finite domains, so does t·⟨g_{1}, …, g_{p}⟩. Thus, the finite trees form a subtheory of Σ TR, denoted T_{Σ}.

If t : [ω^{∗}] → (⋃_{n} Σ_{n}) ∪ X_{p} is a tree and u ∈ [ω^{∗}], we write t_{u} for the tree

t_{u}(v) := t(uv), v ∈ [ω^{∗}].

A tree t is regular if the set {t_{u} : u ∈ [ω^{∗}]} is finite. The collection of regular trees determines another subtheory of Σ TR, denote Σ tr.

Recall that when Σ is ranked set, a Σ-algebra B is a set equipped with a function

\xymatrix{σ_{B} : B^{n} \ar[r] & B}

for each σ ∈ Σ_{n}. If B, C are Σ-algebras, a Σ-algebra morphism h : B → C is a function such that for all n ≥ 0 and all σ ∈ Σ_{n},

h(σ_{B}(b_{1}, …, b_{n}) = σ_{C}(h(b_{1}), …, h(b_{n})),

b_{i} ∈ B.

For each set p ≥ 0, the sets Σ TR(1, p) and T_{Σ}(1, p) are Σ-algebras, where for σ ∈ Σ_{n}, t_{i} ∈ Σ TR(1, p),

σ(t_{1}, …, t_{n}) := σ · ⟨t_{1}, …, t_{n}⟩.

We take it that the following facts are well-known.

Theorem 11.2 (Free theories) The theory T_{Σ} is the algebraic theory freely generated by Σ, i.e., for any algebraic theory T and any function h mapping Σ_{n} → B(1, n), for each n ≥ 0, there is a unique theory morphism h^{#} : T_{Σ} → T such that

h^{#}(η(σ)) = h(σ),

for all σ ∈ Σ_{n}, n ≥ 0.

12 Conway and Iteration Theories

Definition 12.1 A preiteration theory is a theory equipped with a dagger operation

\xymatrix{T (n, n + p) \ar[r] & T (n, p)}
f ↦ f^{†}

for each n, p ≥ 0. This operation need not satisfy any particular properties. A morphism φ : T → T′ of preiteration theories is a theory morphism which preserves the dagger operation, i.e.,

φ(f^{†}) = nφ(f)^{†}, f : n  [figure] n + p.

Notation. In any preiteration theory, we let ⊥_{n,p} : n → p abbreviate (1_{n} ⊕ 0_{p})^{†}, and when p = 0, we write just ⊥_{n}, and when n = 1, just ⊥.

Definition 12.2 A Conway theory is a preiteration theory satisfying the following equational axioms:

1. Parameter identity

(f · (1_{n} ⊕ g))^{†} = f^{†} · g,

all f : n → n + p, g : p → q. When n = 1, this equation is called the scalar parameter identity.

2. Composition identity

(f · ⟨g, 0_{n} ⊕ 1_{p}⟩)^{†} = f · ⟨(g · ⟨f, 0_{m} ⊕ 1_{p}⟩)^{†}, 1_{p}⟩,

all f : n → m + p, g : m → n + p. When m = n = 1, this equation is the scalar composition identity.

3. Double dagger identity

f^{††} = (f · (⟨1_{n}, 1_{n}⟩ ⊕ 1_{p}))^{†},

all f : n → n+n+p. When n = 1, this equation is called the scalar double dagger identity.

A morphism of Conway theories is a preiteration theory morphism.

Since we have defined Conway theories by equations, they form a variety of preiteration theories. We give several more non-trivial equations that hold in Conway theories.

Proposition 12.3 Each Conway theory T satisfies the following identities.

1. (Elgot) Fixed point identity

f^{†} = f · ⟨f^{†}, 1_{p}⟩,

all f : n → n + p. When n = 1, this identity is called the scalar fixed point identity.

2. Left zero identity

(0_{n} ⊕ f)^{†} = f,

all f : n → p. When n = 1, this identity is called the scalar left zero identity.

3. Right zero identity

(f ⊕ 0_{q})^{†} = f^{†} ⊕ 0_{q},

all f : n → n + p. When n = 1, this identity is called the scalar right zero identity.

4. Pairing identity

⟨f, g⟩^{†} = ⟨f^{†} · ⟨h^{†}, 1_{p}⟩, h^{†}⟩,

all f : n → n + m + p, g : m → n + m + p, where

h = g · ⟨f^{†}, 1_{m+p}⟩ : m  [figure] m + p.

5. Permutation identity

(π · f · (π^{−1} ⊕ 1_{p}))^{†} = π · f^{†},

for all f : n → n + p and for all base permutations π : n → n. Here π^{−1} denotes the inverse of π.

(There are several other axiomatizations of Conway theories, see [7].)

13 Iteration Theories

Suppose that G = (G,^{∘}) is a finite group on the set [n]. In each theory T, we associate with G the base morphisms ρ_{i}^{G} : n → n, i ∈ [n], defined by:

j_{n} · ρ_{i}^{G} := (i ^{∘} j)_{n}, all j ∈ [n], i.e.,
ρ_{i}^{G} := ⟨(i ^{∘} 1)_{n}, (i ^{∘} 2)_{n}, …, (i ^{∘} n)_{n}⟩.

¿From now on, we write just ij instead of i ^{∘} j. The morphism (ij)_{n} is the corresponding base morphism 1 → n. The morphisms ρ_{i}^{G}, denoted sometimes just ρ_{i}, are called the base morphisms associated with the group G.

We define a morphism g_{G} : n → n + p for each scalar g : 1 → n + p.

g_{G} := ⟨g · (ρ_{1}^{G} ⊕ 1_{p}), …, g · (ρ_{n}^{G} ⊕ 1_{p})⟩ : n  [figure] n + p,

where τ_{n} : n → 1 is the unique base morphism.

Definition 13.1 The group-identity associated with G is the equation

g_{G}^{†} = τ_{n} · (g · (τ_{n} ⊕ 1_{p}))^{†}, g : 1  [figure] n + p.  (14)

Example 13.2 Suppose that G is the group of order 3. Then the identity associated with G is the equation

⟨f, f · (⟨2_{3}, 3_{3}, 1_{3}⟩ ⊕ 1_{p}), f · (⟨3_{3}, 1_{3}, 2_{3}⟩ ⊕ 1_{p})⟩^{†} = τ_{3} · (f · (τ_{3} ⊕ 1_{p}))^{†},

where f : 1 → 3 + p.

Definition 13.3 An iteration theory is a Conway theory which satisfies all identities associated with finite (simple) groups. A morphism of iteration theories is a preiteration theory morphism.

Free iteration theories are also tree theories.

Let Σ be a signature, and let ⊥ be a letter not in any set Σ_{n}. Σ_{⊥} is the signature obtained from Σ by adding the letter ⊥ to Σ_{0}. In the tree theory Σ_{⊥} tr, 1_{1}^{†} = ⊥.

Theorem 13.4 [7] For any signature Σ, the theory Σ_{⊥} tr of regular Σ_{⊥}- trees is the iteration theory freely generated by Σ; for any iteration theory T and any function h : Σ → T which maps σ ∈ Σ_{n} to a morphism h(σ) : 1 → n in T, all n ≥ 0, there is a unique iteration theory morphism h^{#} : Σ_{⊥} tr → T such that

h(σ) = h^{#}(η(σ)),

for all σ ∈ Σ_{n}, n ≥ 0.

Example 13.5 Let L = (L, ≤) be a complete (or just ω-complete) poset. Let T_{L} denote the theory whose morphisms 1 → n are the continuous (i.e., sup preserving) functions L^{n} → L; the composite of f : 1 → n with ⟨g_{1}, …, g_{n}⟩ : n → p is the function

L^{p} [figure: ⟨g_{1},...,g_{n}⟩]L^{n} [figure: f] L.

For each continuous f : L^{n+p} → L^{n} and each a ∈ L^{p} there is a least b ∈ L^{n} such that b = f(b, a). This b is denoted μb. b = f(b, a). It was shown in several places that T_{L} is an iteration theory, where, for f : n → n + p, (i.e., f : L^{n+p} → L^{n})

f^{†}(a) = μb. b = f(b, a).

There is a number of classes of theories whose identities are captured by the axioms of iteration theories.

Theorem 13.6 [7] An identity holds in all iteration theories iff it holds in all theories T_{L}, for ω-complete posets L.

Other representative classes are theories in which the fixed point operation is a “unique fixed point”, or alternatively, an “initial fixed point”. See [10] for a thorough account.

A sufficient condition that a Conway theory satisfies the group identities is that it satisfies the implication we have called the weak functorial implication. (Actually, there is one such implication for each n ≥ 1.) A preiteration theory satisfies the weak functorial implication if, whenever the square

[figure: 1; 1 + p; g; n; 1; τ_{n}; n; n + p; f; n + p; 1 + p; τ_{n}⊕1_{p}]

commutes, then so does 13 Iteration Theories 51 Here, τ_{n} : n → 1 is the unique base morphism. For example, when L is an ω-complete poset, T_{L} satisfies the weak functorial implication, since

[figure: n; p; f^{†}; n; 1; τ_{n}; p; 1; g]

f^{†} = sup_{k} f^{(k)},

where the powers of f are defined by:

f^{(1)} = f · (⊥_{n} ⊕ 1_{p})
f^{(k+1)} = f · ⟨f^{(k)}, 1_{p}⟩.

Similarly, g^{†} = sup g^{(k)}. But, for each k > 0,

f^{(k)} = τ_{n} · g^{(k)}.

Recent BRICS Report Series Publications

RS-02-19 Stephen L. Bloom and ZoltánÉsik. An Extension Theorem with an Application to Formal Tree Series. April 2002. 51 pp.

RS-02-18 Gerth Stølting Brodal and Rolf Fagerberg. Cache Oblivious Distribution Sweeping. April 2002. To appear in 29th International Colloquium on Automata, Languages, and Programming, ICALP ’02 Proceedings, LNCS, 2002.

RS-02-17 Bolette Ammitzbøll Madsen, Jesper Makholm Nielsen, and Bjarke Skjernaa. On the Number of Maximal Bipartite Subgraphs of a Graph. April 2002. 7 pp.

RS-02-16 Jiří Srba. Strong Bisimilarity of Simple Process Algebras: Complexity Lower Bounds. April 2002. To appear in 29th International Colloquium on Automata, Languages, and Programming, ICALP ’02 Proceedings, LNCS, 2002.

RS-02-15 Jesper Makholm Nielsen. On the Number of Maximal Independent Sets in a Graph. April 2002. 10 pp.

RS-02-14 Ulrich Berger and Paulo B. Oliva. Modified Bar Recursion. April 2002. 23 pp.

RS-02-13 Gerth Stølting Brodal, Rune B. Lyngsø, Anna Östlin, and Christian N. S. Pedersen. Solving the String Statistics Problem in Time O(n log n). March 2002. To appear in 29th International Colloquium on Automata, Languages, and Programming, ICALP ’02 Proceedings, LNCS, 2002.

RS-02-12 Olivier Danvy and Mayer Goldberg. There and Back Again. March 2002. This report supersedes the earlier report BRICS RS-01-39.

RS-02-11 Aske Simon Christensen, Anders Møller, and Michael I. Schwartzbach. Extending Java for High-Level Web Service Construction. March 2002.

RS-02-10 Ulrich Kohlenbach. Uniform Asymptotic Regularity for Mann Iterates. March 2002. 17 pp.

RS-02-9 Anna Östlin and Rasmus Pagh. One-Probe Search. February 2002. 17 pp.

RS-02-8 Ronald Cramer and Serge Fehr. Optimal Black-Box Secret Sharing over Arbitrary Abelian Groups. February 2002. 19 pp.