Theory and Applications of Categories, Vol. 9, No. 9, 2002, pp. 166–197.

THE ALTERNATION HIERARCHY FOR THE THEORY OF μ-LATTICES

LUIGI SANTOCANALE

ABSTRACT. The alternation hierarchy problem asks whether every μ-term ϕ, that is, a term built up also using a least fixed point constructor as well as a greatest fixed point constructor, is equivalent to a μ-term where the number of nested fixed points of a different type is bounded by a constant independent of ϕ. In this paper we give a proof that the alternation hierarchy for the theory of μ-lattices is strict, meaning that such a constant does not exist if μ-terms are built up from the basic lattice operations and are interpreted as expected. The proof relies on the explicit characterization of free μ-lattices by means of games and strategies.

Introduction

The alternation hierarchy problem is at the core of the definition of categories of μ-algebras [17, 18] which we resume as follows. For a given equational theory 𝕋, we let T_{0} be the category of its partially ordered models and order preserving morphisms. Out of T_{0} we can select objects and morphisms so that all the “desired” least prefix-points exist and are preserved, this process giving rise to a category S_{1}. The desired least prefix-points are those needed to have models of an iteration theory [6] where the dagger operation is interpreted as the least prefix-point. If we use, as a selection criterion, the existence of greatest postfix-points and their preservation, we obtain a category P_{1}. If we let T_{1} be the intersection of S_{1} and P_{1}, then T_{1} is a quasivariety and the category of models of a theory 𝕋_{1} which is axiomatized by equational implications. We can repeat the process out of T_{1} and 𝕋_{1} and the iteration of this process leads to the construction of categories S_{n}, P_{n}, T_{n} for arbitrary positive numbers n. The category of μ-𝕋-algebras is defined to be the inverse limit of the corresponding diagram of inclusions; the alternation hierarchy problem asks whether this process stops after a finite number of steps, i.e. whether the category of μ-𝕋-algebras is equivalent to a category among S_{n}, P_{n}, T_{n} for some n ≥ 0. The main contribution presented in this paper is theorem 2.6 stating that the alternation hierarchy for the theory of μ-lattices is strict, i.e. that there is no such number when 𝕋 is the theory of lattices.

The alternation hierarchy for the propositional μ-calculus has recently been shown to be strict in several cases [2, 7, 16]; together with open problems on fix-point free polynomials in free lattices [10], these results have challenged us to consider the hierarchy problem for the theory of μ-lattices; in particular we were interested in understanding whether the explicit characterization of free μ-lattices [19, 20] could be of help.

Research carried out at BRICS, Basic Research in Computer Science, Centre of the Danish National Research Foundation. The author is grateful to André Arnold for useful comments that lead to improve the presentation of these results.

Received by the editors 200 November 10 and, in revised form, 2002 January 27.

Published on 2002 January 31 in the volume of articles from CT2000.

2000 Mathematics Subject Classification: 03D55, 06B25, 91A43.

Key words and phrases: free lattices, free μ-lattices, fixed points, parity games.

\begin{matrix}c \\ ◯ \end{matrix} Luigi Santocanale, 2002. Permission to copy for private use granted.

It is our opinion that μ-algebras are algebraic objects suitable to generalize the role of iteration theories in the context of the theorization of communication and interactive computation. This statement is exemplified by the consideration of free μ-lattices which have been characterized by means of games and strategies. Games for free μ-lattices model bidirectional synchronous communication channels which can be recursively constructed from a few primitives: left and right choices – the lattice operations – and left and right iterations – the least and greatest fixed point operators. If G and H are games for a free μ-lattice, we say that G ≤ H if there exists a winning strategy in a compound game ⟨G, H⟩ for a player whom we call Mediator. Such a strategy can be understood as a protocol for letting the left user of the communication channel G communicate with the right user of H in an asynchronous way. The order theoretic point of view, which we adopt here, identifies two such channels G and H if there are protocols in both directions, i.e. winning strategies for Mediator in both games ⟨G, H⟩ and ⟨H, G⟩. The analysis of different strategies, in the spirit of categorical proof theory and of the bicompletion of categories [12, 13, 14], is probably a more appropriate setting in which to understand communication; this study is under way and suggests a possible characterization of free bicomplete categories with enough initial algebras and terminal coalgebras of functors. However, we can still ask whether the order theoretic identification is degenerate by posing the alternation hierarchy problem; its translation in the language of communication sounds as follows: is every channel equivalent to another one where the number of alternations between left and right iterations is bounded by a fixed positive integer? The negative answer we provide to the order theoretic problem implies also that a categorical identification is not degenerate; moreover the answer depends on a coincidence of order theoretic ideas with categorical ideas. There are games A for which the copycat strategy, which plays the role of the identity, is the unique strategy in the game ⟨A, A⟩; because of that, the asynchronous communication, which is the result of a protocol mediating between the left user of the left channel and the right user of the right channel, has the same dynamics as the communication along the single channel A; therefore it happens to be synchronous and we call these games synchronizing. These games impose strong conditions on the structure of games H equivalent to A; we show that they are hard, i.e. they are good representatives of their equivalence class as far as we are concerned with their alternation complexity.

The ideas presented here have originated from Philip Whitman’s proof that free lattices are not in general complete [24]. It is difficult to relate these ideas to those contained in previous works on the alternation hierarchy for the propositional μ-calculus [2, 3, 7, 8, 16, 18]. The main reason is that the traditional models of this calculus are boolean algebras of sets with modal operators and that the alternation hierarchy for the class of distributive μ-lattices is degenerate, since every distributive lattice is a μ-lattice. In particular, the main theorem presented in this paper cannot be derived from those results, at least not in a straightforward way. Existing techniques for proving hardness of a μcalculus formula, as summarized in [2], are diagonalization arguments and rely on the presence of the boolean complement; they cannot be applied in the context of μ-lattices. However, our technique is also a sort of a diagonalization argument, but of a categorical flavor. An analogous technique for the propositional μ-calculus would go through the explicit characterization of the order relation by means of refutations [22]. Other works [1, 5, 15] have studied the structure of games as models of linear logic. With respect to those works, the focus is here on the algebraic structure imposed by fix-points instead of the algebraic structure imposed by the multiplicative connectives of linear logic.

The paper is structured as follows. In section 1 we present definitions of key concepts and introduce the notation we shall use. In section 2 we present μ-lattices and the alternation hierarchy problem; we sketch the general strategy used to answer the problem. In section 3 we review the structure of free μ-lattices in view of the hierarchy; for the sake of completeness, we present once more the proof that the preorder relation on games is transitive. In section 4 we define synchronizing games and prove their hardness. In section 5 we construct synchronizing games of arbitrary complexity.

1. Notation and useful definitions

1.1. Least and greatest fix-points. Let P be a partially ordered set and let ϕ : P ^{}P be an order preserving function. The least prefix-point of ϕ, whenever it exists, is an element μ_{z}.ϕ(z) of P such that ϕ( μ_{z}.ϕ(z) ) ≤ μ_{z}.ϕ(z) and such that, if ϕ( p) ≤ p, then μ_{z}.ϕ(z) ≤ p. The greatest postfix-point of ϕ is defined dually and is denoted by ν_{z}.ϕ(z). Least prefix-point and greatest postfix-point are Conway operators in the sense of [6]. A summary of their properties can be found in [17].

1.2. Pointed graphs and trees with back edges. By a graph G we mean a tuple ⟨G_{0}, G_{1}, dom , cod ⟩, where G_{0} is a set (of vertexes or states), G_{1} is a set (of directed edges or transitions) and dom , cod : G_{1} ^{}G_{0} are functions. By a morphism of graphs f : G ^{}H we mean a pair of functions f_{i} : G_{i} ^{}H_{i}, i = 0, 1, such that f_{0} ∘ dom = dom ∘ f_{1} and f_{0} ∘ cod = cod ∘ f_{1}. We often write a graph as a pair ⟨G_{0}, G_{1}⟩ and leave in the background the functions dom , cod . If G_{1} ⊆ G_{0} × G_{0}, we assume that dom and cod are the restrictions of the projections to G_{1}.

Let G = ⟨G_{0}, G_{1}⟩ be a graph, a path γ in G is a morphism of graphs γ : n̂ ^{}G where n̂ is the graph 0 → 1 → … → n. The length of γ, denoted |γ|, is defined to be n. We set dom γ = γ(0) and cod γ = γ(|γ|). Paths γ_{1}, γ_{2} can be composed in the usual way, provided that cod γ_{1} = dom γ_{2}, and we write γ_{1} ⋆ γ_{2} for their composition; if g ∈ G_{0} we write 1_{g} for the unique path γ such that |γ| = 0 and dom γ = g = cod γ. A category F (G), free over G, is defined in this way. Let G, H be graphs and let f : G ^{}F (H) be a morphism of graphs, we say that f is non-decreasing if |f(τ)| ≤ 1 for every τ ∈ G_{1}. The morphism of graphs f is non-decreasing if and only if its extension f : F (G) ^{}F (H) to a functor is convex, i.e. if f(γ) = δ_{1} ⋆ δ_{2}, then we can find γ_{1}, γ_{2} such that f(γ_{i}) = δ_{i}, i = 1, 2, and γ = γ_{1} ⋆ γ_{2}. We say that a path γ in G visits a vertex g ∈ G_{0}, or equivalently that g lies on γ, if there exists i ∈ {0, …, |γ|} such that γ(i) = g. We say that a path γ is simple if it does not visit a node twice, i.e. if γ_{0} is injective as a function. We say that γ is a cycle if dom γ = cod γ and that γ is proper if |γ| > 0.

A pointed graph is a tuple ⟨G_{0}, G_{1}, g_{0}⟩ such that ⟨G_{0}, G_{1}⟩ is a graph and g_{0} ∈ G_{0}; we shall say that g_{0} is the root of ⟨G_{0}, G_{1}, g_{0}⟩. A morphism of pointed graphs f : G ^{}H is a morphism of graphs f : ⟨G_{0}, G_{1}⟩ ^{}⟨H_{0}, H_{1}⟩ such that f_{0}(g_{0}) = h_{0}. An infinite path in G is a morphism of graphs γ : ω̂ ^{}G where ω̂ is the graph 0 → 1 → … → n → . . .. Since the pointed graph ⟨ω̂, 0⟩ is the inductive limit of the pointed graphs ⟨n̂, 0⟩, we shall often identify an infinite path γ with the set {γ_{n}}_{n≥0} of prefixes of γ of finite length. On the other hand, if {γ_{n}}_{n≥0} is a set of paths such that |γ_{n}| = n and γ_{n+1} = γ_{n} ⋆ τ_{n+1}, we shall use that same notation {γ_{n}}_{n≥0} to denote the infinite path which associates to the transition n → n + 1 of ω̂ the transition τ_{n+1}. A pointed graph ⟨G_{0}, G_{1}, g_{0}⟩ is said to be reachable if for every g ∈ G_{0} there exists a path γ such that dom γ = g_{0} and cod γ = g. Let G be a graph and let g_{0} ∈ G_{0}, we denote by \overline{G, g_{0}} the greatest subgraph H of G such that ⟨H, g_{0}⟩ is reachable.

1.3. Definition. A tree with back edges is a pointed graph ⟨G_{0}, G_{1}, g_{0}⟩ such that G_{1} ⊆ G_{0} × G_{0} and with the property that, for every vertex g ∈ G_{0}, there exists a unique simple path γ_{g} from g_{0} to g. In this case, we say that an edge τ : g → g′ is a forward edge if γ_{g} ⋆ τ = γ_{g′} and that it is a back edge otherwise.

To give a tree with back edges is equivalent to giving the pair ⟨⟨G_{0}, F, g_{0}⟩, B⟩, where F is the set of forward edges and B is the set of back edges. Then ⟨G_{0}, F, g_{0}⟩ is a tree, i.e. a pointed graph such that, for every vertex g ∈ G_{0}, there exists a unique path from g_{0} to g; moreover, if g → g′ is an edge belonging to B, then g′ is an ancestor of g in the tree ⟨G_{0}, F, g_{0}⟩. We can specify a tree with back edges by giving a pair ⟨T, B⟩, where T = ⟨T_{0}, T_{1}, t_{0}⟩ is a tree and B ⊆ T_{0} × T_{0} is a set of pairs with the above property.

Let ⟨T, B⟩ be a finite tree with back edges. A vertex r ∈ T_{0} is called a return if there exists a back edge t → r. Observe that, for an infinite path γ in ⟨T, B⟩, there exists a unique return r_{γ} which is visited infinitely often and which is of minimal height. The height of a vertex in ⟨T, B⟩ is the length of the unique simple path from the root to the vertex. Similarly, for every proper cycle γ in ⟨T, B⟩, there exists a unique return r_{γ} of minimal height lying on γ. A vertex x ∈ T_{0} is said to be a leaf if it is a leaf of T in the usual sense and there are no back edges from x; this can be summarized by saying that { g′ | x → g′ } is empty. There is an operation of substitution of a tree with back edges for a leaf induced by the analogous operations on trees. Let x be a leaf of ⟨T_{1}, B_{1}⟩, we define:

⟨T_{1}, B_{1}⟩[⟨T_{2}, B_{2}⟩/x] = ⟨T_{1}[T_{2}/x], B_{1} + B_{2}⟩.

If ⟨T, B⟩ is a tree with back edges and t ∈ T_{0}, we say that t is a complete vertex if for every descendant t′ of t and every back edge t′ → r, r is also a descendant of t. If t is a complete vertex, we can define trees with back edges T_{↓}^{t} and T_{t}^{↓} so that t is a leaf of T_{t}^{↓}, t is the root of T_{↓}^{t}, and moreover T = T_{t}^{↓}[T_{↓}^{t}/t]. Indeed, let T_{1} = \overline{T, t} and T_{2} = \overline{T′, t_{0}}, where T′_{0} = T_{0} and T′_{1} = T_{1} \ { τ | dom τ = t }; define then T_{↓}^{t} as ⟨T_{1}, B|_{T_{1}}⟩ and T_{t}^{↓} as ⟨T_{2}, B|_{T_{2}}⟩. A return r is said to be minimal if there are no other returns on the path γ_{r} from the root to r. A minimal return is easily seen to be a complete vertex.

1.4. Games and strategies.

1.5. Definition. A partial game is a tuple G = ⟨G_{0}, G_{1}, g_{0}, ϵ, W_{σ}⟩ where ⟨G_{0}, G_{1}⟩ is a graph, g_{0} ∈ G_{0}, ϵ : G_{0} ^{}{0, σ, π} is a coloring, and W_{σ} is a set of infinite paths in ⟨G_{0}, G_{1}⟩. We require that if ϵ(g) = 0, then { g′ | g → g′ } = ∅.

The above data must be interpreted as follows: G_{0} is the set of positions of G, g_{0} is the initial position and G_{1} is the set of possible moves. For a position g ∈ G_{0}, if ϵ(g) = σ, then it is player σ who must move, if ϵ(g) = π, it is π’s turn to move. A position g ∈ G_{0} is final if there are no possible moves from g, i.e. if { g′ | g → g′ } = ∅. In this case, if ϵ(g) = σ, then player σ loses, if ϵ(g) = π, then player π loses, if ϵ(g) = 0, then g is a draw and we call g a partial final position. We shall write X_{G} for the set { x ∈ G_{0} | ϵ(x) = 0 } of partial final positions of G. Finally, W_{σ} is the set of infinite plays which are wins for player σ. We define W_{π} to be the complement of W_{σ}; we assume that there are no “infinite draws” so that W_{π} is meant to be the set of infinite plays which are wins for player π. A game is a partial game G such that X_{G} = ∅. We shall say that a partial game is bipartite if ϵ(g) ≠ ϵ(g′) for every move g → g′.

In the definitions below, G will be a fixed a partial game as defined in 1.5.

1.6. Definition. A winning strategy for player σ in G is a non empty set S of paths in G satisfying the following properties:

• γ ∈ S implies dom γ = g_{0},

• γ_{1} ⋆ γ_{2} ∈ S implies γ_{1} ∈ S,

• if γ ∈ S and ϵ(cod γ) = π, then γ ⋆ τ ∈ S for every τ ∈ G_{1} such that dom τ = cod γ,

• if γ ∈ S and ϵ(cod γ) = σ, then there exists τ ∈ G_{1} such that dom τ = cod γ and γ ⋆ τ ∈ S,

• if γ is an infinite path in G such that for every n ≥ 0 the prefix of γ of length n belongs to S, then γ belongs to W_{σ}.

A strategy for player σ in G is a nonempty set S of paths in G such that the first three properties hold. Let γ be a path in G, we say that γ has been played according to the strategy S if there exists a path γ_{0} such that γ_{0} ⋆ γ ∈ S.

1.7. Definition. A bounded memory winning strategy for player σ in G is a pair (S, ψ), where S = ⟨S_{0}, S_{1}, s_{0}⟩ is a finite reachable pointed graph and ψ : S ^{}⟨G_{0}, G_{1}, g_{0}⟩ is a morphism of pointed graphs. The following properties hold:

• If s ∈ S_{0} and ϵ(ψ(s)) = π, then for every τ ∈ G_{1} such that dom τ = ψ(s) there exists a transition τ′ ∈ S_{1} such that dom τ′ = s and ψ(τ′) = τ,

Theory and Applications of Categories, Vol. 9, No. 9 171

• if s ∈ S and ϵ(ψ(s)) = σ, then there exists τ′ ∈ S_{1} such that dom τ′ = s,

• if γ is an infinite path in S, then ψ ∘ γ ∈ W_{σ}. 1.8. Lemma. Let (S, ψ) be a bounded memory winning strategy for player σ. Then the set of paths

ψS = { ψ ∘ γ | γ is a path in S and dom γ = s_{0} }

is a winning strategy for player σ as defined in 1.6.

2. The theory of μ-lattices and the hierarchy

We begin by defining μ-lattices and the hierarchy. We shall later give an equivalent but more combinatorial definition of μ-lattices using partial games. This approach will allow us to have a combinatorial grasp on the hierarchy. 2.1. Definition. The set of terms Λ_{ω} and the arity-function a : Λ_{ω} ^{}ℕ are defined by induction as follows:

1. ⋀_{k} ∈ Λ_{ω} and a(⋀_{k}) = k, for k ≥ 0.

2. ⋁_{k} ∈ Λ_{ω} and a(⋁_{k}) = k, for k ≥ 0.

3. If ϕ ∈ Λ_{ω}, a(ϕ) = k, and ϕ_{i} ∈ Λ_{ω} for i = 1, …, k, then ϕ ∘ (ϕ_{1}, …, ϕ_{k}) ∈ Λ_{ω} and a(ϕ ∘ (ϕ_{1}, …, ϕ_{k})) = ∑_{i=1,...,k} a(ϕ_{i}).

4. If ϕ ∈ Λ_{ω}, a(ϕ) = k + 1, then μ_{s}.ϕ ∈ Λ_{ω} and a(μ_{s}.ϕ) = k, for s = 1, …, k + 1.

5. If ϕ ∈ Λ_{ω}, a(ϕ) = k + 1, then ν_{s}.ϕ ∈ Λ_{ω} and a(ν_{s}.ϕ) = k, for s = 1, …, k + 1. 2.2. Definition. Let L be a lattice, we define a partial interpretation of terms ϕ ∈ Λ_{ω}, a(ϕ) = k, as order preserving functions |ϕ| : L^{k} ^{}L.

1. | ⋀_{k} |(l_{1}, …, l_{k}) = ⋀_{i=1,...,k} l_{i} .

2. As in 1, but substituting each symbol ⋀ with the symbol ⋁.

3. Let ϕ ∈ Λ_{ω}, a(ϕ) = k, and let ϕ_{i} ∈ Λ_{ω} for i = 1, …, k. Suppose |ϕ| and |ϕ_{i}| are

defined. In this case we define |ϕ ∘ (ϕ_{1}, …, ϕ_{k})| to be:

|ϕ ∘ (ϕ_{1}, …, ϕ_{k})|(l_{1}, …, l_{h})
= |ϕ|( |ϕ_{1}|(l_{h_{1}^{−}}, …, l_{h_{1}^{+}}), …, |ϕ_{k}|(l_{h_{k}^{−}}, …, l_{h_{k}^{+}}) ) ,

where h_{i}^{−} = 1 + ∑_{j=1}^{i−1} a(ϕ_{j}), h_{i}^{+} = ∑_{j=1}^{i} a(ϕ_{j}) and h = h_{k}^{+} = ∑_{j=1}^{k} a(ϕ_{j}). Otherwise |ϕ ∘ (ϕ_{1}, …, ϕ_{k})| is undefined.

4. Let ϕ ∈ Λ_{ω} be such that a(ϕ) = k + 1. Suppose that |ϕ| is defined and let s ∈ {1, …, k + 1}. If for each vector (l_{1}, …, l_{k}) ∈ L^{k} the least prefix-point of the order preserving function |ϕ|(l_{1}, …, l_{s−1}, z, l_{s}, …, l_{k}) exists, then we define |μ_{s}.ϕ| to be:

|μ_{s}.ϕ|(l_{1}, …, l_{k}) = μ_{z}.|ϕ|(l_{1}, …, l_{s−1}, z, l_{s}, …, l_{k}) .

Otherwise |μ_{s}.ϕ| is undefined.

5. As in 4, but substituting each symbol μ with the symbol ν, and the word least prefixpoint with the word greatest postfix-point.

2.3. Definition. A lattice L is a μ-lattice if the interpretation of terms ϕ ∈ Λ_{ω} is a total function. Let L_{1}, L_{2} be two μ-lattices. An order preserving function f : L_{1} ^{}L_{2} is a μ-lattice morphism if the equality |ϕ| ∘ f^{a(ϕ)} = f ∘ |ϕ| holds for all ϕ ∈ Λ_{ω}. We shall write L_{ω} for the category of μ-lattices.

2.4. Definition. We define classes of terms Σ_{n}, Π_{n}, Λ_{n} ⊆ Λ_{ω}, for n ≥ 0. We set Σ_{0} = Π_{0} = Λ_{0}, where Λ_{0} is the least class which contains ⋁_{k} and ⋀_{k}, k ≥ 0, and which is closed under substitution (rule 3 of definition 2.1). Suppose that Σ_{n} and Π_{n} have been defined. We define Σ_{n+1} to be the least class of terms which contains Σ_{n} ∪ Π_{n} and which is closed under substitution and the μ-operation (rule 4 of definition 2.1). Similarly, we define Π_{n+1} to be the least class of terms which contains Σ_{n}∪Π_{n} and which is closed under substitution and the ν-operation (rule 5 of definition 2.1). We let Λ_{n} = Π_{n+1} ∩ Σ_{n+1} and observe that Λ_{ω} = ⋃_{n≥0} Σ_{n} = ⋃_{n≥0} Π_{n} = ⋃_{n≥0} Λ_{n}.

2.5. Definition. We say that a lattice is a Σ_{n}-model if for every ϕ ∈ Σ_{n} |ϕ| : L^{a(ϕ)} ^{}L is defined. Let L_{1}, L_{2} be two Σ_{n}-models, an order preserving function f : L_{1} ^{}L_{2} is a morphism of Σ_{n}-models if for every ϕ ∈ Σ_{n} the equality f ∘ |ϕ| = |ϕ| ∘ f^{a(ϕ)} holds. We let S_{n} be the category of Σ_{n}-models and morphisms of Σ_{n}-models. We define in a similar way a Π_{n}-model, a morphism of Π_{n}-models and the category P_{n}, a Λ_{n}-model, a morphism of Λ_{n}-models and the category L_{n}.

Clearly L_{0} is the category of lattices and we have inclusion of categories

[figure: L_{0}; S_{1}; P_{1}; L_{1}; …; L_{n−1}; S_{n}; P_{n}; L_{n}; …; L_{ω}]

The alternation hierarchy problem for the theory of μ-lattices can be stated in the following way: is there a number n ≥ 0 such that every term ϕ ∈ Λ_{ω} is equivalent to a term ϕ′ ∈ Λ_{n}? Two terms are considered to be equivalent if they have the same arity and their interpretations are equal in every μ-lattice. This question can be equivalently formulated as follows: is there a number n ≥ 0 and a category C_{n} among S_{n}, P_{n}, L_{n} such that the inclusion functor L_{ω} ^{⊂} ^{}C_{n} is an equivalence of categories? If such a C_{n} exists, then C_{n} = L_{ω}, since if P is a partially ordered set which is order-isomorphic to a μ-lattice, then it is itself a μ-lattice; as a consequence for every m > n all the S_{m}, P_{m} and L_{m} are equal to L_{ω}.

2.6. Theorem. The alternation hierarchy for the theory of μ-lattices is strict, i.e. there is no positive integer n such that L_{n} = L_{ω}.

Proof. For every n ≥ 0, we exhibit in 3.12 a sub-Λ_{n}-model J_{n,P} of the free μ-lattice J_{P} over the partially ordered set P. The Λ_{n}-model J_{n,P} is the free Λ_{n}-model over the partially ordered set P, in particular it is generated by P and the inclusion i_{n,P} : J_{n,P} ^{⊂} ^{}J_{P} preserves the generators. If L_{n} = L_{ω}, then i_{n,P} has to be an isomorphism; however, we show in 5.2 that i_{n,P} is a proper inclusion for every n ≥ 0 if P contains an antichain of cardinality six.

The alternation hierarchy problem for a class K of μ-lattices can be stated as follows. Let \overline{K}_{ω} be the quasi-variety generated by the class of μ-lattices K in L_{ω}, by which we mean the closure of the full sub-category determined by objects in K under products, subobjects and regular epis. Similarly let \overline{K}_{n} be the quasi-variety generated by the class K in L_{n}. The inclusion functors L_{ω} ^{⊂} ^{}L_{n} restrict to inclusions \overline{K}_{ω} ^{⊂} ^{}\overline{K_{n}} and the problem is to determine whether there exists a number n ≥ 0 such that the above inclusion is an equivalence. The above theorem has the following consequence.

2.7. Theorem. The alternation hierarchy for the class of complete lattices is strict.

Proof. Let K be the class of complete lattices. Since every free μ-lattice can be embedded in a complete lattice by a morphism of μ-lattices, as proved in [19, 20], then \overline{K}_{ω} = L_{ω}. Similarly \overline{K}_{n} = L_{n}, since J_{n,P} is the free Λ_{n}-model, so that free Λ_{n}-models can be embedded into complete lattices. However L_{n} ≠ L_{ω}.

The theory of μ-lattices has an equivalent presentation by means of a class J of partial games, cf. 1.5, which are a sort of combinatorial terms. A partial game G in this class always comes with its set of partial final positions X_{G}; given a lattice L we can define the partial interpretation of games G ∈ J as order preserving functions |G| : L^{X_{G}} ^{}L. A lattice L turns out to be a μ-lattice if and only if the interpretation of a partial game G ∈ J is always defined.

2.8. Definition. A partial game G is in the class L if and only if ⟨G_{0}, G_{1}, g_{0}⟩ is a finite tree with back edges and moreover γ ∈ W_{σ} if and only if ϵ(r_{γ}) = π. If G ∈ L, we denote by R(G) the set of positions which are returns of ⟨G_{0}, G_{1}, g_{0}⟩ and by χ(G) the number card G_{0} + card R(G).

When specifying a partial game G ∈ L we shall omit the set W_{σ}, since this is determined by the underlying tree with back edges and the coloring ϵ.

2.9. Definition. On the class L the following constants and operations are defined.

0. x is the partial game with just one partial final position, which we again call x.

1. Let I be a finite set, the partial game ⋀_{I} has starting position ∧_{0} ∉ I, ϵ(∧_{0}) = π, partial final positions i and moves ∧_{0} → i for every i ∈ I.

2. Let I be a finite set, the partial game ⋁_{I} is defined in a similar way: it has starting position ∨_{0} ∉ I, ϵ(∨_{0}) = σ, partial final positions i and moves ∨_{0} → i for every i ∈ I.

3. Substitution. Let G and H be partial games in L and let x ∈ X_{G}. The underlying pointed graph of the game G[H/x] is obtained by substitution of the tree with back edges underlying H for x in the tree with back edges underlying G. The coloring ϵ is defined accordingly, i.e. if g ≠ x is a position coming from G_{0}, then ϵ(g) is as in G, otherwise, for a position h coming from H_{0}, ϵ(h) is as in H.

4. μ-operation. Let G ∈ L be a partial game and let x ∈ X_{G}. The underlying graph of the game μ_{x}.G[x] is the same as the underlying graph of G with one more move x → g_{0}. The initial position of μ_{x}.G[x] is x and we let ϵ(x) = σ.

5. ν-operation. Let G ∈ L be a partial game and let x ∈ X_{G}. The underlying pointed graph of ν_{x}.G[x] is the same as the underlying graph of μ_{x}.G[x], however we let ϵ(x) = π.

It is useful to have a picture of these operations.

0. The game x is

[figure: x]

1. 2. Let I = {i_{1}, …, i_{n}} be a finite set. The games ⋀_{I} and ⋁_{I} are:

[figure: π; i_{1}; i_{2}; …; i_{n}; σ; i_{1}; i_{2}; …; i_{n}]

3. Let G, H be partial games in L and let x ∈ X_{G}. We represent those games as:

[figure: G; x; H]

The game G[H/x] can be represented as:

[figure: G; H]

4. 5. Let G be a partial game in L and let x ∈ X_{G}. This game can be represented as above. We represent the games μ_{x}.G[x] and ν_{x}.G[x] as:

[figure: σ; G; π; G]

2.10. Definition. We let J be the class of games G ∈ L for which the following two conditions hold, for every r ∈ R(G):

1. there exists a unique back edge P (r) → r,

2. there exists a unique move r → S(r).

We let K be the class of games G ∈ L for which only the first of the two conditions above holds, for any r ∈ R(G).

We have the inclusion of classes J ⊆ K ⊆ L, but those classes are essentially the same. A more detailed account of the equivalence between J and K is given in the proof of theorem 4.2.

We shall write G = H if G, H are partial games and there exists an isomorphism of structure between them. This means that there exists an isomorphism of the underlying pointed graphs f : ⟨G_{0}, G_{1}, g_{0}⟩ ^{}⟨H_{0}, H_{1}, h_{0}⟩ such that ϵ_{G} = ϵ_{H} ∘ f_{0} and such that γ ∈ W_{σ}_{G} if and only if f ∘ γ ∈ W_{σ}_{H}. Substitution satisfies the commutativity rule (G[H/x])[K/y] = (G[K/y])[H/x] if x, y ∈ X_{G} and x ≠ y. Hence if { H_{x} }_{x∈X_{G}} is a collection of games in L, we shall write by G[ H_{x}/x]_{x∈X_{G}} for any sequence of substitutions.

2.11. Remark. It is possible to show that the class J is the least subclass of L which is closed under the constants and the operations of definition 2.9. Indeed, a stronger result holds: a partial game G ∈ J has a unique form x, ⋀_{I}[H_{i}/i]_{i∈I}, ⋁_{I}[H_{i}/i]_{i∈I}, μ_{x}.H[x], ν_{x}.H[x], where H or the H_{i} satisfy χ(H) < χ(G) and χ(H_{i}) < χ(G). Hence, in what follows, we shall be able to define by induction on the structure of partial games in J.

In a similar way we define a partial interpretation for games in J.

2.12. Definition. Let L be a lattice. We define an interpretation of partial games G ∈ J as order preserving functions |G| : L^{X_{G}} ^{}L. The correspondence sending G to |G| is in general only a partial function, i.e. |G| could be undefined for some G.

0. Let G = x so that X_{G} = {x}. We let |G|(λ) = λ(x).

1. Let G = ⋀_{I}[H_{i}/i]_{i∈I}, so that X_{G} = ∑_{i∈I} X_{H_{i}}. If the { |H_{i}| }_{i∈I} are defined, then we define

|G|(λ) = ⋀_{i∈I} |H_{i}|(λ_{H_{i}}) ,

where λ_{H_{i}} is the restriction of λ to X_{H_{i}}. Otherwise |G| is undefined.

2. As in 1, but substituting each symbol ⋀ with the symbol ⋁.

4. Let G = μ_{x}.H[x] so that X_{H} = X_{G} ∪ {x}. If |H| is defined and if also for each collection λ ∈ L^{X_{G}} there exists the least prefix-point of the unary order preserving function

ϕ( l) = |H|(λ^{l}) ,

where λ^{l}(y) = λ(y) if y ≠ x and λ^{l}(x) = l, then we define

|G|(λ) = μ_{z}.ϕ( z) .

Otherwise |G| is undefined.

5. As in 4, but substituting each symbol μ with the symbol ν, and the word least prefixpoint with the word greatest postfix-point.

2.13. Proposition. A lattice L is a μ-lattice if and only if |G| is defined on L for every game G ∈ J. An order preserving function f : L_{1} ^{}L_{2} is a μ-lattice morphism if for all G ∈ J we have f ∘ |G| = |G| ∘ f^{X_{G}}, i.e.

f( |G|(λ) ) = |G|( f ∘ λ) ,

for every λ ∈ L_{1}^{X_{G}}.

Proof. Using the correspondence between the rules of definition 2.1 and the operations defined in 2.9, inductively define for each ϕ ∈ Λ_{ω} a pair ⟨G_{ϕ}, λ_{ϕ}⟩ where G_{ϕ} ∈ J and λ_{ϕ} : a(ϕ) ^{}X_{G_{ϕ}} is a bijection, with the following property: for each lattice L, G_{ϕ} is defined on L if and only if ϕ is defined and moreover

|ϕ|(λ) = |G_{ϕ}|(λ ∘ λ_{ϕ}) .

This shows that if L is a lattice such that |G| is defined on L for every G ∈ J, then L is a μ-lattice. The above formula shows that if f preserves the interpretation of games, then it is a μ-lattice morphism:

f ∘ |ϕ|(λ) = f ∘ |G_{ϕ}|(λ ∘ λ_{ϕ})
= |G_{ϕ}|(f ∘ λ ∘ λ_{ϕ})
= |ϕ|(f ∘ λ) .

On the other hand, assign to each G ∈ J a pair ⟨ϕ_{G}, λ_{G}⟩ where ϕ_{G} ∈ Λ_{ω} and λ_{G} : a(ϕ_{G}) ^{}X_{G} is a bijection, so that for each lattice L, |ϕ_{G}| is defined on L if and only if |G| is defined on L; moreover

|ϕ_{G}|(λ) = |G|(λ ∘ λ_{G}) .

This is done by induction on the structure of games in J, cf. 2.11. The game x is sent to ⋀_{1}, the game ⋀_{I}[G_{i}/i]_{i∈I} is sent to ⋀_{k} ∘(ϕ_{G_{ψ(1)}}, …, ϕ_{G_{ψ(k)}}), where ψ : k ^{}I is a bijection, and μ_{x}.G[x] is sent to μ_{s}.ϕ_{G} where s = λ_{G}^{−1}(x). Similar definitions are given for games of the form ⋁_{I}[G_{i}/i]_{i∈I} and ν_{x}.G[x].

The above assignment shows that if L is a μ-lattice, i.e. if for each ϕ ∈ Λ_{ω} |ϕ| is defined on L, then for every G ∈ J |G| is defined on L too. A morphism which preserves the interpretation of terms will also preserve the interpretation of games:

f ∘ |G|(λ) = f ∘ |ϕ_{G}|(λ ∘ λ_{G}^{−1})
= |ϕ_{G}|(f ∘ λ ∘ λ_{G}^{−1})
= |G|(f ∘ λ) .

2.14. Definition. We define by induction classes of partial games S_{n}, P_{n}, L_{n}, for n ≥ 0. We set S_{0} = P_{0} = L_{0}, where L_{0} is the least class which contains x, ⋁_{I} and ⋀_{I}, where I is a finite set, and which is closed under substitution. Suppose that S_{n} and P_{n} have been defined. We define S_{n+1} to be the least class of games which contains S_{n} ∪ P_{n} and which is closed under substitution and the μ-operation. Similarly, we define P_{n+1} to be the least class of games which contains S_{n} ∪ P_{n} and which is closed under substitution and the νoperation. We let L_{n} = S_{n+1}∩P_{n+1} and observe that J = ⋃_{n≥0} S_{n} = ⋃_{n≥0} P_{n} = ⋃_{n≥0} L_{n}.

2.15. Proposition. A lattice is a Σ_{n}-model if and only if for every G ∈ S_{n} |G| : L^{X_{G}} ^{}L is defined. Let L_{1}, L_{2} be two Σ_{n}-models, an order preserving function f : L_{1} ^{}L_{2} is a morphism of Σ_{n}-models if and only if for every G ∈ S_{n} we have f ∘ |G| = |G| ∘ f^{X_{G}}. Analogous results hold for the classes P_{n} and L_{n}, Π_{n}-models, and Λ_{n}-models, Π_{n}-morphisms and Λ_{n}-morphisms, respectively.

Proof. The transformation of terms into partial games ϕ ^{}⟨G_{ϕ}, λ_{ϕ}⟩, which we defined in the proof of proposition 2.13, restricts to a transformation Σ_{n} ^{}S_{n}, so that if G is defined on L for every G ∈ S_{n}, then L is a Σ_{n}-model, and a lattice morphism which preserves the interpretation of every partial game in S_{n} is a morphism of Σ_{n}-models.

In a similar way the transformation G ^{}⟨ϕ_{G}, λ_{G}⟩ carries partial games in S_{n} into terms in Σ_{n}.

In the rest of this section we give a combinatorial characterization of the classes S_{n}, P_{n}, L_{n}.

2.16. Definition. Let G ∈ L. A chain C in G is a totally ordered subset {r_{0} < … < r_{k}} ⊆ R(G) such that:

1. ϵ(r_{i}) ≠ ϵ(r_{i+1}), for i = 0, …, k − 1,

2. for i = 0, …, k − 1, there is a cycle γ of G such that r_{γ} = r_{i} and r_{i+1} lies on γ.

We say that C is a σ-chain if ϵ(r_{0}) = σ, otherwise we say that C is a π-chain. We shall write C ⊏ G if C is a chain in G, C ⊏_{σ} G if C is σ-chain in G and C ⊏_{π} G if C is a π-chain in G.

2.17. Definition. Let G ∈ L, we define

L(G) = max{ card C | C ⊏ G } ,
L_{σ}(G) = max{ card C | C ⊏_{σ} G } ,
L_{π}(G) = max{ card C | C ⊏_{π} G } .

For every n ≥ 0, we define the class L_{n} ⊆ J by saying that G ∈ L_{n} if and only if L(G) ≤ n. We let S_{0} = P_{0} = L_{0}. For every n ≥ 1 we define the classes S_{n}, P_{n} by saying that

G ∈ S_{n} if and only if L_{σ}(G) ≤ n and L_{π}(G) ≤ n − 1 ,
G ∈ P_{n} if and only if L_{σ}(G) ≤ n − 1 and L_{π}(G) ≤ n .

2.18. Proposition. We have equalities L_{n} = L_{n}, for n ≥ 0 and S_{n} = S_{n}, P_{n} = S_{n}, for n ≥ 1.

Proof. We prove the proposition for n = 0. Observe that G ∈ L_{0} if and only if every chain has cardinality less or equal to 0, i.e. the only chain is the empty set. This happens if and only if there are no returns in G, since a return r gives rise to a chain {r}. It is clear that G ∈ L_{0} if and only if R(G) = ∅.

Suppose that S_{n} = S_{n} and that P_{n} = P_{n}.

We shall show first that S_{n} ∪ P_{n} ⊆ S_{n+1} and that S_{n+1} is closed under substitution and the μ-operation.

It is clear from the definition that S_{n} ∪ P_{n} ⊆ S_{n+1}, so that S_{n} ∪ P_{n} ⊆ S_{n+1}. The class S_{n+1} is closed under substitution: every chain in G[H/x] is either a chain from G[x] or a chain of H, since if g ∈ G_{0} and h ∈ H_{0}, then there is no cycle γ of G[H/x] on which both g and h lie. It is also closed under the μ-operation. Let G[x] be in S_{n+1} and let C = {r_{0}, …, r_{k}} be a chain in μ_{x}.G[x]. Observe first that if r_{0} ≠ x then {r_{0}, …, r_{k}} is also a chain of G[x]. This is because a cycle γ_{i} such that r_{γ_{i}} = r_{i} does not contain the transition x → S(x), otherwise r_{γ_{i}} = x. If C is a π-chain, then r_{0} ≠ x so that C is a π-chain of G[x] and card C ≤ n. If C is a σ-chain, we distinguish two cases: either r_{0} ≠ x, so that C is also a chain of G[x] and card C ≤ n + 1; or r_{0} = x, then {r_{1}, …, r_{k}} is a π-chain in G[x], so that k ≤ L_{π}(G[x]) ≤ n and card C = k + 1 ≤ n + 1.

We shall now prove that if C ⊆ J is a class such that S_{n} ∪ P_{n} ⊆ C which is also closed under substitution and the μ-operation, then S_{n+1} ⊆ C. If G ∈ S_{n+1} we let ζ(G) be the number

card { C ⊏_{σ} G | card C = n + 1},

and prove that G ∈ C by induction on ζ(G).

Suppose that ζ(G) = 0. Then all chains of G have cardinality less than n so that G ∈ L_{n}.

2.19. Lemma. The class L_{n} is the closure under substitution of S_{n} ∪ P_{n}.

Proof. Let G ∈ L_{n} be a given partial game. If we can find a return r which is a complete vertex distinct from the root, then we can write G = G_{r}^{↓}[G_{↓}^{r}/r] and deduce that G belongs to the closure of S_{n} ∪P_{n} under substitution by the inductive hypothesis that this property holds for both G_{r}^{↓} and G_{↓}^{r}. If this is not possible, then we claim that every return of G lies on the same strongly connected component. To justify the claim, we argue that if r is a return of G, then we can find a path from r to the root, and therefore we can construct a cycle on which both r and the root lie. Either r is the root itself, or else we can find a path δ_{1} from r to a return r′ ≠ r which lies on γ_{r}, since r is not a complete vertex; we can compose δ_{1} with a path δ_{2} from r′ to the root – we can suppose that δ_{2} exists, since the height of r′ is strictly less than the height of r – to obtain the desired path.

Thus, in order to prove the lemma, it is enough to observe that if G ∈ L is such that L(G) = n and every return of G lies on the same strongly connected component, then G ∈ S_{n} ∪ P_{n}. Suppose we can find a σ-chain {r_{0}, …, r_{n−1}} as well as a π-chain {r′_{0}, …, r′_{n−1}} in G, both of cardinality n. Choose a cycle γ on which both r_{0}, r′_{0} lie. If ϵ(r_{γ}) = π, then {r_{γ}, r_{0}, …, r_{n−1}} is a π-chain of cardinality n + 1. If ϵ(r_{γ}) = σ, then {r_{γ}, r′_{0}, …, r′_{n−1}} is a σ-chain of cardinality n + 1. This contradicts the hypothesis that G ∈ L_{n}.

Using the lemma we conclude that if G ∈ S_{n+1} and ζ(G) = 0, then G ∈ C, since C contains S_{n} ∪ P_{n} = S_{n} ∪ P_{n} and is closed under substitution.

So suppose that ζ(G) ≥ 1. Consider the following order on σ-chains C such that card C = n + 1:

{r_{0}, …, r_{n}} ≤ {r′_{0}, …, r′_{n}} if and only if
{r_{1}, …, r_{n}} = {r′_{1}, …, r′_{n}} and r_{0} is an ancestor of r′_{0}.

Choose a σ-chain C = {r_{0}, …, r_{n}} which is minimal with respect to this order. We claim that r_{0} is a complete vertex, i.e. we can represent G as G_{r_{0}}^{↓}[G_{↓}^{r_{0}}/r_{0}], so that G_{↓}^{r_{0}} = μ_{r_{0}}.H[r_{0}].

Suppose that r_{0} is not a complete vertex. We can find a return r which is a proper ancestor of r_{0} and a cycle γ on which r, r_{0} lie and such that r_{γ} = r. If ϵ(r) = π then {r, r_{0}, …, r_{n}} is a π-chain in G of cardinality n + 2, against the assumptions. If ϵ(r) = σ, then {r, r_{2}, …, r_{n+1}} is a σ-chain which is strictly smaller than C in the previous order, again contradicting the hypothesis.

Since ζ(G_{r_{0}}^{↓}[r_{0}]) < ζ(G) and similarly ζ(H[r_{0}]) < ζ(G), by the induction hypothesis, we have G_{r_{0}}^{↓}[r_{0}] ∈ C and H[r_{0}] ∈ C. Since C is closed under substitution and the μoperation, we see that G = G_{r_{0}}^{↓}[μ_{r_{0}}.H[r_{0}]/r_{0}] ∈ C.

A similar argument shows that P_{n+1} = P_{n+1}.

By definition it is also clear that L_{n} = S_{n+1} ∩ P_{n+1}, so that L_{n} = L_{n}. This ends the proof of proposition 2.18.

3. Free μ-lattices and free Λ_{n}-models

The goal of this section is to review the characterization of free μ-lattices. We shall then describe a canonical sub-Λ_{n}-model of a free μ-lattice J_{P} and argue that it is the free Λ_{n}-model over the partially ordered set P.

3.1. Definition. Let P be a partially ordered set. A game over P is a pair ⟨G, λ⟩ where G is a game in K and λ : X_{G} ^{}P is a valuation of the partial final positions in P. We write K(P) for the class of games over P and J (P) for the subclass of pairs ⟨G, λ⟩ such that G ∈ J.

We can understand a game over P as a game with complete information with a payoff function taking values in the partially ordered set P. Player σ is trying to maximize his payoff, while his opponent π is trying to minimize the payoff; however, we can also adopt the opponent’s view and think of G as a game over P^{op}, so player π is also trying to maximize the payoff but in the dual poset.

We shall use the simplified notation G for a game ⟨G, λ⟩ over P, leaving in the background the valuation λ : X_{G} ^{}P. In particular, let G ∈ K, let {⟨H_{x}, λ_{x}⟩}_{x∈X_{G}} be a collection of elements of K(P), and observe that the set X_{G[H_{x}/x]_{x∈X_{G}}} is the disjoint union of the sets X_{H_{x}} for x ∈ X_{G}; the notation G[H_{x}/x]_{x∈X_{G}} will abbreviate ⟨G[H_{x}/x]_{x∈X_{G}}, λ⟩, where λ(y) = λ_{x}(y) whenever y ∈ X_{H_{x}}.

We now describe a preorder on the class K(P). This is done by constructing a game ⟨G, H⟩, where G, H ∈ K(P), and by saying that G ≤ H if one of the players, Mediator, has a winning strategy in this game, cf. 1.6. This game, which is essentially the same game described in [5, 15], is played on the two boards G and H at the same time. One player, the one we call Mediator and denote by the letter M, is a team composed by player π on G and player σ on H; the other player, whom we call the Opponents and denote by the letter O, is formed out of player σ on G and player π on H. Mediator, in order to choose a move, must wait for the Opponents to have exhausted their moves on both boards. Mediator’s goal is to reach a pair of positions (x, y) ∈ X_{G} × X_{H}, such that λ(x) ≤ λ(y); in the case of an infinite play, his goal is to win on at least one board. We picture the game as follows:

[figure: σ; :; G; :; π − M − σ; :; H; :; π]

The frame around Mediator’s team is meant to suggest that Mediator can behave like a single player, like a master playing on different chess boards, where the Opponents are indeed two distinct players, since they do not get any advantage from sharing information. We formally define the game ⟨G, H⟩ as follows.

3.2. Definition. Let G, H ∈ K(P). The game ⟨G, H⟩ is defined as:

• Positions of ⟨G, H⟩ are pairs of positions from G and H. The initial position is (g_{0}, h_{0}).

• The coloring ϵ(g, h) is calculated as ϵ(g) · ϵ(h) ∈ {?, M, O}, where the product is given by the table:

\begin{matrix}· & π & σ & 0 \\ σ & O & O & O \\ π & O & M & M \\ 0 & O & M & ? \end{matrix} .

If ϵ(x) · ϵ(y) =?, i.e. if x ∈ X_{G} and y ∈ X_{H}, then ϵ(x, y) = O if and only if λ(x) ≤ λ(y): the pair (x, y) becomes a winning final position for Mediator exactly when λ(x) ≤ λ(y).

• Moves of ⟨G, H⟩ are either left moves (g, h) → (g′, h), where g → g′ ∈ G_{1}, or right moves (g, h) → (g, h′), where h → h′ ∈ H_{1}; however, the Opponents can play only with σ on G or with π on H. This means that the set of moves is obtained from the set G_{1} × H_{0} + G_{0} × H_{1} by removing right moves (g, h) → (g, h′) whenever (ϵ(g), ϵ(h)) = (σ, σ) and left moves (g, h) → (g′, h) whenever (ϵ(g), ϵ(h)) = (π, π).

A morphism of graphs from (the graph underlying) ⟨G, H⟩ to the free category on (the graph underlying) G, is defined as follows: (g, h)_{G} = g and if τ = (g, h) → (g′, h) is a left move, then τ_{G} = g → g′, if τ = (g, h) → (g, h′) is a right move, then τ_{G} = 1_{g}. This morphism is extended to a convex functor from the free category on ⟨G, H⟩ to the free category on G and to a correspondence sending infinite paths in ⟨G, H⟩ to finite or infinite paths in G. We call all these three correspondences left projection and denote them by ( )_{L} or ( )_{G}. The right projection, denoted by ( )_{R} or ( )_{H}, is defined in an analogous way.

• An infinite play γ is a win for Mediator if and only if either its left projection γ_{G} is an infinite play and ϵ(r_{γ_{G}}) = σ, or its right projection γ_{H} is an infinite play and ϵ(r_{γ_{H}}) = π.

3.3. Definition. Let G, H ∈ K(P) be games over P. We declare that G ≤ H if and only if Mediator has a winning strategy in the game ⟨G, H⟩.

We remark that if Mediator has a winning strategy in the game ⟨G, H⟩, then he also has a bounded memory winning strategy, cf. 1.7. This follows from [20, §4] and from well known facts of the theory of games played on finite graphs [21, 25].

3.4. Proposition. Let G, H, K ∈ K(P) be games over P. Then G ≤ G and if G ≤ H and H ≤ K, then G ≤ K.

3.5. Definition. Let G, H ∈ J (P). We write G ≡ H if G ≤ H and H ≤ G, so that ≡ is an equivalence relation. We shall denote by [G] the equivalence class of G and by J_{P} the set of those equivalence classes.

The following is the main result of [19].

3.6. Theorem. For every ordered set P, J_{P} is a μ-lattice, where if G ∈ J and { [H_{x}] }_{x∈X_{G}} ∈ J_{P}^{X_{G}}, then

|G|{ [H_{x}] }_{x∈X_{G}} = [G[H_{x}/x]_{x∈X_{G}}] .

The μ-lattice J_{P} is free over P, i.e. it comes with an embedding η_{P} : P^{}^{}J_{P} with the following universal property: if f : P ^{}L is an order preserving function from P to a μ-lattice L, then there exists a unique morphism of μ-lattices f̃ such that f̃∘ η_{P} = f.

We shall review here the concepts developed to prove proposition 3.4, since we will need them later.

We proved that G ≤ G by exhibiting the copycat strategy in ⟨G, G⟩. It is played as follows. From a position of the form (g, g) it is always the case that the Opponents have to move just on one board. When they stop moving, if they do, Mediator will have the opportunity to copy all the moves played by the Opponents so far on the other board until the play again reaches a position of the form (g′, g′).

We proved that if G ≤ H and H ≤ K then G ≤ K, by describing a game ⟨G, H, K⟩ with the two following properties: given two winning strategies R and S on ⟨G, H⟩ and ⟨H, K⟩ there exists a winning strategy R||S on ⟨G, H, K⟩; given a winning strategy T on ⟨G, H, K⟩ there exists a winning strategy T_{\H} on ⟨G, K⟩. The game ⟨G, H, K⟩ is obtained by gluing the games ⟨G, H⟩ and ⟨H, K⟩ along the center board H. One player, whom we call the Mediators and denote by the letter M, is a team composed by Mediator on ⟨G, H⟩ and Mediator on ⟨H, K⟩; the other player, called the Opponents and denoted by the letter O, is formed out of player σ on G and player π on K. The Mediators can exchange information through the center board H. The game can be pictured as follows:

[figure: σ; :; G; :; π − σ; :; H; :; π − σ; :; K; :; π]

3.7. Definition. Let G, H, K ∈ K(P). The game ⟨G, H, K⟩ is defined as follows:

• Positions of ⟨G, H, K⟩ are triples of positions (g, h, k) ∈ G_{0} × H_{0} × K_{0}. The initial position is (g_{0}, h_{0}, k_{0}).

• The coloring ϵ(g, h, k) is calculated as ϵ(g) · ϵ(k) ∈ {?, O, M}, where the product is given by the table of page 181. If ϵ(x) · ϵ(z) =?, i.e. if x ∈ X_{G} and z ∈ X_{K}, then if ϵ(h) ≠ 0, then ϵ(x, h, z) = M, otherwise, if also h = y ∈ X_{H}, then ϵ(x, y, z) = O if and only if λ(x) ≤ λ(y) ≤ λ(z).

• Moves of ⟨G, H, K⟩ are either left moves (g, h, k) → (g′, h, k), where g → g′ ∈ G_{1}, or central moves (g, h, k) → (g, h′, k), where h → h′ ∈ H_{1}, or right moves (g, h, k) → (g, h, k′), where k → k′ ∈ K_{1}; however, the Opponents can play only with σ on G or with π on K. Several kinds of projections on subsets of the three boards can be defined as in definition 3.2; they will be denoted ( )_{G}, ( )_{H}, ( )_{K}, ( )_{⟨G,H⟩}, ( )_{⟨H,K⟩}, ( )_{⟨G,K⟩}. Observe that for every path γ, finite or infinite, (γ_{⟨G,H⟩})_{G} = (γ_{⟨G,K⟩})_{G} = γ_{G} and similar equalities hold in the other cases.

• An infinite play γ is a win for the Mediators if and only if its left projection γ_{G} is an infinite play and ϵ(r_{γ_{G}}) = σ, or its right projection γ_{K} is an infinite play and ϵ(r_{γ_{K}}) = π.

3.8. Definition. Let R be a winning strategy for Mediator in ⟨G, H⟩ and let S be a winning strategy for Mediator in ⟨H, K⟩. A strategy R||S for the Mediators in the game ⟨G, H, K⟩ is described by the formula

R||S = { γ | γ_{⟨G,H⟩} ∈ R and γ_{⟨H,K⟩} ∈ S } .

Let T be a winning strategy for the Mediators in the game ⟨G, H, K⟩. A strategy T_{\H} for Mediator in the game ⟨G, H, K⟩ is defined by the formula

T_{\H} = { γ_{⟨G,K⟩} | γ ∈ T } .

3.9. Proposition. The strategy R||S is a winning strategy for the Mediators in the game ⟨G, H, K⟩.

Proof. We check that all the conditions of definition 1.6 are satisfied.

If γ ∈ R||S then γ_{⟨G,H⟩} ∈ R and γ_{⟨H,K⟩} ∈ S, so that dom γ_{⟨G,H⟩} = (g_{0}, h_{0}) and dom γ_{⟨H,K⟩} = (h_{0}, k_{0}). Let dom γ = (g, h, k), then (g, h) = (dom γ)_{⟨G,H⟩} = dom γ_{⟨G,H⟩} = (g_{0}, h_{0}), similarly (h, k) = (h_{0}, k_{0}), so that dom γ = (g, h, k) = (g_{0}, h_{0}, k_{0}).

Suppose that γ ⋆ τ ∈ R||S. From γ_{⟨G,H⟩} ⋆ τ_{⟨G,H⟩} = (γ ⋆ τ)_{⟨G,H⟩} ∈ R, we argue that γ_{⟨G,H⟩} ∈ R; similarly γ_{⟨H,K⟩} ∈ S, so that γ ∈ R||S.

Let γ be a path in R||S and let (g, h, k) = cod γ.

Firstly, let us assume that ϵ(g, h, k) = O. If τ is a move available to the Opponents from this position, then it is either a left move or a right move. Suppose it is a left move, say τ = (g, h, k) → (g′, h, k). We deduce that ϵ(g) = σ, which in turn implies that ϵ(g, h) = O. Since γ_{⟨G,H⟩} ∈ R and cod γ_{⟨G,H⟩} = (g, h), then the path γ_{⟨G,H⟩} ⋆ τ_{⟨G,H⟩} ∈ R. We deduce that γ ⋆ τ ∈ R||S, since ( γ ⋆ τ )_{⟨G,H⟩} = γ_{⟨G,H⟩} ⋆ τ_{⟨G,H⟩} ∈ R and ( γ ⋆ τ )_{⟨H,K⟩} = γ_{⟨H,K⟩} ∈ S. If τ is a right move, then a similar argument shows that γ ⋆ τ ∈ R||S.

Suppose now that ϵ(g, h, k) = M. If ϵ(h) = 0 then either ϵ(g) = π or ϵ(k) = σ, suppose ϵ(g) = π. In this case ϵ(g, h) = M, and we can find a transition τ of ⟨G, H⟩ such that γ_{⟨G,H⟩} ⋆ τ ∈ R. Since τ = (g, h) → (g′, h) is a left move, we can lift it to a left move τ′ = (g, h, k) → (g′, h, k), so that γ ⋆ τ′ ∈ R||S since (γ ⋆ τ′)_{⟨G,H⟩} = γ_{⟨G,H⟩} ⋆ τ ∈ R and (γ ⋆ τ′)_{⟨H,K⟩} = γ_{⟨H,K⟩} ∈ S. We can reason similarly if ϵ(k) = σ.

Suppose that ϵ(h) ∈ {σ, π}, say ϵ(h) = σ. In this case ϵ(g, h) = M, and we can find a transition τ of ⟨G, H⟩ such that γ_{⟨G,H⟩} ⋆ τ ∈ R. If τ is a left move, then we lift it to τ′ as before and conclude that γ ⋆ τ′ ∈ R||S. Hence suppose that τ = (g, h) → (g, h′) is a right move. Since ϵ(h) = σ, we deduce that ϵ(h, k) = O, so that γ_{⟨H,K⟩} ⋆ τ̃ ∈ S, where τ̃ = (h, k) → (h′, k). If we set τ′ = (g, h, k) → (g, h′, k), we deduce that γ ⋆ τ′ ∈ S||R, since (γ ⋆ τ′)_{⟨G,H⟩} = γ_{⟨G,H⟩} ⋆ τ ∈ R and (γ ⋆ τ′)_{⟨H,K⟩} = γ_{⟨H,K⟩} ⋆ τ̃ ∈ S. We can reason similarly if ϵ(h) = π.

Suppose now that (g, h, k) = (x, y, z), x ∈ X_{G}, y ∈ X_{H}, z ∈ X_{K}. Since cod γ_{⟨G,H⟩} = (x, y), we deduce that ϵ(x, y) = O, so that λ(x) ≤ λ(y). Since cod γ_{⟨H,K⟩} = (y, z), we deduce that ϵ(y, z) = O, so that λ(y) ≤ λ(z).

Consider an infinite play γ in ⟨G, H, K⟩ which is the result of playing in this way. Either γ_{⟨G,H⟩} is an infinite play, or γ_{⟨H,K⟩} is an infinite play; we suppose the first. If ϵ(γ_{G}) is not an infinite winning play for player π in G, then γ_{H} is an infinite winning play for σ on H: indeed, the pair (γ_{G}, γ_{H}) is the left and right projection of the infinite play γ_{⟨G,H⟩}, which has been played according to the winning strategy R. We can then argue that γ_{⟨H,K⟩} is also an infinite play, moreover it has been played according to the winning strategy S. Since γ_{H} is not an infinite winning play for π on H, and the pair (γ_{H}, γ_{K}) is the left and right projection of γ_{⟨H,K⟩}, it follows that γ_{K} is an infinite winning play for σ on K. A similar argument is used if γ_{⟨H,K⟩} is an infinite play.

3.10. Proposition. The strategy T_{\H} is a winning strategy for Mediator in the game ⟨G, K⟩.

Proof. Let γ ∈ T, then dom γ = (g_{0}, h_{0}, k_{0}), so that dom γ_{⟨G,K⟩} = (dom γ)_{⟨G,K⟩} = (g_{0}, k_{0}). Similarly, if γ_{⟨G,K⟩} = γ_{1} ⋆ τ, then we can find a factorization γ = γ′_{1} ⋆ γ′_{2} such that (γ′_{1})_{⟨G,K⟩} = γ_{1} and (γ′_{2})_{⟨G,K⟩} = τ. It follows that γ_{1} ∈ T_{\H}.

Choose a play γ ∈ T and suppose that cod γ = (g, h, k), so that cod γ_{⟨G,K⟩} = (g, k). Suppose that ϵ(g, k) = O and let τ be a move available to the Opponents from (g, k).

If τ = (g, h) → (g′, h) is a left move, then ϵ(g) = σ, and therefore ϵ(g, h, k) = O. The transition τ′ = (g, h, k) → (g′, h, k) is a move of ⟨G, H, K⟩, hence γ ⋆ τ′ ∈ T and γ_{⟨G,K⟩} ⋆ τ = γ_{⟨G,K⟩} ⋆ τ′_{⟨G,K⟩} = (γ ⋆ τ′)_{⟨G,K⟩} ∈ T_{\H}.

Suppose that ϵ(g, k) = M, and observe that ϵ(g, h, k) = M; we must find a transition τ such that γ_{⟨G,K⟩} ⋆ τ ∈ T_{\H}. Suppose also that we have constructed paths {γ_{i}}_{i=0,...,n} with the following properties: |γ_{j}| = j, γ_{i} is a prefix of γ_{j} if i ≤ j, γ ⋆ γ_{i} ∈ T and (γ ⋆ γ_{i})_{⟨G,K⟩} = γ_{⟨G,K⟩}. Since ϵ(cod γ ⋆ γ_{n}) = M, there exists a transition τ such that γ ⋆ γ_{n} ⋆ τ ∈ T. If τ is a left or right transition, then τ_{⟨G,K⟩} is a transition of ⟨G, K⟩, so that γ_{⟨G,K⟩} ⋆ τ_{⟨G,K⟩} ∈ T_{\H}, and we are done. If τ is a central transition, then we extend the above collection by letting γ_{n+1} = γ_{n} ⋆ τ. Since we cannot build an infinite collection {γ_{n}}_{n≥0} with the above properties – the infinite path {γ ⋆ γ_{n}}_{n≥0} is played according to the winning strategy T, but it is not a win for the Mediators in ⟨G, H, K⟩ – we shall eventually find n ≥ 0 and a right or left transition τ such that γ ⋆ γ_{n} ⋆ τ ∈ T.

Finally, consider an infinite path γ = {γ_{n}}_{n≥0} played according to the strategy T_{\H}. Consider the set of paths

T (γ) = { γ′ ∈ T | γ′_{⟨G,K⟩} ∈ {γ_{n}}_{n≥0} } .

The set T (γ) is closed under prefixes and it is infinite. Hence, it has the structure of a finitely branching infinite tree and we can find an infinite path γ′ = {γ′_{k}} on this tree, which is a subtree of T, such that γ′_{⟨G,K⟩} = γ. Since T is a winning strategy, we have that ϵ(r_{γ_{G}}) = ϵ(r_{γ′_{G}}) = σ or ϵ(r_{γ_{K}}) = ϵ(r_{γ′_{K}}) = σ.

This concludes the proof of proposition 3.4.

3.11. Definition. For every [G] ∈ J_{P}, we define L[G] to be the number

min{ n | L(H) = n , H ∈ [G]}

and let

J_{n,P} = { [G] | L[G] ≤ n } .

3.12. Proposition. The set J_{n,P} is a sub-Λ_{n}-model of J_{P} and the embedding η_{P} : P^{}^{}J_{P} restricts to an embedding η_{n,P} : P^{}^{}J_{n,P}. With this structure J_{n,P} is free over of P, i.e. the above embedding has the usual universal property with respect to order preserving functions with codomain a Λ_{n}-model.

Proof. Let G be a game in L_{n} and { [H_{x}] }_{x∈X_{G}} be a collection of elements in J_{n,P}; we must prove that |G|{ [H_{x}] }_{x∈X_{G}} ∈ J_{n,P}. For each x ∈ X_{G} choose H′_{x} ∈ [H_{x}] such that L(H′_{x}) ≤ n, so that [H_{x}] = [H′_{x}]. The equalities

|G|{ [H_{x}] }_{x∈X_{G}} = |G|{ [H′_{x}] }_{x∈X_{G}}
= [G[H′_{x}/x]_{x∈X_{G}}]

show that |G|{ [H_{x}] }_{x∈X_{G}} ∈ J_{n,P}, since G ∈ L_{n}, H′_{x} ∈ L_{n} and L_{n} is closed under substitution. Since η_{P} (p) = [x, λ^{p}], where λ^{p}(x) = p, it is clear that η_{P} (p) ∈ J_{n,P}.

As a Λ_{n}-model, J_{n,P} is isomorphic to L_{n,P}, the antisymmetric quotient of the preordered class L_{n}(P) of pairs ⟨G, λ⟩ with G ∈ L_{n}, and we shall prove freeness of L_{n,P}. Observe first that the correspondence ⟨G, λ⟩ ^{}⟨G, f ∘ λ⟩, induced by an ordered preserving function f : P ^{}Q, induces an order preserving correspondence L_{n}(f) : L_{n}(P) ^{}L_{n}(Q), and a morphism of Λ_{n}-models L_{n,f} : L_{n,P} ^{}L_{n,Q}. This makes up a functor L_{n} and η_{n} is then a natural transformation in the obvious sense.

On the other hand, if L is a Λ_{n}-model, then the correspondence EV_{n}(L) : L_{n}(L) ^{}L, defined by EV_{n}(L)⟨G, λ⟩ = |G|(λ), also preserves the order, so that it induces a morphism of Λ_{n}-models EV_{L} : L_{n,L} ^{}L such that EV_{n,L} ∘ η_{n,L} = Id_{L}. To prove this, the same argument as in [20, §5.15] is used.

If f : P ^{}L is an order preserving function with codomain a Λ_{n}-model, then EV_{n,L} ∘ L_{n,f} is the desired unique extension of f to a morphism of Λ_{n}-models from L_{n,P} to L.

We shall denote by i_{n,P} : J_{n,P} ^{⊂} ^{}J_{P} the inclusion, so that i_{n,P} is a morphism of Λ_{n}-models and the equality η_{P} = i_{n,P} ∘ η_{n,P} holds.

4. Synchronizing games

The goal of this section is to give a general criterion by which to prove that the inclusion i_{n,P} : J_{n,P} ^{⊂} ^{}J_{P} is proper.

4.1. Definition. Let A ∈ K(P). We say that A is synchronizing if it is bipartite and the only winning strategy for Mediator in the game ⟨A, A⟩ is the copycat strategy.

The intuitions which have induced us to call these games synchronizing are explained as follows: if Mediator is playing according to a winning strategy in the game ⟨G, H⟩, then it is impossible for both the Opponents to win, so that at least one must lose. We can imagine therefore that there is a sort of asynchronous game going on between player σ on G and player π on H, the asynchrony being induced by the mediating choices of Mediator. However, if G = H = A and the only winning strategy for Mediator in ⟨A, A⟩ is the copycat strategy, then there are very few mediating choices. If moreover the game A is bipartite, then the resulting game between player σ on the left and player π on the right is easily recognized to be equivalent with the game A itself, in which the two players act on a synchronous base.

Since a strategy in the game ⟨A, A⟩ is essentially an endomorphism of A, and the copycat strategy plays the role of the identity, we may consider a synchronizing game to be a particular kind of asymmetric object. We remark that if A ∈ J (P) is such that L(A) = 0, then A can be identified with a term for the free lattice over P. In this case, A is synchronizing if and only if it is in normal form as a free lattice term [10, 23]. It is an open problem whether this notion of synchronizing game leads to a normal form for μlattice terms. Examples of synchronizing games are given in section 5. Their remarkable property is stated in the following proposition.

4.2. Theorem. Let A ∈ K(P) be a synchronizing game such that L(A) = n. Then we can construct a game A_{•} ∈ J (P) such that L[A_{•}] = n.

4.3. Corollary. In order to show that the inclusion i_{n,P} : J_{n,P} ^{⊂} ^{}J_{P} is proper, it is enough to find a synchronizing game A in K(P) such that L(A) > n.

Proof. In the following let A = ⟨A_{0}, A_{1}, a_{0}, ϵ, λ⟩ be such a synchronizing game.

The game A_{•} is obtained from A by forcing property 2 in definition 2.10 to hold. If we let A_{•} be ⟨A_{• 0}, A_{• 1}, a_{• 0}, ϵ_{•}, λ_{•}⟩, this game is formally defined as follows.

• The set of positions is

A_{• 0} = R(A) × { 0 } ∪ A_{0} × { 1 } .

The initial position a_{• 0} is (a_{0}, 0) if a_{0} is in R(A), otherwise the initial position is (a_{0}, 1).

• The set of moves is

A_{• 1} = { (g, 1) → (g′, 1) | g → g′ ∈ A_{1}, g′ ∉ R(A) }
∪ { (g, 1) → (r, 0) | g → r ∈ A_{1}, r ∈ R(A) }
∪ { (r, 0) → (r, 1) | r ∈ R(A) } .

• We let ϵ_{•}(g, i) = ϵ(g), and observe that if ϵ_{•}(g, i) = 0, then i = 1 and ϵ(g) = 0; hence, we define λ_{•}(x, i) = λ(x) if ϵ_{•}(x, i) = 0.

Observe that this construction preserves the essential structure of cycles and the color of the returns, from which we deduce that L(A) = L(A_{•}). It is easily seen that A_{•} ∈ J (P), so that L[A_{•}] ≤ L(A_{•}) = L(A) = n.

In order to argue that L[A_{•}] ≥ n, choose an arbitrary H ∈ [A_{•}]. A copycat-like strategy can be used by Mediator to win in both the games ⟨A, A_{•}⟩ and ⟨A_{•}, A⟩, so that, by transitivity, we obtain A ≤ H and H ≤ A. By the analysis of possible plays in the game ⟨A, H, A⟩, we shall construct a chain C in H such that card C = n; it will follow that L(H) ≥ n and L[A_{•}] ≥ n. If θ is a path in ⟨A, H, A⟩ or ⟨A, A⟩, we shall use θ_{L} and θ_{R} for the left and right projections, since the notation θ_{A} would be ambiguous.

The lemma 4.4 below has the following interpretation: if the Opponents know that the Mediators are playing according to a winning strategy, then they can choose a path γ of A and force the Mediators to play on ⟨A, H, A⟩ so that the chosen path is played on the left board as well as on the right board. In this case, we informally say that the Opponents play along the path γ. We let T be any winning strategy for the Mediators in the game ⟨A, H, A⟩.

4.4. Lemma. Let γ be a path of A and let a = dom γ. Suppose that there is a position h of H such that the position (a, h, a) of ⟨A, H, A⟩ has been reached using T. We can lift γ to a play θ_{γ} of ⟨A, H, A⟩ with the following properties:

• dom θ_{γ} = (a, h, a),

• the left projection ( θ_{γ})_{L} as well as the right projection ( θ_{γ})_{R} are both equal to γ,

• the play θ_{γ} has been played according to the strategy T by the Mediators.

Proof. Firstly, we prove the lemma in case γ = a → a′ is a transition of A; we also suppose that ϵ(a) = σ; if ϵ(a) = π we can reason by duality. From position (a, h, a) it is the Opponents’ turn to move, on the left, so that they can choose the move τ on the left.

Since A is bipartite, we have ϵ(a′) ≠ ϵ(a), and in position (a′, h, a) it is the Mediators’ turn to move. From this position, the strategy T will suggest playing a finite path on H (a′, h, a) →^{∗} (a′, h′, a), possibly of zero length, and then it will suggest playing on an external board. An infinite path played only on H cannot arise, since T is a winning strategy, and such an infinite path would not be a win for the Mediators. T cannot suggest a move on the left board - otherwise the strategy T_{\H} would not be the copycat strategy - hence it will suggest a move on the right board. Since T_{\H} is the copycat strategy, the only suggested move will be (a′, h′, a) → (a′, h′, a′).

The generalization of the statement to paths is obtained by induction on the length.

4.5. Lemma. Let θ be a path of ⟨A, H, A⟩, which has been played according to the winning strategy T, such that θ_{L} = θ_{R}. If γ = θ_{L} = θ_{R} has a factorization γ = γ_{1} ⋆ γ_{2}, then there exists a factorization θ = θ_{1} ⋆ θ_{2} such that (θ_{1})_{L} = (θ_{1})_{R} = γ_{1} and (θ_{2})_{L} = (θ_{2})_{R} = γ_{2}.

Proof. We shall prove that if δ is a path of ⟨A, A⟩, which has been played according to the winning strategy T_{\H}, i.e according to the copycat strategy, for which the equalities δ_{L} = δ_{R} = γ hold, then we can lift a factorization γ = γ_{1} ⋆ γ_{2} to a factorization δ = δ_{1} ⋆ δ_{2} in ⟨A, A⟩ such that (δ_{i})_{L} = (δ_{i})_{R} = γ_{i}, for i = 1, 2. To obtain the statement of the lemma, it will be enough to let δ = θ_{⟨A,A⟩}, and then lift the factorization θ_{⟨A,A⟩} = δ_{1} ⋆ δ_{2} to a factorization θ = θ_{1} ⋆ θ_{2}, which is possible since the functor ( )_{⟨A,A⟩} is convex.

The statement is proved by induction on the length of γ_{2}. If |γ_{2}| = 0, the result is obvious; suppose therefore that |γ_{2}| > 0. Since |δ| = |δ_{L}| + |δ_{R}| = 2|γ| ≥ 2, we can write δ = δ′ ⋆ τ′ where |τ′| = 2. Since T_{\H} is the copycat strategy and A is bipartite, we deduce that δ′_{L} = δ′_{R} = γ′, τ′_{L} = τ′_{R} = τ so that |τ| = 1, and write γ = γ′ ⋆ τ. Let γ_{2} = γ′_{2} ⋆ τ and γ′ = γ_{1} ⋆ γ′_{2}. Since |γ′_{2}| < |γ_{2}|, we can use the induction hypothesis and let δ′ = δ_{1} ⋆ δ′_{2} be such that (δ_{1})_{L} = (δ_{1})_{R} = γ_{1} and (δ′_{2})_{L} = (δ′_{2})_{R} = γ′_{2}. Then δ = δ′_{1} ⋆ (δ′_{2} ⋆ τ′) is the desired factorization.

The lifting property of the previous lemma can be generalized: if θ_{L} = θ_{R} = γ_{1}⋆…⋆γ_{n}, where n ≥ 0, then we can find a factorization θ = θ_{1} ⋆ … ⋆ θ_{n} such that (θ_{i})_{L} = (θ_{i})_{R} = γ_{i} for i = 1, …, n.

We have observed that A ≤ H and H ≤ A, hence we shall fix two winning bounded memory strategies for Mediator in the games ⟨A, H⟩ and ⟨H, A⟩, say (R, ψ) and (S, ϕ), respectively. We let

K = max(card R_{0}, card S_{0}) ,

and consider the strategy ψR||ϕS in the game ⟨A, H, A⟩, the definition of which is found in 1.8 and 3.8.

The following lemma can be interpreted as follows: if the Opponents play enough time along a cycle γ of A, then they can force the Mediators to play in a cycle of H of the same color as γ.

4.6. Lemma. Let γ be a proper cycle of A and let θ be a path of ⟨A, H, A⟩, played according to the strategy ψR||ϕS, such that θ_{L} = θ_{R} = γ^{K}. It is possible to find a factorization

θ = Θ_{0} ⋆ Θ ⋆ Θ_{1}

such that Θ_{L}, Θ_{H} and Θ_{R} are all proper cycles. Moreover, Θ_{L} = Θ_{R} = γ^{k}, with 1 ≤ k ≤ K, and ϵ(r_{Θ_{H}}) = ϵ(r_{γ}).

Proof. Let θ be a path of ⟨A, H, A⟩, played according to the strategy ψR||ϕS, such that θ_{L} = θ_{R} = γ^{K}, where γ is proper cycle of A such that ϵ(r_{γ}) = π; if ϵ(r_{γ}) = σ, a dual argument – with the strategy ϕS instead of ψR – can be used. According to lemma 4.5, we can factor θ as

θ = θ_{1} ⋆ … ⋆ θ_{K} ,

so that, for each i = 1, …, K, the relations (θ_{i})_{L} = (θ_{i})_{R} = γ hold.

By the definition of the strategies ψR and ψR||ϕS, there exists a path ρ in R such that ψ ∘ ρ = θ_{⟨A,H⟩}. Consider the factorization in ⟨A, H⟩

ψ ∘ ρ = θ_{⟨A,H⟩}
= (θ_{1})_{⟨A,H⟩} ⋆ … ⋆ (θ_{K})_{⟨A,H⟩} .

Since the functor ψ ∘ is convex, we can lift this factorization to a factorization in R

ρ = ρ_{1} ⋆ … ⋆ ρ_{K}

such that ψ ∘ ρ_{i} = (θ_{i})_{⟨A,H⟩}, for i = 1, …, K. Consider also the set

{ dom ρ_{i} , cod ρ_{i} | i = 1, …, K } ,

and observe that there exist i_{0}, i_{1} ∈ {1, …, K} such that i_{0} ≤ i_{1} and dom ρ_{i_{0}} = cod ρ_{i_{1}}, since card R_{0} ≤ K. Let

Υ = ρ_{i_{0}} ⋆ … ⋆ ρ_{i_{1}},

then Υ is a cycle, and if we let k = i_{1} − i_{0} + 1, then

(ψ ∘ Υ)_{L} = ( (ψ ∘ ρ_{i_{0}}) ⋆ … ⋆ (ψ ∘ ρ_{i_{1}}) )_{L}
= ( (θ_{i_{0}})_{⟨A,H⟩} ⋆ … ⋆ (θ_{i_{1}})_{⟨A,H⟩})_{L}
= (θ_{i_{0}})_{L} ⋆ … ⋆ (θ_{i_{1}})_{L}
= γ^{k} .

Observe also that r_{(ψ∘Υ)_{L}} = r_{γ^{k}} = r_{γ} and that ϵ(r_{γ}) = π. Since ψR is a winning strategy, we argue that ( ψ∘Υ )_{H} is a proper cycle and that ϵ(r_{( ψ∘Υ)_{H}}) = π. Otherwise Υ would give rise, by infinite iteration, to the infinite path Υ^{ω} in the graph R such that ψ∘Υ^{ω} = ( ψ∘Υ )^{ω} is not a win for Mediator in the game ⟨A, H⟩.

In order to conclude the argument, let

Θ = θ_{i_{0}} ⋆ … ⋆ θ_{i_{1}} ,

and find Θ_{0}, Θ_{1} so that the relation θ = Θ_{0} ⋆ Θ ⋆ Θ_{1} is satisfied. Then Θ_{L} = Θ_{R} = γ^{k} with k ≥ 1 by construction. We have also

Θ_{H} = (Θ_{⟨A,H⟩})_{H}
= ( (θ_{i_{0}})_{⟨A,H⟩} ⋆ … ⋆ (θ_{i_{1}})_{⟨A,H⟩})_{H}
= ( (ψ ∘ ρ_{i_{0}}) ⋆ … ⋆ (ψ ∘ ρ_{i_{1}}) )_{H}
= (ψ ∘ Υ)_{H} ,

so that we can conclude that Θ_{H} is a proper cycle such that ϵ(r_{Θ_{H}}) = π = ϵ(r_{γ}).

The following lemma can be interpreted as follows: if the Opponents play enough time along a chain C of A, then they can force the Mediators to play along a chain of H of the same length and color as C.

4.7. Lemma. Let C = {a_{0}, …, a_{n−1}} be a chain in A. For j = 0, …, n − 2, let γ_{j} be proper cycles such that r_{γ_{j}} = a_{j} and a_{j+1} lie on γ_{j}. Factor γ_{j} as γ_{j} = γ_{j}^{↓} ⋆ γ_{j}^{↑}, where dom γ_{j}^{↓} = a_{j} and cod γ_{j}^{↓} = a_{j+1}. Similarly, let γ_{n−1} be a proper cycle of A such that r_{γ_{n−1}} = a_{n−1} = dom γ_{n−1}. For j = n − 1, …, 0, define cycles Γ_{j} in A as follows:

Γ_{n−1} = γ_{n−1}^{K} ,
Γ_{j−1} = (γ_{j−1}^{↓} ⋆ Γ_{j} ⋆ γ_{j−1}^{↑})^{K} .

Let θ be a path in ⟨A, H, A⟩, played according to the strategy ψR||ϕS, such that θ_{L} = θ_{R} = Γ_{j}. We can find a factorization

θ = Θ_{0} ⋆ Θ ⋆ Θ_{1},

with the property that Θ_{H} is a proper cycle visiting a chain {r_{Θ_{H}} = r_{j}, …, r_{n−1} }. Moreover ϵ(r_{j}) = ϵ(a_{j}).

Proof. We prove the proposition by induction on j = n − 1, …, 0.

If j = n − 1, apply lemma 4.6 to θ and γ_{n−1}: it is possible to find a factorization

θ = Θ_{0} ⋆ Θ ⋆ Θ_{1}

such that Θ_{H} is a proper cycle and ϵ(r_{Θ_{H}}) = ϵ(r_{γ_{n−1}}) = ϵ(a_{n−1}).

Suppose that we have proven the assertion for j; we prove it for j − 1. Let θ be a path such that θ_{L} = θ_{R} = (γ_{j−1}^{↓} ⋆ Γ_{j} ⋆ γ_{j−1}^{↑})^{K}. Apply lemma 4.6 to θ and γ_{j−1}^{↓} ⋆ Γ_{j} ⋆ γ_{j−1}^{↑} and find a factorization

θ = Θ_{0} ⋆ Θ ⋆ Θ_{1}

such that Θ_{H} is a proper cycle and ϵ(r_{Θ_{H}}) = ϵ(a_{j−1}), since r_{(γ_{j−1}^{↓}⋆Γ_{j}⋆γ_{j−1}^{↑})} = r_{γ_{j−1}} = a_{j−1}. Moreover, there exists k ≥ 1 such that

Θ_{L} = Θ_{R} = ( γ^{k−1} ⋆ γ_{j−1}^{↓}) ⋆ Γ_{j} ⋆ γ_{j−1}^{↑} ,

where γ = γ_{j−1}^{↓} ⋆ Γ_{j} ⋆ γ_{j−1}^{↑}. By lemma 4.5, we can lift the above factorization to a factorization

Θ = δ_{0} ⋆ δ ⋆ δ_{1} ,

so that δ_{L} = δ_{R} = Γ_{j}. Using the induction hypothesis, there is a factorization

δ = Δ_{0} ⋆ Δ ⋆ Δ_{1} ,

such that Δ_{H} is a proper cycle visiting a chain { r_{Δ_{H}} = r_{j}, …, r_{n−1} }; moreover ϵ(r_{j}) = ϵ(a_{j}). Since

Θ_{H} = (δ_{0} ⋆ Δ_{0})_{H} ⋆ Δ_{H} ⋆ (Δ_{1} ⋆ δ_{1})_{H} ,

we deduce that Θ_{H} visits r_{j}, …, r_{n−1}. If we let r_{j−1} = r_{Θ_{H}}, then the desired chain visited by Θ_{H} is {r_{j−1}, r_{j}, …, r_{n−1}}, since ϵ(r_{j}) = ϵ(a_{j}) ≠ ϵ(a_{j−1}) = ϵ(r_{j−1}). This concludes the proof of lemma 4.7.

In order to prove theorem 4.2, choose a chain C of A, the cardinality of which is maximal, i.e. it is n. Define Γ_{0} as has been done in lemma 4.7, and let γ be the unique simple path from the initial position a_{0} to dom Γ_{0}. Using lemma 4.4, we can lift the path γ ⋆ Γ_{0} of A to a path θ_{γ⋆Γ_{0}} of ⟨A, H, A⟩, played according to the strategy ψR||ϕS by the Mediators, such that both (θ_{γ⋆Γ_{0}})_{L} and (θ_{γ⋆Γ_{0}})_{R} are equal to γ ⋆ Γ_{0}. Using lemma 4.5, we can also lift the given factorization to a factorization θ_{γ⋆Γ_{0}} = θ_{γ} ⋆ θ_{Γ_{0}} so that in particular (θ_{Γ_{0}})_{L} = (θ_{Γ_{0}})_{R} = Γ_{0}. Using lemma 4.7, the center projection (θ_{Γ_{0}})_{H} visits a chain in H of cardinality n which is, moreover, of the same color as the given chain C of A. This concludes the proof of theorem 4.2.

5. Generalized Whitman polynomials

In this section we let X = {a_{0}, a_{1}, a_{2}, b_{0}, b_{1}, b_{2}} be a set of six generators and define a sequence of synchronizing games W^{n} ∈ K(X), n ≥ 1, such that L(W^{n}) = n. We can argue that [W_{•}^{n}] ∉ J_{m,X} if n > m, as in 4.3.

5.1. Theorem. For every n ≥ 1, the inclusion i_{n,X} : J_{n,X} ^{⊂} ^{}J_{X} is proper, where X is a set of six generators.

5.2. Corollary. If P contains an antichain {a_{0}, a_{1}, a_{2}, b_{0}, b_{1}, b_{2}}, then the inclusion i_{m,P} : J_{m,P} ^{⊂} ^{}J_{P} is proper.

The strictness of the alternation hierarchy will follow as explained in 2.6. The construction of the games W^{n} has been suggested by the Whitman polynomial

p(x) = a ∨ (b ∧ (c ∨ (a ∧ (b ∨ (c ∧ x))))) .

Earlier in Birkhoff’s paper [4], a partition lattice and an infinite chain of the form p^{n}(a) are exhibited, so that the free lattice on three generators is shown to be infinite. A more functional interpretation of p(x) is given in [24]. P. Whitman proved that the free lattice on three generators is not complete by showing that free lattices are continuous – so that if the join of the infinite chain p^{n}(a) exists, then it has to be a fixed point of p(x) – and by proving that this polynomial has no fixed point. Later, Crawley and Dean [9] characterized free lattices with infinite operations and used the above polynomial to give lower bounds on the cardinality of those lattices, and a similar technique was used by Hales [11] to show that free complete lattices do not exist in general. Philip Whitman’s result, also documented in the monograph [10], can be used to show that the inclusion i_{0,X} : J_{0,X} ^{⊂} ^{}J_{X} is proper when card X ≥ 3, where we recall that J_{0,X} coincides with the free lattice on the set X.

5.3. Definition. The game W^{n} is defined as follows:

• The set of positions is

{ g_{j}, w_{j} | j = 0, …, 6n − 1 }

and the initial position is g_{0}.

• The set of forward edges is

{ g_{j} → g_{j+1} | j = 0, …, 6n − 2 } ∪ { g_{j} → w_{j} | j = 0, …, 6n − 1 }.

• The set of back edges is

{ g_{3(2n−k)−1} → g_{3k} | k = 0, …, n − 1 }.

• ϵ(w_{j}) = 0, for i = 1, …, 6n − 1 and ϵ(g_{j}) = Q_{j mod 2}, where Q_{0} = σ and Q_{1} = π.

• Eventually, λ(w_{j}) = a_{j mod 3}, if j < 3n and λ(w_{j}) = b_{j mod 3}, if j ≥ 3n.

For example, the games W^{1} and W^{2} are pictured as follows:

[figure: σ; a_{0}; π; a_{1}; σ; a_{2}; π; b_{0}; σ; b_{1}; π; b_{2}; σ; a_{0}; π; a_{1}; σ; a_{2}; π; a_{0}; σ; a_{1}; π; a_{2}; σ; b_{0}; π; b_{1}; σ; b_{2}; π; b_{0}; σ; b_{1}; π; b_{2}]

5.4. Theorem. For each n ≥ 1, the game W^{n} ∈ K(X) is synchronizing and L( W^{n}) = n.

It is easy to see that the game W^{n} is bipartite. Moreover:

5.5. Proposition. The unique strategy in the game ⟨W^{n}, W^{n}⟩ is the copycat strategy.

Proof. In the proof, we shall use the following notation: if g is a position of W^{n} such that ϵ(g) ≠ 0, we shall write w_{g} for the unique g′ such that g → g′ and ϵ(g′) = 0. We let S^{n}(g) be the set of elements g′ such that ϵ(g′) ≠ 0 for which there exists a path of length n from g to g′. We shall use the notation S_{g}^{n} for any element g′ ∈ S^{n}(g), S_{g} will stand for S_{g}^{1} and we shall have g = S_{g}^{0}; with the above notation we must beware of the fact that identities like S_{g}^{n} = S_{g}^{n} do not hold. The following lemma will prove to be useful.

5.6. Lemma. If n ≢ m mod 3, then λ(w_{S_{g}^{n}}) ≠ λ(w_{S_{g}^{m}}).

Proof. It is enough to observe that if g_{j} → g_{j′} is an edge, then j′ ≡ j + 1 mod 3. Hence, if g = g_{i}, g′ ∈ S^{n}(g) and g′′ ∈ S^{m}(g), then λ(w_{g′}) ∈ {a_{i+n mod 3}, b_{i+n mod 3}} and λ(w_{g′′}) ∈ {a_{i+m mod 3}, b_{i+m mod 3}}. However

{a_{i+n mod 3}, b_{i+n mod 3}} ∩ {a_{i+m mod 3}, b_{i+m mod 3}} = ∅ ,

since i + n ≢ i + m mod 3.

In order to prove proposition 5.5, we shall suppose that the game has reached a position of the form (g, g), with ϵ(g) ≠ 0. We shall suppose that ϵ(g) = σ, and use a dual argument if ϵ(g) = π. Depending on the Opponents’ choice, we shall analyse the moves available to Mediator and show that the only possible reply is the one suggested by the copycat strategy. We shall draw trees to represent possible moves as well as winning strategies for the Opponents. Positions are labeled on the left by the player who must move. Dotted transitions are used for Mediator’s moves leading to winning positions for the Opponents.

From (g, g), the Opponents have the following two types of moves:

\begin{matrix}O \\ M \end{matrix}  [figure: (g, g); (w_{g}, g); (S_{g}, g)]

From position (w_{g}, g), Mediator can play as follows:

\begin{matrix}M \\ O \end{matrix}  [figure: (w_{g}, g); (w_{g}, w_{g}); (w_{g}, S_{g})]

Position (w_{g}, S_{g}) is winning for the Opponents, since they can move (w_{g}, S_{g}) → (w_{g}, w_{S_{g}}), where they win because of lemma 5.6.

From position (S_{g}, g), Mediator can play as follows:

\begin{matrix}M \\ O \end{matrix}  [figure: (S_{g}, g); (w_{S_{g}}, g); (S_{g}^{2}, g); (S_{g}, S_{g}); (S_{g}, w_{g})]

We exhibit a winning strategy for the Opponents from position (w_{S_{g}}, g):

\begin{matrix}M \\ O \\ M \\ O \\ M \end{matrix}  [figure: (w_{S_{g}}, g); (w_{S_{g}}, w_{g}); (w_{S_{g}}, S_{g}); (w_{S_{g}}, S_{g}^{2}); (w_{S_{g}}, w_{S_{g}^{2}}); (w_{S_{g}}, S_{g}^{3}); (w_{S_{g}}, w_{S_{g}^{3}})]

We exhibit a winning strategy for the Opponents from position (S_{g}^{2}, g):

\begin{matrix}O \\ M \\ O \\ M \end{matrix}  [figure: (S_{g}^{2}, g); (w_{S_{g}^{2}}, g); (w_{S_{g}^{2}}, S_{g}); (w_{S_{g}^{2}}, w_{S_{g}}); (w_{S_{g}^{2}}, w_{g})]

We exhibit a winning strategy for the Opponents from position (S_{g}, w_{g}):

\begin{matrix}M \\ O \\ M \end{matrix}  [figure: (S_{g}, w_{g}); (w_{S_{g}}, w_{g}); (S_{g}^{2}, w_{g}); (w_{S_{g}^{2}}, w_{g})]

To complete the argument, we must show that if (S_{g}, S_{g}) is a position such that S_{g} ≠ S_{g}, i.e. it is of the form (g_{3k}, g_{3(2n−k)}) or (g_{3(2n−k)}, g_{3k}) with k ∈ {1, …, n − 1}, then the Opponents have a winning strategy. Suppose that (S_{g}, S_{g}) = (g_{3k}, g_{3(2n−k)}), so that λ(w_{3k}) = a_{0} and λ(w_{3(2n−k)}) = b_{0}; the Opponents have the following strategy:

\begin{matrix}O \\ M \\ O \\ M \end{matrix}  [figure: (g_{3k}, g_{3(2n−k)}); (g_{3k}, w_{3(2n−k)}); (w_{3k}, w_{3(2n−k)}); (S_{g}^{2}, w_{S_{g}}); (w_{S_{g}^{2}}, w_{S_{g}})]

Similarly, the Opponents have a winning strategy from position (g_{3(2n−k)}, g_{3k}). This concludes the proof of proposition 5.5.

5.7. Proposition. The game W^{n} contains a σ-chain of cardinality n. Since card R(W^{n}) = n, we deduce that L( W^{n}) = n.

Proof. Firstly, we observe that R(W^{n}) = { g_{3k} | k = 0, …, n−1 }, and then that R(W^{n}) is itself a chain. For if 0 ≤ k < k′ ≤ n − 1, then 3k′ < 3(2n − k′) − 1 < 3(2n − k) − 1, so that g_{3k′} lies on the cycle going from g_{3k} down to g_{3(2n−k)−1} and back to g_{3k}.

References

[1] S. Abramsky and R. Jagadeesan. Games and full completeness for multiplicative linear logic. J. Symbolic Logic, 59(2):543–574, 1994.

[2] A. Arnold. The μ-calculus alternation-depth hierarchy is strict on binary trees. Theor. Inform. Appl., 33(4-5):329–339, 1999.

[3] A. Arnold and D. Niwiński. Rudiments of μ-calculus. North-Holland Publishing Co., Amsterdam, 2001.

[4] G. Birkhoff. On the structure of abstract algebras. Proc. Camb. Philos. Soc., 31:433– 454, 1935.

[5] A. Blass. A game semantics for linear logic. Ann. Pure Appl. Logic, 56(1-3):183–220, 1992.

[6] S. L. Bloom and Z. Ésik. Iteration theories. Springer-Verlag, Berlin, 1993.

[7] J. C. Bradfield. The modal mu-calculus alternation hierarchy is strict. Theoret. Comput. Sci., 195(2):133–153, 1998.

[8] J. C. Bradfield. Simplifying the modal mu-calculus alternation hierarchy. In STACS 98, volume 1373 of Lecture Notes in Comput. Sci., pages 39–49, 1998.

[9] P. Crawley and R. A. Dean. Free lattices with infinite operations. Trans. Amer. Math. Soc., 92:35–47, 1959.

[10] R. Freese, J. Ježek, and J. B. Nation. Free lattices. American Mathematical Society, Providence, RI, 1995.

[11] A. W. Hales. On the non-existence of free complete Boolean algebras. Fund. Math., 54:45–66, 1964.

[12] H. Hu and A. Joyal. Coherence completions of categories. Theoret. Comput. Sci., 227(1-2):153–184, 1999.

[13] A. Joyal. Free bicomplete categories. C. R. Math. Rep. Acad. Sci. Canada, 17(5):219– 224, 1995.

[14] A. Joyal. Free bicompletion of enriched categories. C. R. Math. Rep. Acad. Sci. Canada, 17(5):213–218, 1995.

[15] A. Joyal. Free lattices, communication, and money games. In Logic and scientific methods, pages 29–68, 1997. Proceedings of the 10th international congress of logic, methodology and philosophy of science, Florence, Italy, August 19–25, 1995.

[16] G. Lenzi. A hierarchy theorem for the μ-calculus. In Automata, languages and programming, volume 1099 of Lecture Notes in Comput. Sci., pages 87–97, 1996.

[17] D. Niwiński. Equational μ-calculus. In Computation theory, volume 208 of Lecture Notes in Comput. Sci., pages 169–176, 1985.

[18] D. Niwinski. On fixed-point clones. In Automata, languages and programming, volume 226 of Lecture Notes in Comput. Sci., pages 464–473, 1986.

[19] L. Santocanale. Sur les μ-treillis libres. PhD thesis, Université du Québec à Montréal, July 2000. Available: http://www.cpsc.ucalgary.ca/∼luigis.

[20] L. Santocanale. Free μ-lattices. J. Pure Appl. Algebra, 168(2-3):227–264, 2002.

[21] W. Thomas. Languages, automata, and logic. In G.Rozenberg and A. Salomaa, editors, Handbook of formal languages. Vol. 3, pages 389–455. Springer-Verlag, Berlin, 1997.

[22] Igor Walukiewicz. Completeness of Kozen’s axiomatisation of the propositional μcalculus. Inform. and Comput., 157(1-2):142–182, 2000.

[23] P. M. Whitman. Free lattices. Ann. of Math. (2), 42:325–330, 1941.

[24] P. M. Whitman. Free lattices. II. Ann. of Math. (2), 43:104–115, 1942.

[25] W. Zielonka. Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theoret. Comput. Sci., 200(1-2):135–183, 1998.

Department of Computer Science, University of Calgary. 2500 University Drive N.W., Calgary, Alberta, Canada T2N 1N4.

Email: luigis@cpsc.ucalgary.ca

This article may be accessed via WWW at http://www.tac.mta.ca/tac/ or by anony-

mous ftp at ftp://ftp.tac.mta.ca/pub/tac/html/volumes/9/n9/n9.{dvi,ps}

THEORY AND APPLICATIONS OF CATEGORIES (ISSN 1201-561X) will disseminate articles that significantly advance the study of categorical algebra or methods, or that make significant new contributions to mathematical science using categorical methods. The scope of the journal includes: all areas of pure category theory, including higher dimensional categories; applications of category theory to algebra, geometry and topology and other areas of mathematics; applications of category theory to computer science, physics and other mathematical sciences; contributions to scientific knowledge that make use of categorical methods.

Articles appearing in the journal have been carefully and critically refereed under the responsibility of members of the Editorial Board. Only papers judged to be both significant and excellent are accepted for publication.

The method of distribution of the journal is via the Internet tools WWW/ftp. The journal is archived electronically and in printed paper format.

Subscription information. Individual subscribers receive (by e-mail) abstracts of articles as they are published. Full text of published articles is available in .dvi, Postscript and PDF. Details will be e-mailed to new subscribers. To subscribe, send e-mail to tac@mta.ca including a full name and postal address. For institutional subscription, send enquiries to the Managing Editor, Robert Rosebrugh,

rrosebrugh@mta.ca.

Information for authors. The typesetting language of the journal is TEX, and L^{A}TEX is the preferred flavour. TEX source of articles for publication should be submitted by e-mail directly to an appropriate Editor. They are listed below. Please obtain detailed information on submission format and style files from the journal’s WWW server at http://www.tac.mta.ca/tac/. You may also write to tac@mta.ca to receive details by e-mail.

Editorial board.

John Baez, University of California, Riverside: baez@math.ucr.edu Michael Barr, McGill University: barr@barrs.org, Associate Managing Editor Lawrence Breen, Université Paris 13: breen@math.univ-paris13.fr Ronald Brown, University of North Wales: r.brown@bangor.ac.uk Jean-Luc Brylinski, Pennsylvania State University: jlb@math.psu.edu Aurelio Carboni, Università dell Insubria: aurelio.carboni@uninsubria.it P. T. Johnstone, University of Cambridge: ptj@dpmms.cam.ac.uk G. Max Kelly, University of Sydney: maxk@maths.usyd.edu.au Anders Kock, University of Aarhus: kock@imf.au.dk F. William Lawvere, State University of New York at Buffalo: wlawvere@acsu.buffalo.edu Jean-Louis Loday, Université de Strasbourg: loday@math.u-strasbg.fr Ieke Moerdijk, University of Utrecht: moerdijk@math.uu.nl Susan Niefield, Union College: niefiels@union.edu Robert Paré, Dalhousie University: pare@mathstat.dal.ca Andrew Pitts, University of Cambridge: Andrew.Pitts@cl.cam.ac.uk Robert Rosebrugh, Mount Allison University: rrosebrugh@mta.ca, Managing Editor Jiri Rosicky, Masaryk University: rosicky@math.muni.cz James Stasheff, University of North Carolina: jds@math.unc.edu Ross Street, Macquarie University: street@math.mq.edu.au Walter Tholen, York University: tholen@mathstat.yorku.ca Myles Tierney, Rutgers University: tierney@math.rutgers.edu Robert F. C. Walters, University of Insubria: walters@fis.unico.it R. J. Wood, Dalhousie University: rjwood@mathstat.dal.ca