BRICS RS-00-28 L. Santocanale: Free μ-lattices BRICS

Basic Research in Computer Science

Free μ-lattices

Luigi Santocanale BRICS Report Series RS-00-28 ISSN 0909-0878 November 2000 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2000, Luigi Santocanale.

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

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

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

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

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

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

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

This document in subdirectory RS/00/28/

Free μ-lattices^{∗}

Luigi Santocanale

             luigis@brics.dk

BRICS^{†}

Abstract

A μ-lattice is a lattice with the property that every unary polynomial has both a least and a greatest fix-point. In this paper we define the quasivariety of μ-lattices and, for a given partially ordered set P, we construct a μ-lattice J_{P} whose elements are equivalence classes of games in a preordered class J (P). We prove that the μ-lattice J_{P} is free over the ordered set P and that the order relation of J_{P} is decidable if the order relation of P is decidable. By means of this characterization of free μ-lattices we infer that the class of complete lattices generates the quasivariety of μ-lattices.

Keywords: μ-lattices, free μ-lattices, free lattices, bicompletion of categories, models of computation, least and greatest fix-points, μ-calculus, Rabin chain games.

1 Introduction

A lattice is a μ-lattice if every unary polynomial has both a least prefixpoint and a greatest postfix-point. Here, a unary polynomial is a derived operator evaluated in all but one variables; however derived operators are built up from the basic lattice operations in a more complex way: by substitution and by the two operations of taking the least prefixpoint and of taking the greatest postfix-point. After recalling the basic facts about the least prefix-point of an order preserving map and, dually, about the greatest postfix-point, we shall give a formal definition of the notion of μ-lattice. We shall complete this definition to the definition of a category: intuitively, a morphism of lattices is also a morphism of μlattices if the required least prefix-points and greatest postfix-points are preserved. The category of μ-lattices is a quasivariety, as is evident from the fact that the property of being a least prefix-point of a polynomial is definable by implications of equations. The main goal of this paper is to explicitely construct a μ-lattice J_{P}, where P is a given partially ordered set, and prove its universal property, i.e. the fact that J_{P} is the free μ-lattice over P. The μ-lattice J_{P} is described as the anti-symmetric quotient of a preordered class of games J (P). Games in J (P) can be thought of as games with complete information having a payoff function taking values in P; infinite plays are allowed, in which case just one player is considered to be the winner. Given two games G and H of J (P) we say that G ≤ H if there exists a winning strategy for a player, Mediator, in a compound game of communication ⟨G, H⟩. We shall first prove that this construction leads to a μ-lattice, in particular that all the required fix-points exist, and then we shall prove that J_{P} is the free μ-lattice over the partially ordered set P. We shall also give a proof that the order relation of J (P) is decidable if the order relation of P is decidable, thus giving a solution to the word problem for the theory of μ-lattices. We shall eventually exemplify the power of this construction by showing that the class of complete lattices generates the quasivariety of μ-lattices. The algebraic notion of μ-lattice has been implicitly proposed before: it is related to the general notion of μ-algebra, studied in [Niw85, Niw97], and it is inspired by ideas originated in the context of the propositional μ-calculus [Pra81, Koz83]. This logical setting is essentially the basic modal system K to which least and greatest fix-point operators have been added. We recall that a main problem in computer science is the verification of programs so that the reason to add fix-point operators to logics has been to make possible to express computational properties of transition systems otherwise ineffable. At the same time, algorithms for model checking properties expressed by formulas of the propositional μcalculus have proved to be more feasible than those for other powerful logics. Our motivations for studying free μ-lattices are of a slightly different nature and came mainly from ideas contained in [Joy95c]. In this paper Whitman’s solution to the word problem for lattices [Whi41] is interpreted and generalized in terms of games and communication. We recall that an interactive computational system is a sort of game between a machine and a user, a program being a strategy which is winning if it satisfies correctness conditions. By pairing the well-known analogy between interactive computational systems and games [NYY92, McN93, AJ94] with the work relating games to bicompletion of categories [Joy77, Joy95c, Joy95a, Joy95b] it is proposed to model interactive computation by free lattices and free bicomplete categories. A previous work [HJ99] pursued this idea and exhibited connections between another model of interactive computation, i.e. coherent spaces of linear logic [Gir87], and a bicompletion of categories. The main advantage of modeling computation with games for free μlattices is the presence of infinite plays. Indeed, games related to free lattices excluded those plays and a richer algebraic object was required to model interactive computation with possibly infinite behaviors. A main source of ideas has been the theory of games developed in connection with monadic second order logic, propositional μ-calculus and sets of infinite objects definable by means of these logics [Rab69, GH82, Arn95, Tho97, Zie98]. The relation among Rabin chain games [EJ91, Wal96], combinatorial games with infinite plays [Con78] and games in the class J (P) is documented in [San00]. A recent tradition in logic and proof-theory interprets proofs as games [Fel86, Bla92, AJ94, Gir98] and provides a game semantic to programming languages [AJM94, HO94]; in all cases the correspondence between proofs or programs and games is shown to be close “enough”. On the other hand, methods from proof theory can be used to give useful presentations of free algebraic objects [LS86]. We adopt here a proof-theoretic point of view and comment our work by saying that it shows how fixpoint operators can have a good proof-theory, statement which has to be interpreted in the following way. A proof system C for the theory of μ-lattices is given and shown to be equivalent to a natural proof system N for the same theory. Cut-elimination, which fails for the system N, is satisfied by the system C so that the order relation in the theory of μ-lattices is eventually shown to be decidable. The main characteristic of the system C is that the underlying graph of a proof is not a tree but a finite graph which could contain cycles; because of that we call C the system of circular proofs. The details of such logical interpretation of the present work are carried out in [San00]. We remark here that circular proofs are analogous to regular refutations in the theory of the propositional μ-calculus [Wal95, NW96].

∗This work was developed at the Département de Mathématiques of the Université du Québec à Montréal, as part of my doctoral research.

† Basic Research in Computer Science, Centre of the Danish National Research Foundation.

The paper is organized as follows.

In section 2, Preliminaries, page 5, we recall definitions and some basic facts about fix-points and games. We shall assume the reader is familiar with the notions of least prefix-point and greatest postfix-point; if not, he is invited to read [Niw85] which is very close to the point of view adopted here.

In section 3, μ-lattices, page 9, we define μ-lattices and the category of μ-lattices.

In section 4, The μ-lattice J_{P}, page 12, we explicitely construct the μlattice J_{P} for a given ordered set P. Similar constructions and theorems have been developed in the context of game semantics for proof systems [Bla92, AJ94] as well as in the context of combinatorial games [Con76, Joy77]. We believe that the main novelty is the proof of proposition 4.11 that the formal construction of a least prefix-point leads to a real least prefix-point with respect to the usual order.

In section 5, Decidability of the order relation of J_{P}, page 27, we prove that if the order relation of P is decidable, then the order relation in J_{P} is decidable too. We obtain this result by showing that the game ⟨G, H⟩ is not so far away from a game whose infinite winning paths are defined by a Muller-condition. Hence we use the main theorem of [GH82] to prove that games of the form ⟨G, H⟩ have bounded memory strategies. In order to effectively construct such a strategy we use ideas implicitly contained in [Tho97] and [Wal96]. The bounded determinacy theorem for the games ⟨G, H⟩ will also be used later in section 6 to prove freeness of J_{P} and it will be fundamental to prove the completeness theorem of section 7.

In section 6, Freeness of the μ-lattice J_{P}, page 30, we prove freeness of J_{P}. We show that given a μ-lattice L there is function EV : J (L) ^{}L which necessarily induces a morphism of μ-lattices EV_{L} : J_{L} ^{}L if it is order preserving. Much of the work is concerned with showing that EV is order preserving.

In section 7, A completeness theorem, page 41, we prove that in the free μ-lattice J_{P} every definable unary operator ϕ satisfies the Knaster-Tarski relation:

μ_{z}.ϕ(z) = ⋁_{α∈Ord} ϕ^{α}(⊥) ,

and, of course, its dual. As a consequence, the free μ-lattice can be embedded in a complete lattice and such embedding is a morphism of μlattices, showing that the full sub-category of complete lattices generates the quasivariety of μ-lattices. We relate this result to [Wal95] in that it is implied that a Kozen’s style of axiomatizing μ-lattices is complete with respect to the complete-lattices semantics where formal μ-lattice terms are interpreted as elements of complete lattices.

We add concluding remarks at page 46 and references at page 47.

2 Preliminaries

2.1 Least and greatest fix-points

In the following we shall consider the category of partially ordered sets and order preserving maps. We shall refer to partially ordered sets simply as ordered sets and, sometimes, to order preserving maps as operators.

Definition 2.1 Let P be an ordered set and let ϕ : P ^{}P be a unary operator. The least prefix-point of ϕ, if it exists, is an element μ_{z}.ϕ(z) ∈ P such that:

i. ϕ( μ_{z}.ϕ(z) ) ≤ μ_{z}.ϕ(z),

ii. if p ∈ P is such that ϕ(p) ≤ p, then μ_{z}.ϕ(z) ≤ p.

The greatest postfix-point of ϕ, denoted ν_{z}.ϕ(z), is defined dually, i.e. it is an element of P such that:

i. ν_{z}.ϕ(z) ≤ ϕ( ν_{z}.ϕ(z) ),

ii. if p ∈ P is such that p ≤ ϕ(p), then p ≤ ν_{z}.ϕ(z).

Of course, if μ_{z}.ϕ(z) exists, then it is uniquely determined by the properties defining it, and similarly for ν_{z}.ϕ(z). We list here some well-known properties of the operation μ of taking the least prefix-point of operators. Their proofs can be found in [Niw85].

Proposition 2.2 [Tar55]. The least prefix-point μ_{z}.ϕ(z) is a fix-point of ϕ:

ϕ( μ_{z}.ϕ(z) ) = μ_{z}.ϕ(z).

By abuse of language, we shall refer to the least prefix-point of ϕ sometimes also as the least fix-point of ϕ.

Proposition 2.3 The operation μ is order preserving: if for all p ∈ P ϕ(p) ≤ ψ(p), then μ_{z}.ϕ(z) ≤ μ_{z}.ψ(z).

Proposition 2.4 The operation μ is dinatural: let ϕ : P ^{}Q, ψ : Q ^{}P be operators, then μ_{z}.ϕ ∘ ψ(z) := ϕ( μ_{y}.ψ ∘ ϕ(y) ), i.e. suppose that μ_{y}.ψ ∘ ϕ(y) exists, then μ_{z}.ϕ ∘ ψ(z) exists too and it is equal to ϕ( μ_{y}.ψ ∘ ϕ(y) ).

Proposition 2.5 Let ϕ : P × P ^{}P be a binary operator and suppose that for every p ∈ P μ_{z}.ϕ(p, z) exists. Then the correspondence p ^{}μ_{z}.ϕ(p, z) is order preserving and μ_{y}.( μ_{z}.ϕ(y, z) ) :=: μ_{z}.ϕ(z, z), i.e. if one of the least prefix-point exists, then the other exists too and they are equal.

Similar properties are true for the greatest postfix-point operation ν.

2.2 Games

Definition 2.6 A partial game is a tuple G = ⟨G_{0}, G_{1}, g_{0}, ϵ, W_{σ}⟩ where ⟨G_{0}, G_{1}⟩ is a graph^{1}, g_{0} ∈ G_{0}, ϵ : G_{0} ^{}{0, σ, π} and W_{σ} is a set of infinite paths in ⟨G_{0}, G_{1}⟩, i.e. morphisms of graphs γ : ω̂ ^{}⟨G_{0}, G_{1}⟩, where ω̂ is the graph 0 → 1 → … → n → …. We require that if ϵ(g) = 0, then { g′ | g → g′ } = ∅. Moreover, since an infinite path γ ∈ W_{σ} does not necessarily satisfy γ(0) = g_{0}, we require the following coherence condition on infinite paths: γ is in W_{σ} if and only if ∂γ is in W_{σ}, where ∂γ is the infinite path defined by ∂γ(n) = γ(n + 1), for n ≥ 0.

1We shall mainly consider partial games whose underlying graph is a relation, i.e. G_{1} ⊆ G_{0} × G_{0}, for example partial games in J. However the development of the theory does not depend on this hypothesis, and we shall consider games whose underlying graph is a span δ_{0}, δ_{1} : G_{1} G_{0}. In particular the game ⟨G , H⟩, G, H ∈ J (P), could be such a game, since it is desirable to distinguish left loops from right loops.

We interpret the above data 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 it 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. Eventually, 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 π.

Definition 2.7 A complete game, or just a game, is a partial game such that X_{G} = ∅.

Definition 2.8 A morphism of partial games f : G ^{}H is a morphism of pointed graphs^{2} f : ⟨G_{0}, G_{1}, g_{0}⟩ ^{}⟨H_{0}, H_{1}, h_{0}⟩ such that ϵ ∘ f = ϵ and such that γ ∈ W_{σ} if and only if f ∘ γ ∈ W_{σ}, for every infinite play γ in G. A morphism of partial games f : G ^{}H is an isomorphism if and only if there exists a morphism of partial games g : H ^{}G such that g ∘ f = Id_{G} and f ∘ g = Id_{H}. Note that f : G ^{}H is an isomorphism of partial games if and only if f is invertible as a morphism of graphs. Moreover, if G is a game, ⟨K_{0}, K_{1}, k_{0}⟩ is a pointed graph and f : ⟨K_{0}, K_{1}, k_{0}⟩ ^{}⟨G_{0}, G_{1}, g_{0}⟩ is a morphism of pointed graphs, then ⟨K_{0}, K_{1}, k_{0}⟩ can be endowed with a unique gamestructure so that f is a morphism of partial games. Indeed, define ϵ by saying that ϵ = ϵ ∘ f, and say that γ ∈ W_{σ} if and only if f ∘ γ ∈ W_{σ}. A sub-game of G is a sub-graph S of ⟨G_{0}, G_{1}⟩ such that g_{0} is a node of S; S is then a pointed graph and the inclusion preserves the point, so that S has a canonical structure of a partial game obtained when the inclusion is made into a morphism of partial games.

Definition 2.9 A morphism of partial games f : G ^{}H is open if for every move f(g) → h′ there exists a move g → g′ such that f(g → g′) = f(g) → h′; it is étale if such a move exists and it is unique. We say that f : G ^{}H is π-open if the above property holds whenever ϵ(g) = π.

2i.e. a morphism of graphs f : ⟨G_{0}, G_{1}⟩ ⟨H_{0}, H_{1}⟩ such that f(g_{0}) = h_{0}.

Definition 2.10 Let G be a partial game. A cover of G is a pair ⟨K, ψ⟩ where K is a partial game and ψ : K ^{}G is an étale morphism of partial games. We shall say that a cover ⟨K, ψ⟩ is finite if the set K_{0} is finite.

Definition 2.11 Let G be a partial game. The unfolding tree of G, denoted by T (G), is the partial game defined as follows: a position of T (G) is a pair (γ, n) where n ≥ 0 and γ is a play of length n beginning at the initial position; more formally, if n̂ is the graph 0 → 1 → … → n, then γ : n̂ ^{}⟨G_{0}, G_{1}⟩ is a morphism of graphs such that γ(0) = g_{0}. The initial position of T (G) is (γ_{0}, 0), where γ_{0} is the unique play of length 0 beginning at g_{0}. Moves are of the form (γ, n) → (δ, n + 1) where δ(i) = γ(i), for 0 ≤ i ≤ n. The evaluation map ev : (γ, n) ^{}γ(n) is a morphism of pointed graphs, so that the definition of T (G) is completed canonically to the definition of a partial game by making ev into a morphism of partial games. It is easily seen that ⟨T (G), ev⟩ is a cover of G.

Proposition 2.12 Let ⟨K, ψ⟩ be a cover of a partial game G. The morphism of partial games ψ_{∗} : T (K) ^{}T (G), defined by ψ_{∗}(γ, n) = (ψ ∘ γ, n), is then an isomorphism.

Let G be a partial game, and let g be a position of G. We shall say that g is reachable if there exists a position (γ, n) of T (G) such that ev(γ, n) = g. We shall say that G is reachable if ev is surjective and that G is a tree if ev is an isomorphism; in particular T (G) is a tree.

Definition 2.13 A partial game G is a σ-game if for every reachable position g such that ϵ(g) = σ, there exists a move g → g′ and if for every infinite path γ such that γ(0) = g_{0}, it is true that γ ∈ W_{σ}. A σ-game is a game where player σ always wins, no matter how he plays.

Definition 2.14 Let G be a partial game. A winning strategy for player σ in G is a reachable sub-game S of T (G) - hence a subtree of T (G) - which is σ-game and such that the inclusion is a π-open morphism of partial games.

Hence, in order to describe a winning strategy S, we shall define it - often implicitly - as a sub-tree of T (G) and then check that: it is closed under π-moves (i.e. the sub-tree is π-open); that from every position g, reached by playing according to S and such that ϵ(g) = σ, there is a move g → g′ available in S; moreover that every infinite play played with S is a win for player σ (i.e. the sub-tree is a σ-game). Sometimes, for clarity of exposition, we shall check that ϵ(g) ∈ {0, π} if g is a position with no moves available.

Proposition 2.15 Let G be a partial game and let ⟨K, ψ⟩ be a cover of G. Then player σ has a winning strategy in G if and only if player σ has a winning strategy in K.

Proof. The proposition follows because T (G) is isomorphic to T (K) and winning strategies have been defined by means of properties which are invariant under isomorphism of partial games. □

We shall frequently use the following notion.

Definition 2.16 Let G be a finite partial game. A bounded memory winning strategy for player σ in G is a tuple ⟨S, K, ψ⟩, where ⟨K, ψ⟩ is a finite cover of G and S is a reachable sub-game of K which is a σ-game and such that the inclusion is a π-open morphism of partial games.

Similar notions, as σ-open morphism, π-game, winning strategy for player π, are defined by swapping π and σ.

3 μ-lattices

In this section we shall define μ-lattices and their morphisms. We shall do it by introducing a set A of terms which are to be interpreted as operators on a lattice.

Definition 3.1 The set of terms A and the arity-function a : A ^{}ℕ are defined by induction as follows:

1. ⋀_{n} ∈ A and a(⋀_{n}) = n, for n ≥ 0.

2. ⋁_{n} ∈ A and a(⋁_{n}) = n, for n ≥ 0.

3. If ϕ_{i} ∈ A, a(ϕ_{i}) = k_{i}, for i = 1, …, n, ϕ ∈ A, a(ϕ) = n, then ϕ ∘ (ϕ_{1}, …, ϕ_{n}) ∈ A and a(ϕ ∘ (ϕ_{1}, …, ϕ_{n})) = ∑_{i=1,...,n} k_{i}.

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

5. If ϕ ∈ A, a(ϕ) = n + 1, then ν_{s}.ϕ ∈ A and a(ν_{s}.ϕ) = n, for s = 1, …, n + 1.

Definition 3.2 Let L be a lattice. We shall define a partial interpretation of terms ϕ ∈ A, a(ϕ) = n, as operators |ϕ| : L^{n} ^{}L.

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

2. | ⋁_{n} |(l_{1}, …, l_{n}) = ⋁_{i=1,...,n} l_{i} .

3. Let ϕ ∈ A be such that a(ϕ) = n and for i = 1, …, n let ϕ_{i} ∈ A be such that a(ϕ_{i}) = k_{i}. Suppose |ϕ| and |ϕ_{i}| are defined. In this case we define |ϕ ∘ (ϕ_{1}, …, ϕ_{n})| to be:

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

where k_{i}^{−} = 1 + ∑_{j=1}^{i−1} k_{j}, k_{i}^{+} = ∑_{j=1}^{i} k_{j} and k = k_{n}^{+} = ∑_{j=1}^{n} k_{j}.

4. Let ϕ ∈ A be such that a(ϕ) = n + 1. Suppose that |ϕ| is defined and let s be an element of {1, …, n + 1}. If for each vector (l_{1}, …, l_{n}) ∈ L^{n} there exists the least prefix-point of the unary operator |ϕ|(l_{1}, …, l_{s−1}, z, l_{s}, …, l_{n}), then we define |μ_{s}.ϕ| to be:

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

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

5. Let ϕ ∈ A be such that a(ϕ) = n+1. Suppose that |ϕ| is defined and let s be an element of {1, …, n+1}. If for each vector (l_{1}, …, l_{n}) ∈ L^{n} there exists the greatest postfix-point of the unary operator |ϕ|(l_{1}, …, l_{s−1}, z, l_{s}, …, l_{n}), then we define |ν_{s}.ϕ| to be:

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

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

Definition 3.3 A lattice L is a μ-lattice if the interpretation of terms ϕ ∈ A is a total function, which is the same as recursively requiring that for each ϕ ∈ A such that a(ϕ) = n + 1, for each s = 1, …, n + 1, and for each vector (l_{1}, …, l_{n}) ∈ L^{n} the least prefix-point and the greatest postfix-point of the unary operator |ϕ|(l_{1}, …, l_{s−1}, z, l_{s}, …, l_{n}) exist.

A complete lattice is a μ-lattice, in particular every finite lattice is a μ-lattice. Also, every distributive lattice L is a μ-lattice: if ϕ ∈ A is such that a(ϕ) = n + 1, then |ϕ|(l_{1}, …, l_{s−1}, z, l_{s}, …, l_{n}) = (z ∧ ψ_{1}(l_{1}, …, l_{n})) ∨ ψ_{2}(l_{1}, …, l_{n}) or |ϕ|(l_{1}, …, l_{s−1}, z, l_{s}, …, l_{n}) = (z ∨ ψ_{1}(l_{1}, …, l_{n})) ∧ ψ_{2}(l_{1}, …, l_{n}), where the ψ_{i} are usual n-ary polynomials of the theory of lattices, so that the required fix-points exist.

Definition 3.4 Let L_{1}, L_{2} be two μ-lattices. An order preserving function f : L_{1} ^{}L_{2} is a μ-lattice morphism if for all ϕ ∈ A such that a(ϕ) = n, the following is a commutative diagram:

[figure: L_{1}^{n}; |ϕ|; L_{1}; L_{2}^{n}; f^{n}; |ϕ|; L_{2}; f] .

The following lemma is easily proved by induction.

Lemma 3.5 A morphism of lattices f : L_{1} ^{}L_{2} between μ-lattices is a μ-lattice morphism if and only if for all ϕ ∈ A such that a(ϕ) = n + 1, if f ∘ |ϕ| = |ϕ| ∘ f^{n+1}, then the following is true:

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

for all vectors (l_{1}, …, l_{n}) ∈ L^{n} and for all s = 1, …, n + 1.

4 The μ-lattice J_{P}

In this section we describe a μ-lattice J_{P} for an arbitrary partially ordered set P. We shall be interested in a class J of partial games, defined as follows.

Definition 4.1 The class J is the least class X of partial games closed under the following operations on partial games and under isomorphisms of partial games.

• x is the game with just one partial final position x.

• Let I be a finite set. ⋁_{I} is the game with starting position ∨_{0} ∉ I, ϵ(∨_{0}) = σ, partial final positions x_{i} and moves ∨_{0} → x_{i}, for i ∈ I. ⋀_{I} is defined similarly; it has starting position ∧_{0} and ϵ(∧_{0}) = π.

• If G and H are games and x ∈ X_{G}, the underlying pointed graph of the game G[H/x] is obtained by the substitution of the underlying pointed graph of H for x in the underlying pointed graph of G; such a graph, which we denote ⟨K_{0}, K_{1}⟩, can be defined by considering any concrete representation of the pushout diagram in the category of graphs:

[figure: ˆ0; x; ⟨G_{0}, G_{1}⟩; ⟨H_{0}, H_{1}⟩; h_{0}; j; ⟨K_{0}, K_{1}⟩; i] .

The graph ⟨K_{0}, K_{1}⟩ is then pointed by i(g_{0}) and ϵ is defined consequently, by the universal property. An infinite path γ in ⟨K_{0}, K_{1}⟩ is such that γ = i∘δ, for a unique path δ in ⟨G_{0}, G_{1}⟩, or there exists an n ≥ 0 and a path δ′ in ⟨H_{0}, H_{1}⟩ such that ∂^{n}γ = j ∘ δ′. After the obvious identifications, we are allowed to define the set W_{σ} by saying that an infinite play γ is a win for σ in G[H/x] if and only if either γ is a win for σ in G, or there exists n ≥ 0 such that the infinite play γ(n) → γ(n + 1) → … is a win for σ in H.

• Let G 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}. We set the starting position to x and say that ϵ(x) = σ. An infinite play γ is a win for σ in μ_{x}.G[x] if and only if the position x is visited finitely many times and there exists n ≥ 0 such that the play γ(n) → γ(n + 1) → … is an infinite winning play for player σ in G.

• Let G be a partial game and let x ∈ X_{G}. The underlying graph of ν_{x}.G[x] is the same as the underlying graph of G with one more move x → g_{0}. We set the starting position to x and say that ϵ(x) = π. An infinite path γ is a win for σ in ν_{x}.G[x] if and only if either the position x is visited infinitely often or there exists n ≥ 0 such that γ(n) → γ(n + 1) → … is an infinite winning play for σ in G.

We shall use the notation G[H] as a shorthand for G[H/x] when there is no possibility of confusion. Substitution satisfies several forms of associativity rules, for example (G[H/x])[K/y] ≅ (G[K/y])[H/x] if x, y ∈ X_{G} and x ≠ y. Hence if x_{i} ∈ X_{G} and H_{i} ∈ J for all i ∈ I, we shall denote by G[H_{i}/x_{i}] any such sequence of substitutions. We shall also write ⋀_{i∈I} G_{i} as a shorthand notation for ⋀_{I}[G_{i}/x_{i}], and similarly we shall write ⋁_{i∈I} G_{i} in place of ⋁_{I}[G_{i}/x_{i}]. Finally, we shall use ⊤ for ⋀_{∅} and ⊥ for ⋁_{∅}. Let ⟨G_{0}, G_{1}⟩ be a graph and let γ : n̂ ^{}⟨G_{0}, G_{1}⟩ be a path. We shall say that γ is simple if it does not visit a node twice, i.e. if γ is injective as a function.

Definition 4.2 A tree with back edges is a pointed graph ⟨G_{0}, G_{1}, g_{0}⟩ such that for every node g ∈ G_{0} there exists an 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 if τ ∘ γ_{g} ≠ γ_{g′}.

Let ⟨G_{0}, G_{1}, g_{0}⟩ be a tree with back edges and let F be the collection of forward edges. The pointed graph ⟨G_{0}, F, g_{0}⟩ is then a tree and if τ : g → g′ is a back edge then g′ is an ancestor of g in the tree ⟨G_{0}, F, g_{0}⟩. Conversely, consider a pair ⟨T, β⟩, where T = ⟨T_{0}, T_{1}, t_{0}⟩ is a tree and β : T_{0} ^{}𝒫(T_{0}) is such that if r ∈ β(t) then r is an ancestor of t. Then the graph ⟨T_{0}, T_{1}^{β}, t_{0}⟩, where T_{1}^{β} = T_{1} ∪ { t → r | r ∈ β(t) }, is a tree with back edges. Hence a pointed graph ⟨G_{0}, G_{1}, g_{0}⟩ is a tree with back edges if and only if there exists such a pair ⟨T, β⟩ and moreover G_{0} = T_{0}, G_{1} = T_{1}^{β} and g_{0} = t_{0}. Since a pair with these properties is uniquely determined by ⟨G_{0}, G_{1}, g_{0}⟩, we can refer to it without creating a source of confusion. Also, we shall identify the pair ⟨T, β⟩ with the graph ⟨T_{0}, T_{1}^{β}, t_{0}⟩. Let ⟨T, β⟩ be a finite tree with back edges. A node r ∈ T_{0} is called a return if r ∈ β(t) for some t ∈ T_{0}. Observe that, for an infinite path γ in ⟨T, β⟩, there exists a unique return r_{γ} visited infinitely often which is of minimal height. Here the height of a node in ⟨T, β⟩ is the length of the unique simple path from the root to the node, i.e. the usual height of the node in the tree T. Similarly, for every proper cycle γ in ⟨T, β⟩, i.e. a cycle of length strictly greater than 0, there exists a unique return r_{γ} of minimal height lying on γ. With that in mind we observe the following.

Proposition 4.3 A partial game G is in the class J if and only if:

i. its underlying pointed graph ⟨G_{0}, G_{1}, g_{0}⟩ is a finite tree with back edges such that if r ∈ G_{0} is a return, then there exists an unique back edge P (r) → r as well as an unique edge r → S(r);

ii. an infinite path γ is in W_{σ} if and only if ϵ(r_{γ}) = π.

Proof. Call X the class of partial games satisfying properties i and ii and observe that it is closed under the operations of definition 4.1, so that J ⊆ X. For the converse it suffices to show that X is generated from a proper subset of the operations of 4.1. To do that, we need to introduce a complexity measure on the class of games X. Let G be a game in this class and let ⟨T, β⟩ be its underlying tree with back edges. Its complexity χ(G) is defined as:

χ( G) = ( card ⋃_{t∈T_{0}} β(t) , card T_{0} ) .

We have that χ(G) ∈ ℕ × ℕ, which is well ordered by the lexicographic order: (n, m) ≤ (n′, m′) if and only if n ≤ n′ and n = n′ implies m ≤ m′. We shall actually prove a stronger statement:

Lemma 4.4 A game G ∈ X is isomorphic to exactly one game of the form x, ⋀_{i∈I} H_{i}, ⋁_{i∈I} H_{i}, μ_{x}.H[x] or ν_{x}.H[x], where the games H_{i} and H belong to X, are uniquely determined up to isomorphism by G and have complexity strictly less than G.

Proof of 4.4. The root t_{0} is either a return or not. In the latter case, depending on the coloring of the root, ϵ(t_{0}) = 0, σ, π, G is isomorphic to games of the form x, ⋀_{i∈I} H_{i}, ⋁_{i∈I} H_{i}, where the games H_{i} are obtained by considering the trees with back edges having their roots the successors {t_{i}}_{t_{0}→t_{i}} of t_{0}. Since the number of positions of the H_{i} is strictly less of that of G, we have χ(H_{i}) < χ(G). Consider now the case that t_{0} is a return. In this case G = Q_{t_{0}}.H[t_{0}] where H is the game in X defined by means of the tree with back edges ⟨T′, β′⟩, where

T′ = ⟨ T_{0} , T_{1} \ {t_{0} → S(t_{0})} ∪ {P (t_{0}) → t_{0}} , S(t_{0}) ⟩

and β′ = β \ {P (t_{0}) → t_{0}}. Of course Q = μ, ν depending whether ϵ(t_{0}) = σ, π in G, and in H we have that ϵ(t_{0}) = 0. Finally χ(H) < χ(G) since the number of returns of H is strictly less then the number of returns of G. This ends the proof of lemma 4.4 as well as the proof of proposition 4.3. □

Since X = J, lemma 4.4 is true with J in place of X. The lemma allows us to define by induction on the structure of games in the class J and of course to use inductive arguments in the proofs. When considering trees with back edges, substitution as defined in 4.1 can be defined directly in terms of substitution on trees as follows: let ⟨T_{i}, β_{i}⟩, i = 1, 2, be two such trees, and let x be a leaf of ⟨T_{1}, β_{1}⟩, that is, x is a leaf of T_{1} and β_{1}(x) = ∅, then:

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

If ⟨T, β⟩ 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 r ∈ β(t′), r is also a descendant of t. In this case ⟨T, β⟩ can be represented as the result of substituting the subtree with back edges of root t in the tree obtained from ⟨T, β⟩ by forcing t to be a leaf. A minimal return is a return r ∈ T_{0} such that there are no other returns on the unique simple path γ_{r}. A minimal return is surely a complete vertex. We arrive at the following conclusion, which will be one of the main observations needed in section 6.

Proposition 4.5 Given a partial game G ∈ J and a minimal return r of G we obtain a representation of G as G_{r}[ Q_{r}.G^{S(r)}[r] /r], where Q = μ if ϵ(r) = σ and Q = ν if ϵ(r) = π. Moreover the partial games G_{r} and G^{S(r)} have complexity strictly less than G.

We are ready to introduce the main object of study, i.e. games over a partially ordered set P.

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

A game over P can be thought as a game where the payoff comes from a partially ordered set. Player σ is trying to maximize his payoff, and, if we adopt σ’s point of view, his opponent π, who is actually playing over P^{op}, is trying to minimize the payoff. If the game is in a position where no moves are available and if this position is labeled by a certain player, then this player loses. We shall use a simplified notation for games over P, when this notation will not be ambiguous. We shall use the notation G for a game ⟨G, λ⟩ over P, leaving in the background the labeling λ : X_{G} ^{}P. Similarly we shall use the notations G[H/x], G[H], ⋀_{i∈I} G_{i}, ⋁_{i∈I} G_{i}, ⊤ and ⊥. Given two games G, H, we shall construct a complete game ⟨G, H⟩, i.e. a game where every position is labeled by a player. This is the same as saying it is a game over the empty-set. This game is played on the two boards at the same time. One player, whom we call Mediator, is formed by a coalition of player π on G and player σ on H, while the other player, whom we call the Opponents, is formed by player σ on G and player π on H. The situation is not symmetric since Mediator, in order to choose a move, must wait for the Opponents to exhaust their moves on both boards. This is actually an advantage: indeed, by waiting for the Opponents to have exhausted their moves, Mediator can select the board on which to continue the play, the Opponents being obliged to reply on it. Mediator’s goal is to reach a compatible pair of positions (x, y) ∈ X_{G} × X_{H}, i.e. a pair such that λ(x) ≤ λ(y). In the case of an infinite play, his goal is to win on at least one board. Therefore we picture the game as follows:

σ_{G} : G : π_{G}  σ_{H} : H : π_{H}

We have added a dotted line between players π_{G} and σ_{H} to suggest that in the compound game they can get an advantage from sharing informations, where the same is not true for the Opponents σ_{G} and π_{H}. Indeed, it is helpful to think of Mediator as being a single player - like a master playing on several chess boards - and of the Opponents as being two distinct players. The game ⟨G, H⟩ is essentially the same as the games described in similar contexts [Bla92, Joy95c]. In order to generalize proofs we need the following observation about games in J (P): if a player plays unfairly then he loses. More formally, if G ∈ J (P) and γ is an infinite play in G such that there exists n_{0} with ϵ(γ(n)) = π for all n ≥ n_{0}, then γ ∈ W_{σ}; and a similar condition is true with π and σ interchanged. In the formal definition of the game ⟨G, H⟩, which is given in the following paragraphs, Mediator is player σ of this game and the Opponents are player π. Consider the ordering 0 ≤ σ ≤ π on the set {0, σ, π}, and the function ¬ : {0, σ, π} ^{}{0, σ, π}, defined by ¬0 = 0, ¬σ = π and ¬π = σ. Define the product · as x · y = (¬x) ∨ y. The table for this product is as follows:

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

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

• Positions of ⟨G, H⟩ are just pairs of positions from G and H:

⟨G, H⟩_{0} = G_{0} × H_{0} .

The initial position is (g_{0}, h_{0}) and we calculate ϵ(g, h) as ϵ(g)·ϵ(h) ∈ {0, σ, π}. In order to turn it into a complete game we declare that, if ϵ(x) · ϵ(y) = 0, i.e. x ∈ X_{G} and y ∈ X_{H}, then:

ϵ(x, y) = \{ \begin{matrix}π , & if λ(x) ≤ λ(y) , \\ σ , & if λ(x) ≰ λ(y) . \end{matrix}

The pair (x, y) becomes a winning final position for Mediator exactly when λ(x) ≤ λ(y).

• The set of moves of ⟨G, H⟩ is a subset of the set G_{1}×H_{0} + G_{0}×H_{1}. It is defined as:

(g, h) → (g′, h) ∈ ⟨G, H⟩_{1} iff g → g′ ∈ G_{1} and ¬ϵ(g) ≥ ϵ(h) ,
(g, h) → (g, h′) ∈ ⟨G, H⟩_{1} iff h → h′ ∈ H_{1} and ¬ϵ(g) ≤ ϵ(h) .

We can classify moves of ⟨G, H⟩ as left moves if they have the form (g, h) → (g′, h) or right moves if they have the form (g, h) → (g, h′). Mediator’s left moves, i.e. those for which ϵ(g) = π, are allowed only if ϵ(h) ≠ π; similarly Mediator’s right moves are allowed only if ϵ(g) ≠ σ. Opponents’ left or right moves are always allowed.

• An infinite play γ is in W_{σ}, i.e. it is a win for Mediator, if and only if its left projection γ_{G} is an infinite winning play for player π in G, or its right projection γ_{H} is an infinite winning play for player σ in H.

In the above definition, the left projection of an infinite play can be defined as follows. If δ is a finite path in the graph underlying ⟨G, H⟩, then it is an arrow in the free category over this graph. Its left projection δ_{G} is the image of δ under the morphism of categories which sends every left move (g, h) → (g′, h) to g → g′ and every right move to an identity. Let γ be an infinite path and consider the increasing sequence {γ_{n}}_{n≥0} of its finite prefixes of length n. We construct γ_{G} in the obvious way by glueing the increasing sequence {γ_{n,G}}_{n≥0}; γ_{G} could be an infinite path as well as a finite path. The right projection γ_{H} is defined in a similar way. The definition of the game ⟨G, H⟩ applies also to pairs ⟨G, λ_{G}⟩ and ⟨H, λ_{H}⟩, where G and H are arbitrary partial games, λ_{G} : X_{G} ^{}P and λ_{H} : X_{H} ^{}P. If moreover K is a partial game and λ_{K} : X_{K} ^{}P, given a morphism of partial games f : K ^{}G such that λ_{K} = λ_{G} ∘ f, we can define ⟨f, H⟩ : ⟨K, H⟩ ^{}⟨G, H⟩ by the formula ⟨f, H⟩(k, h) = (f(k), h). It is easily seen that ⟨f, H⟩ is a morphism of games and that it is injective or étale if f is such.

Definition 4.8 Let G, H ∈ J (P) be games over P. Say that G ≤ H if Mediator has a winning strategy in ⟨G, H⟩.

Proposition 4.9 For games in J (P) the following is true:

i. G ≤ G and if G ≤ H and H ≤ K then G ≤ K.

ii. For every finite set I

∀i ∈ I G ≤ H_{i} iff G ≤ ⋀_{i∈I} H_{i} ,
∀i ∈ I G_{i} ≤ H iff ⋁_{i∈I} G_{i} ≤ H .

Proof of proposition 4.9.i. We prove that G ≤ G by exhibiting a strategy in ⟨G, G⟩ - the copycat strategy - and then showing that it is a winning one. From a position of the form (g, g) it is always the case that just one of the Opponents has to move. When he stops moving, if he does stop, Mediator will have the opportunity to copy all the moves played so far on the other board until the play reaches again a position of the form (g′, g′). By playing with this strategy, a pair of final positions can only be of the form (x, x) for one partial final position x ∈ X_{G}, and of course λ(x) ≤ λ(x). Consider an infinite play γ which is the result of playing in this way. Either one of the Opponents has been playing unfairly, in which case γ is a win for Mediator, or the play has gone up to infinity by repeated copying of moves from one board to the other. In this latter case the left projection γ_{L} of γ is equal to the right one γ_{R}. Hence γ_{L} is a winning infinite play for π on G or γ_{R} = γ_{L} is a winning infinite play for σ on G. This shows that γ is a win for Mediator and also that the copycat strategy is a winning strategy.

We prove that if G ≤ H and H ≤ K then G ≤ K, by describing a game ⟨G, H, K⟩ with the following properties:

a. given two winning strategies R and S on ⟨G, H⟩ and ⟨H, K⟩ there exists a winning strategy R ∘ S on ⟨G, H, K⟩,

b. given a winning strategy T on ⟨G, H, K⟩ there exists a winning strategy T_{\H} on ⟨G, K⟩.

If R is a winning strategy witness of G ≤ H and S is a winning strategy witness of H ≤ K, then the strategy (R ∘ S)_{\H}, which we call the communication strategy, will be the winning one required to show that G ≤ K. Let G, H, K be three partial games. The game ⟨G, H, K⟩ is defined as follows:

• ⟨G, H, K⟩_{0} = G_{0} × H_{0} × K_{0}, the initial position is (g_{0}, h_{0}, k_{0}), and ϵ(g, h, k) = ¬ϵ(g)∨(ϵ(h)∧¬ϵ(h))∨ϵ(k). Moreover, if ϵ(x, y, z) = 0, i.e. x ∈ X_{G}, y ∈ X_{H} and z ∈ X_{K}, then we declare that (x, y, z) is a winning position for player σ if and only if λ(x) ≤ λ(y) ≤ λ(z).

• ⟨G, H, K⟩_{1} is defined as:

(g, h, k) → (g′, h, k) iff g → g′ and ¬ϵ(g) ≥ ϵ(h) ∨ ϵ(k) ,
(g, h, k) → (g, h′, k) iff h → h′ and
¬ϵ(g) ≤ (ϵ(h) ∧ ¬ϵ(h)) ≥ ϵ(k) ,
(g, h, k) → (g, h, k′) iff k → k′ and ¬ϵ(g) ∨ ¬ϵ(h) ≤ ϵ(k) .

• γ ∈ W_{σ} if and only if γ_{G} ∈ W_{π} or γ_{K} ∈ W_{σ}.

The game ⟨G, H, K⟩ is a generalization of the game ⟨G, H⟩ and can be informally pictured as follows:

σ_{G} : G : π_{G}  σ_{H} : H : π_{H}  σ_{K} : K : π_{K}

Intuitively, in the game ⟨G, H, K⟩ player σ is formed by an alliance of players π_{G}, σ_{H}, π_{H} and σ_{K}: players π_{G}, σ_{H} and π_{H}, σ_{K} are consciously playing together, as they would do as the Mediators of the games ⟨G, H⟩ and ⟨H, K⟩ respectively, where players π_{H}, σ_{H} are unconsciously playing together, they are actually playing against each other in H. Proof of a. Observe that from a position (g, h, k) the set of moves available to player π_{⟨G,H⟩} is a subset of the set of moves available from position (g, h) of ⟨G, H⟩, and similarly for player π_{⟨H,K⟩} and the moves available from position (h, k) of ⟨H, K⟩. Moreover, if ϵ(g, h, k) = σ, then either ϵ(g, h) = σ or ϵ(h, k) = σ; in the first case, all the moves available to σ_{⟨G,H⟩} from position (g, h) of ⟨G, H⟩ are available from (g, h, k) and, similarly for the latter case, all the moves available to σ_{⟨H,K⟩} from position (h, k) of ⟨H, K⟩ are also available from (g, h, k). We can now make sense of the following statement: the strategy R ∘ S is defined by saying that player σ uses R on the board ⟨G, H⟩ and S on the board ⟨H, K⟩. The strategy R ∘ S is closed under π-moves. Suppose that ϵ(g, h, k) = π, then either ϵ(g) = σ or ϵ(k) = π, suppose the first. If player π chooses to move (g, h, k) → (g′, h, k), where (g, h) is a position reached by playing with R and (h, k) is a position reached by playing with S, then (g′, h) is a position reached with R and (h, k) is a position reached with S. Reason similarly if ϵ(k) = π. Suppose now that ϵ(g, h, k) = σ. If ϵ(h) = 0 then either ϵ(g) = π or ϵ(k) = σ. If the former, then player σ can use strategy R to choose a move (g, h) → (g′, h); if (g, h) has been reached with R and (h, k) has been reached playing with S, then so have (g′, h) and (h, k). Reason similarly if ϵ(k) = σ. Suppose that ϵ(h) ∈ {σ, π}, say ϵ(h) = σ. In this case ϵ(g, h) = σ and player σ can choose a move from ⟨G, H⟩ using the strategy R. If this move is of the form (g, h) → (g′, h), then (g′, h) has been reached with R and (h, k) has been reached by playing with S. If this move is of the form (g, h) → (g, h′), then (g, h′) has been reached with R and (h′, k) has been reached with S too, since in this case (h, k) → (h′, k) is an Opponents’ move in ⟨H, K⟩. Reason similarly if ϵ(h) = π. Consider a final position (x, y, z). Then (x, y) is a position reached by playing with R and (y, z) is a position reached by playing with S. Because R and S are winning, it follows that λ(x) ≤ λ(y) and λ(y) ≤ λ(z). Consider an infinite play γ in ⟨G, H, K⟩ which is the result of playing in this way. Suppose that γ_{G} is not an infinite winning play for player π in G. Since the pair (γ_{G}, γ_{H}) is the left and right projection of the play γ_{⟨G,H⟩}, which has been played according to the winning strategy R, it follows that γ_{H} is an infinite winning play for σ on H. Hence γ_{H} is not an infinite winning play for π on H. Since the pair (γ_{H}, γ_{K}) is the left and right projection of the play γ_{⟨H,K⟩}, which has been played according to the winning strategy S, it follows that γ_{K} is an infinite winning play for σ on K. Proof of b. Player σ plays in ⟨G, H, K⟩ according to the strategy T, and reports external moves to ⟨G, K⟩. In a position (g, k) σ will have recorded a position h such that (g, h, k) is a position reached by playing with T. In the initial position (g_{0}, k_{0}) he records h_{0}. Suppose that a position (g, k) has been reached and that σ has recorded h. If ϵ(g, k) = π then ϵ(g, h, k) = π, and every move of player π in the game ⟨G, K⟩ is a move of player π on ⟨G, H, K⟩ and vice-versa, so that the strategy T_{\H} is closed under Opponents’ moves. For example, if Opponents move g → g′ on G, then this move is also available to player π of ⟨G, H, K⟩ from position (g, h, k). Hence the position (g′, h, k) is reached by playing with T, and, by playing with T_{\H}, the new position (g′, k) is reached from (g, k) and the record h is unaltered. Suppose that ϵ(g, k) = σ, so that ϵ(g, h, k) = σ. The position (g, h, k) has been reached using T, and the play can continue, according to T, either externally on G or K, or internally on H. In the first case such a continuation becomes a move on ⟨G, K⟩ by T_{\H}, the record h being unaltered. In the second case, i.e. when T suggests a move of the form (g, h, k) → (g, h′, k), the position (g, k) is unaltered but the record is changed to h′, and player σ can ask the strategy T for another continuation. The strategy T will suggest another move from position (g, h′, k) and, eventually, this move will be an external one on G or K. This is because T is a winning strategy and an infinite internal play on H which is stuck on both G and K, is not a winning play for player σ. Consider a pair of final positions (x, z) reached by playing with the strategy T_{\H}, say with record h. Then the position (x, h, z) has been reached by playing with T. ϵ(x, h, z) ∈ {0, σ} and if ϵ(x, h, z) = σ then the play can be prolonged by playing with T, forcedly on H, but it will eventually end in a position of the form (x, y, z) with ϵ(y) = 0. Because T is winning, λ(x) ≤ λ(y) ≤ λ(z), hence λ(x) ≤ λ(z). Finally, consider an infinite play γ played according to the strategy T_{\H}. Evidently, γ comes from an infinite play γ′ played according to the strategy T. Since T is winning we obtain that γ_{G} = γ′_{G} ∈ W_{π} or γ_{K} = γ′_{K} ∈ W_{σ}. This ends the proofs of proposition 4.9.i. □

Proof of proposition 4.9.ii. We shall prove first that:

⋀_{j∈J} H_{j} ≤ H_{i} ,

for an arbitrary i ∈ J. Let ∧_{0} and h_{i} be the initial positions of ⋀_{j∈J} H_{j} and H_{i} respectively. Observe that if ϵ(h_{i}) ∈ {0, σ} then Mediator can immediately move (∧_{0}, h_{i}) → (h_{i}, h_{i}) on the left. After this move the game is as in ⟨H_{i}, H_{i}⟩, hence Mediator can play according to the copycat strategy. If ϵ(h_{i}) = π, then the right opponent moves on the board H_{i}. When he stops, if he does, he will give the chance to Mediator to choose H_{i} on the left and to copy there all the moves played so far on the right, entering in this way the pattern of the copycat strategy. We show now that:

G ≤ ⋀ G .

Let g_{0} be the initial position of G. The reasoning is similar to the one of the previous paragraph. If ϵ(g_{0}) ∈ {0, π}, then Mediator immediately enters the pattern of the copycat strategy after the unique Opponents’ move (g_{0}, ∧_{0}) → (g_{0}, g_{0}). If ϵ(g_{0}) = σ then Mediator is allowed to enter the pattern of the copycat strategy as soon as the Opponents move (g′, ∧_{0}) → (g′, g_{0}) on the right.

We can now show that if G ≤ H_{i} for all i ∈ I, then:

G ≤ ⋀_{i∈I} H_{i} .

We can suppose that the initial position g_{0} of G is such that ϵ(g_{0}) = π, otherwise we can substitute the game G with the equivalent one ⋀ G. In the game ⟨G, ⋀_{i∈I} H_{i}⟩ the first moves are of the form (g_{0}, ∧_{0}) → (g_{0}, h_{i}) so that, after the right opponent has chosen such a move, the game is as in ⟨G, H_{i}⟩ and Mediator can play according to a given strategy to win this game. The proof that G_{i} ≤ H for all i ∈ I if and only if ⋁_{i∈I} G_{i} ≤ H is dual. This ends the proof of proposition 4.9.ii. □

Definition 4.10 A game-operator K[x] on J (P) is a triple ⟨K, x, λ⟩ where K ∈ J, x ∈ X_{K} and λ : X_{K} \ {x} ^{}P.

Proposition 4.11 Let K[x] be a given game-operator on J (P) and let G, H ∈ J (P) be games over P. Then:

i. if G ≤ H then K[G] ≤ K[H],

ii. K[ μ_{x}.K[x] ] ≤ μ_{x}.K[x] and if K[H] ≤ H then μ_{x}.K[x] ≤ H,

iii. ν_{x}.K[x] ≤ K[ ν_{x}.K[x] ] and if G ≤ K[G] then G ≤ ν_{x}.K[x].

Proof of proposition 4.11.i. The result is clear if ϵ(g_{0}) ∈ {0, π} and ϵ(h_{0}) ∈ {0, σ}, where g_{0}, h_{0} are the initial positions of G and H respectively. In this case Mediator can play according to the copycat strategy; if a play reaches a position of the form (x, k) or (k, x), a sequence of Opponents’ moves will stop, because of the new color of position x, which is now identified on the left with g_{0} and on the right with h_{0}. Mediator can copy moves and reach the position (x, x), i.e. (g_{0}, h_{0}), where he starts playing according to a given strategy to win ⟨G, H⟩. The general result will follow if we can show that K[G] ≤ K[⋀ G] when ϵ(g_{0}) = σ, and, dually, that K[⋁ H] ≤ K[H] when ϵ(h_{0}) = π; in this case from G ≤ H it will follow ⋀ G ≤ ⋁ H, K[⋀ G] ≤ K[⋁ H] and eventually K[G] ≤ K[H], by transitivity. Essentially Mediator plays according to the copycat strategy in ⟨K[G], K[G]⟩: the insertion of a unique π-move from position x (which is now identified to ∧_{0}, the initial position of ⋀ G) on the right doesn’t matter. The following two sequences of possible plays are meant to show what could happen by playing with the copycat strategy in ⟨K[G], K[⋀ G]⟩:

\begin{matrix}→_{σ_{L}}^{∗} (g_{0}, k) →_{σ_{L}}^{∗} (g, k) →_{σ_{R}}^{∗} (g, ∧_{0}) →_{π_{R}} (g, g_{0}) →_{σ_{R}}^{∗} (g, g) , \\ →_{π_{R}}^{∗} (k, ∧_{0}) →_{π_{R}} (k, g_{0}) →_{π_{L}}^{∗} (g_{0}, g_{0}) . \end{matrix}

Here an arrow →_{σ_{L}}^{∗} means a sequence of moves played by σ on the left board and similar conventions hold for →_{σ_{R}}^{∗}, →_{π_{L}}^{∗}, →_{π_{R}}^{∗}. In the following if S is a strategy witness of G ≤ H, we shall call K[S] the strategy witness of K[G] ≤ K[H] obtained by pasting the copycat strategy of K[x] with the strategy S. This concludes the proof of proposition 4.11.i. □

Proof of proposition 4.11.ii. We construct an infinite cover ψ : K_{σ}^{ω}[⊥] ^{}μ_{x}.K[x]; the game K_{σ}^{ω}[⊥] is said to be infinite in that its underlying graph is infinite. Covers are preserved by the construction of the game ⟨G, H⟩, hence we obtain a cover:

⟨ψ, H⟩ : ⟨K_{σ}^{ω}[⊥], H⟩ ^{}⟨μ_{x}.K[x], H⟩ .

From a game-theoretic point of view there is no difference between a game and one of its covers, since they have the same unfolding tree and a strategy is a particular subtree of the unfolding tree, cf. 2.15. We shall construct a winning strategy in the game ⟨K_{σ}^{ω}[⊥], H⟩ and deduce the existence of a winning strategy in ⟨μ_{x}.K[x], H⟩. The infinite game K_{σ}^{ω}[⊥] is defined as follows:

• Its positions are of the form (k, n) with k ∈ K_{0} and n ≥ 0, the initial position is (x, 0), ϵ(k, n) = ϵ(k) if k ≠ x and ϵ(x, n) = σ.

• Moves of K_{σ}^{ω}[⊥] are either of the form (k, n) → (k′, n), where k → k′ is a move of K, or are of the form (x, n) → (k_{0}, n + 1).

The function ψ, defined by ψ(k, n) = k, is easily seen to be a cover of the underlying graph of μ_{x}.K[x] by the underlying graph of K_{σ}^{ω}[⊥]. We complete the definition of K_{σ}^{ω}[⊥] in the obvious way:

• γ is a winning path for σ in K_{σ}^{ω}[⊥] if and only if ψ ∘ γ is a winning path for σ in μ_{x}.K[x].

We suppose in what follows that ϵ(h_{0}) = σ, otherwise we reason with the equivalent game ⋁ H. Let K_{σ}[x] = ⋁ K[x], i.e. K_{σ}[x] = ⟨⋁ K, x, λ⟩. Define K_{σ}^{n}[x] by induction, as K_{σ}^{0}[x] = x and K_{σ}^{n+1}[x] = K_{σ}^{n}[ K_{σ}[x] ]. Observe that K_{σ}^{n}[⊥] is a subgame of both K_{σ}^{n+1}[⊥] and K_{σ}^{ω}[⊥], i.e. there is a commutative diagram of the form:

[figure: K_{σ}^{n}[⊥]; j_{n}; K_{σ}^{ω}[⊥]; K_{σ}^{n+1}[⊥]; i_{n}; j_{n+1}; K_{σ}^{ω}[⊥]; ‖]

which allows us to identify the game K_{σ}^{n}[⊥] as the truncation of the game K_{σ}^{ω}[⊥] at position (x, n). Under these identifications an infinite play γ is winning for π in K_{σ}^{ω}[⊥] if and only if either it is unbounded, i.e. for all n ≥ 0 there exists an m such that γ(m) = (x, n), or it is bounded and it is a winning infinite play for π in some K_{σ}^{n}[⊥]. We define winning strategies S^{n} in ⟨K_{σ}^{n}[H], H⟩ for n ≥ 1 as follows: if n = 1, from the fact that K[H] ≤ H we deduce that K_{σ}[H] ≤ H so that the strategy S^{1} is given. Suppose we have defined a strategy S^{n} in ⟨K_{σ}^{n}[H], H⟩, then S^{n+1} is defined in the following way: Mediator plays exactly as in S^{n} until a position of the form (x, n, h) is reached; from this position Mediator plays according to the communication strategy using on the left the given strategy S^{1} for ⟨K_{σ}[H], H⟩, beginning at the initial position (x_{0}, h_{0}) and using on the right the strategy residual of S^{n} from position (h_{0}, h) of ⟨K_{σ}^{n}[H], H⟩. Observe that this definition amounts essentially to:

S^{n+1} = ( K_{σ}^{n}[S^{1}] ∘ S^{n})_{\K_{σ}^{n}[H]} .

Observe now that K_{σ}^{n}[⊥] is a sub-game of K_{σ}^{n}[H] and so ⟨K_{σ}^{n}[⊥], H⟩ is a sub-game of ⟨K_{σ}[H], H⟩; moreover the strategies S^{n} can be restricted to winning strategies R^{n} in ⟨K_{σ}^{n}[⊥], H⟩. However, when we look at R^{n} as a strategy in ⟨K_{σ}^{ω}[⊥], H⟩, we see it is not a winning strategy. The reason is that R^{n} is not closed under Opponents’ moves since player σ_{K_{σ}^{ω}[⊥]} on the left could choose a move of the form (x, n, h) → (k_{0}, n+1, h). However, by definition, R^{n} can be extended to the strategy R^{n+1}, hence the strategy R^{ω}, defined as:

R^{ω} = ⋃_{n≥0} R^{n} ,

of ⟨K_{σ}^{ω}[⊥], H⟩, is now closed under Opponents’ moves. It is a winning strategy: every play which is bounded on the left has been played according to a winning strategy R^{n}, hence it is a winning play. On the other hand, every play which is unbounded on the left is a win for π on the left, hence for Mediator. To show that K[ μ_{x}.K[x] ] ≤ μ_{x}.K[x] observe that K_{σ}[ μ_{x}.K[x] ] is a cover of μ_{x}.K[x] and so ⟨K_{σ}[ μ_{x}.K[x] ] , μ_{x}.K[x]⟩ is a cover of ⟨μ_{x}.K[x], μ_{x}.K[x]⟩. Essentially, Mediator can play according to the copycat strategy. This concludes the proof of proposition 4.11.ii. By a dual argument we prove also proposition 4.11.iii. □

We can now state the desired algebraic results.

Definition 4.12 We say that two games G, H ∈ J (P) are equivalent if G ≤ H and H ≤ G. We shall denote by [G] or by [G, λ] the equivalence class of the game G, respectively ⟨G, λ⟩, and by J_{P} the set of those equivalence classes of games.

Definition 4.13 Let f : P ^{}Q be an order preserving function. Define the order preserving function J (f) : J (P) ^{}J (Q) by the formula J (f)⟨G, λ⟩ = ⟨G, f ∘ λ⟩. J (f) is order preserving, because a winning strategy in ⟨G, H⟩ becomes a winning strategy in ⟨J (f)(G), J (f)(H)⟩. It suffices for Mediator to play exactly as in ⟨G, H⟩ and to realize that for a pair of final positions (x, y), x ∈ X_{G} and y ∈ X_{H}, reached by playing in this way, from λ(x) ≤ λ(y) it follows f(λ(x)) ≤ f(λ(y)). J (f) is then well defined over equivalence classes of games in J (P). Hence we obtain an order preserving map J_{f} : J_{P} ^{}J_{Q}, defined as:

J_{f}[G, λ] = [G, f ∘ λ] .

Theorem 4.14 For every ordered set P, J_{P} is a μ-lattice, and, for an order preserving map f : P ^{}Q, J_{f} : J_{P} ^{}J_{Q} is a morphism of μ-lattices. Indeed the construction J is a functor from the category of ordered sets to the category of μ-lattices. Moreover, there exists an embedding η_{P} : P ^{}J_{P} which is natural in P.

Proof. By proposition 4.9, the set J_{P}, with its natural ordering, given by:

[G] ≤ [H] iff G ≤ H ,

is a lattice, for example:

⊤ = [⋀_{∅}] ,
[G_{1}] ∧ [G_{2}] = [⋀_{i∈2} G_{i}] .

More generally, it is possible to associate to each ϕ ∈ A such that a(ϕ) = n a pair (G_{ϕ}, ψ_{ϕ}), where G_{ϕ} ∈ J and ψ_{ϕ} : n ^{≅}^{}X_{G_{ϕ}} is a bijection, such that:

|ϕ|( [H_{1}], …, [H_{n}] ) = [ G_{ϕ}[H_{i}/ψ_{ϕ}(i)] ] ,

for all ordered sets P and for all vectors (H_{1}, …, H_{n}) of games in J (P). Since the definition of those pairs does not depend on the ordered set P, if f : P ^{}Q is an order preserving map, it becomes clear that:

J_{f}( |ϕ|([H_{1}], …, [H_{n}]) ) = |ϕ|( J_{f}[H_{1}], …, J_{f}[H_{n}] ) .

η_{P} is defined by η_{P} (p) = [x, λ^{p}] where λ^{p}(x) = p. Naturality is easily checked as well as the fact that η_{P} is an embedding. □

5 Decidability of the order relation of J_{P}

We observe now that if the order relation of P is decidable, so is the order relation of J (P). Assuming that two equivalence classes are always presented by means of their elements, this will imply the decidability of the order relation of J_{P}. For ease of exposition we shall assume from now on that the order relation of P is decidable. The strategy used to obtain this result relies on well known facts of the theory of infinite games played on finite graphs, this latter theory being closely related to the theory of automata which recognize languages of infinite words or infinite trees. Surveys on the subject are [Tho97] and [Zie98]. The set of infinite winning paths of a game G is usually specified as the set of paths which are accepted by an automaton built from the underlying graph and a given acceptance condition. One of the most powerful acceptance conditions is Muller’s condition: a table F (i.e. a collection F of subsets of G_{0}) is given and it is declared that

γ ∈ W_{σ} if and only if In_{0}(γ) ∈ F ,

where In_{0}(γ) = { g ∈ G_{0} | card{ n | γ(n) = g } = ∞ }. We shall refer to such a game as a Muller game. Moreover, if F and its complement F^{c} are both closed under binary unions, such a game is called a Rabin chain game or parity game. In this case, it becomes possible to specify a finite number of pairs (E_{i}, F_{i}) ⊆ 𝒫(G_{0}) × 𝒫(G_{0}), i = 1, …, n, so that

γ ∈ W_{σ} if and only if ∃i In_{0}(γ) ∩ E_{i} ≠ ∅ , In_{0}(γ) ∩ F_{i} = ∅ .

This way of specifying a set of infinite paths is usually referred to as a Rabin acceptance condition. In the particular case of a Rabin chain game, these pairs can be chosen so that they form a chain: E_{i} ⊆ F_{i} for i = 1, …, n and F_{i} ⊆ E_{i+1} for i = 1, …, n − 1. Given G, H ∈ J (P), we shall construct a finite cover p : K ^{}⟨G, H⟩ such that K is a Muller game. Then, by the main theorem in [GH82], and using ideas contained in [Tho97], we can effectively construct a finite cover p′ : K′ ^{}K so that K′ is a Rabin chain game. Using the fixpoint formula of [EJ91, Wal96], we can then effectively compute the set S of winning positions in K′ for player σ. In order to decide whether player σ has a winning strategy in ⟨G, H⟩, it is then enough to check whether S ∩ (p ∘ p′)^{−1}(g_{0}, h_{0}) ≠ ∅. We need to generalize the notion of Muller game as follows.

Definition 5.1 A game ⟨G_{0}, G_{1}, g_{0}, ϵ, W_{σ}⟩ is Muller-definable by moves if there exists a table F ⊆ 𝒫(G_{1}) such that:

γ ∈ W_{σ} if and only if In_{1}(γ) ∈ F ,

where:

In_{1}(γ) = { g → g′ ∈ G_{1} | card{ n | γ(n → n + 1) = g → g′ } = ∞ } .

Proposition 5.2 Let G, H be games in J (P). The game ⟨G, H⟩ is Muller definable by moves.

Proof. Observe that each move of ⟨G, H⟩ has a unique form (g, h) → (g′, h) for a move g → g′ of G or (g, h) → (g, h′) for a move h → h′ of H. Hence, given α ⊆ ⟨G, H⟩_{1}, we define α_{G} by:

α_{G} = { g → g′ | ∃h ∈ H_{0} s.t.(g, h) → (g′, h) ∈ α }

and similarly we define α_{H}. An infinite path γ in ⟨G, H⟩ satisfies the relation In_{1}(γ)_{G} = In_{1}(γ_{G}), where γ_{G} is the path induced by γ on G. A similar relation holds for γ and γ_{H}. Since it is easily seen that γ_{G} ∈ W_{π} if and only if the set X = In_{1}(γ_{G}) has the property:

1. there exists a return r such that ϵ(r) = σ, the move r → S(r) ∈ X and r is of minimal height among returns r′ such that r′ → S(r′) ∈ X,

and similarly γ_{H} ∈ W_{σ} if and only if the set X = In_{1}(γ_{H}) has the property:

2. there exists a return r such that ϵ(r) = π, the move r → S(r) ∈ X, and r has minimal height among returns r′ such that r′ → S(r′) ∈ X,

it becomes clear that we can define F ⊆ 𝒫⟨G, H⟩_{1} by saying that α ∈ F if and only if α_{G} has the property 1 or α_{H} has the property 2. □

Proposition 5.3 Let G = ⟨G_{0}, G_{1}, g_{0}, ϵ, W_{σ}⟩ be a game which is Muller definable by moves. Suppose that all the sets { τ ∈ G_{1} | cod(τ) = g } are finite. Then there exists a surjective finite cover p : K ^{}G and a table F_{0} ⊆ 𝒫(K_{0}) which makes K into a Muller game.

Proof. For all g ∈ G_{0} we define:

K(g) = \{ \begin{matrix}\{ τ ∈ G_{1} | cod(τ) = g \} , & if this set is not empty , \\ \{∗\} , & otherwise . \end{matrix}

Positions of K are pairs (x, g) with g ∈ G_{0} and x ∈ K(g); moves of K are of the form (x, g) → (g → g′, g′) for a move g → g′ of G and for each x ∈ K(g); essentially the last move which has been played in G is remembered. The morphism of graphs defined by p_{2}(x, g) = g and p_{2}( (x, g) → (g → g′, g′) ) = g → g′ is a finite surjective cover of G. Let F_{1} ⊆ 𝒫(G_{1}) be a table for G and say that α ⊆ K_{0} is an element of F_{0} ⊆ 𝒫(K_{0}) if and only if p_{1}(α) ∈ F_{1}, where p_{1} : K_{0} ^{}G_{1} is the first projection, actually a partial map. Consider an infinite path γ in K. Then In_{0}(γ) ∈ F_{0} if and only if p_{1}(In_{0}(γ)) ∈ F_{1}, by definition of F_{0}. Because of the equality p_{1}(In_{0}(γ)) = In_{1}(p_{2} ∘ γ), the latter relation holds if and only if In_{1}(p_{2} ∘ γ) ∈ F_{1}. □

We can summarize our considerations with the following proposition.

Theorem 5.4 Let G, H ∈ J (P) be two games over P. We can effectively construct a finite cover p : K ^{}⟨G, H⟩ such that the game structure induced by p on K is that of a Rabin chain game. Hence the existence of a winning strategy for Mediator in the game ⟨G, H⟩ can be effectively decided.

6 Freeness of the μ-lattice J_{P}

To prove freeness of the μ-lattice J_{P} we introduce a function EV : J (L) ^{}L, for every μ-lattice L. Such a function induces a μ-lattice morphism EV_{L} : J_{L} ^{}L given that it is well defined on equivalence classes. Having proved that, and also noticed that EV_{L} ∘ η_{L} = Id_{L}, we can prove freeness as follows. Let f : P ^{}L be an order preserving map, where L is a μ-lattice. Then EV_{L} ∘ J_{f} : J_{P} ^{}L is a μ-lattice morphism with the property that (EV_{L} ∘ J_{f}) ∘ η_{P} = f, by naturality of η and the relation EV_{L} ∘ η_{L} = Id_{L}. This morphism is also the only morphism f′ : J_{P} ^{}L such that f′ ∘ η_{P} = f, since J_{P} is generated by P. Therefore the μ-lattice J_{P} is free over P. The main problem will be to show that EV is order preserving, i.e. if G, H ∈ J (L) and G ≤ H then EV (G) ≤ EV (H).

Lemma 6.1 Let L be a μ-lattice, and let EV : J (L) ^{}L be a function satisfying the following conditions:

\begin{aligned}EV ( η( l) ) & = & l , \\ EV ( ⋀_{i∈I} G_{i} ) & = & ⋀_{i∈I} EV ( G_{i} ) , \\ EV ( ⋁_{i∈I} G_{i} ) & = & ⋁_{i∈I} EV ( G_{i} ) , \\ EV ( μ_{x}.G[x] ) & = & μ_{z}.EV ( G[z] ) , \\ EV ( ν_{x}.G[x] ) & = & ν_{z}.EV ( G[z] ) . \end{aligned}

Here η( l) = ⟨x, λ^{l}⟩, where λ^{l}(x) = l, and EV ( G[z] ) : L ^{}L is the function which maps l ∈ L to EV ( G[ η( l) ] ). If EV preserves the order, then the induced operator EV_{L} : J_{L} ^{}L, defined by:

EV_{L}[G] = EV ( G) ,

is a morphism of μ-lattices.

Proof. Suppose EV preserves the order. Then EV_{L} is a morphism of lattices, for example:

EV_{L}( ⋀_{i∈I}[G_{i}] ) = EV_{L} [ ⋀_{i∈I} G_{i} ]
= EV ( ⋀_{i∈I} G_{i} )
= ⋀_{i∈I} EV ( G_{i} )
= ⋀_{i∈I} EV_{L} [G_{i}] .

Let ϕ ∈ A be such that a(ϕ) = n + 1 and let (G_{ϕ}, ψ_{ϕ}) be as in the proof of proposition 4.14; suppose also that |ϕ| ∘ EV_{L}^{n+1} = EV_{L} ∘ |ϕ|. Let (H_{1}, …, H_{n}) ∈ J (L)^{n} and s ∈ {1, …, n + 1}. Define ψ′ : n ^{}X_{G_{ϕ}} to be ψ′(i) = ψ_{ϕ}(i) if i < s, ψ′(i) = ψ_{ϕ}(i + 1) if i ≥ s and let x = ψ_{ϕ}(s). Then:

μ_{z}.|ϕ|( [H_{1}], …, [H_{s−1}], z, [H_{s}], …, [H_{n}] )
= [ μ_{x}.(G_{ϕ}[H_{i}/ψ′(i)])[x] ] .

By the assumptions on EV we have:

EV ( μ_{x}.(G_{ϕ}[H_{i}/ψ′(i)])[x] ) = μ_{z}.EV ( G_{ϕ}[H_{i}/ψ′(i)][z] )

and moreover:

EV ( G_{ϕ}[H_{i}/ψ′(i)][z] )

= |ϕ|( EV_{L}[H_{1}], …, EV_{L}[H_{s−1}], z, EV_{L}[H_{s}], …, EV_{L}[H_{n}] ) ,

which holds because of the relation:

EV ( G_{ϕ}[H_{i}/ψ′(i)][η( l)] )
= EV_{L}( |ϕ|([H_{1}], …, [H_{s−1}], [η( l)], [H_{s−1}], …, [H_{n}] )

and because of the facts |ϕ| ∘ EV_{L}^{n+1} = EV_{L} ∘ |ϕ| and EV ( η( l) ) = l. Hence least prefix-points are preserved. A similar argument is used for greatest postfix-points, and the desired preservation of all fix-points is obtained. The criterion of lemma 3.5 is satisfied so that EV_{L} is a μlattice morphism. □

6.1 Theory of the evaluation

We recall that a game-operator on J (P) is a triple ⟨G, x, λ⟩ where G ∈ J, x ∈ X_{G} and λ : X_{G} \ {x} ^{}P. We write ⟨G[x], λ⟩ for such a game-operator, or G[x] to simplify the notation. If p ∈ P, we obtain a game ⟨G[x], λ^{p}⟩ ∈ J (P) by extending the definition of λ to all of X_{G}. λ^{p} : X_{G} ^{}P is defined by:

λ^{p}(y) = \{ \begin{matrix}p, & y = x , \\ λ(y), & otherwise . \end{matrix}

Let H be a sub-game of G. If λ is a partial function from X_{G} to P, let λ_{H} be the restriction of λ to X_{H}. If x ∈ X_{H} and λ : X_{G} \ {x} ^{}P, we observe that ( λ_{H} )^{p} = ( λ^{p})_{H}, and we shall write only λ_{H}^{p} for the two members of the equality. Observe that the game ⟨G[x], λ^{p}⟩ is isomorphic to the game G[η(p)], which we shall often write as G[p]. In the following let L be a fixed μ-lattice. We shall develop first a rigorous theory of the evaluation, and then switch to a simpler notation and restate properties of evaluation in this notation with the goal of making the main proof of 6.14 readable.

Definition 6.2 For all partial games G ∈ J we define EV_{G} : L^{X_{G}} ^{}L by induction on the structure in the following way:

\begin{aligned}EV_{x}( λ) & = & λ(x) , \\ EV_{⋀_{i∈I} G_{i}}( λ) & = & ⋀_{i∈I} EV_{G_{i}}( λ_{G_{i}}) , \\ EV_{⋁_{i∈I} G_{i}}( λ) & = & ⋁_{i∈I} EV_{G_{i}}( λ_{G_{i}}) , \\ EV_{μ_{x}.G[x]}( λ) & = & μ_{z}.EV_{G[x]}( λ^{z}) , \\ EV_{ν_{x}.G[x]}( λ) & = & ν_{z}.EV_{G[x]}( λ^{z}) . \end{aligned}

For all G ∈ J we extend the definition of EV to all positions g of G by setting, for the initial position g_{0}:

EV_{G,g_{0}}(λ) = EV_{G}(λ) ,

and for a position g ≠ g_{0}:

\begin{aligned}EV_{⋀_{i∈I} G_{i},g}( λ) & = & EV_{G_{ig} ,g}( λ_{G_{ig}} ) , \\ EV_{⋁_{i∈I} G_{i},g}( λ) & = & EV_{G_{ig} ,g}( λ_{G_{ig}} ) , \\ EV_{μ_{x}.G[x],g}( λ) & = & EV_{G[x],g}( λ^{μ}) , \\ EV_{ν_{x}.G[x],g}( λ) & = & EV_{G[x],g}( λ^{ν} ) . \end{aligned}

where i_{g} is the only index i ∈ I such that g is a position of G_{i}, μ = μ_{z}.EV_{G[x]}(λ^{z}) and ν = ν_{z}.EV_{G[x]}(λ^{z}).

Remark 6.3 By induction, for any partial game G ∈ J, if cardX_{G} = n we can find a bijection ψ : n ^{≅}^{}X_{G} and a term ϕ ∈ A such that a(ϕ) = n and such that:

EV_{G}( λ) = |ϕ|( λ ∘ ψ) .

It becomes clear that the definition of EV makes sense in that the required fix-points exist.

Proposition 6.4 For every game G ∈ J and position g ∈ G_{0} the function EV_{G,g} : L^{X_{G}} ^{}L is order preserving.

Proof. That’s evident if g is the root by the remark 6.3; otherwise it is proved by induction on the structure of games in the class J. □

Proposition 6.5 Let G = K[H/x] be a partial game in J. Then the relation X_{G} = (X_{K} \ {x}) ∪ X_{H} is true. Let λ : X_{G} ^{}L be given and let λ_{K} and λ_{H} be the restrictions of λ to X_{K} \{x} and to X_{H} respectively. Let h_{0} be the root of H and set e = EV_{H,h_{0}}(λ_{H}). For all positions k of K it is true that:

EV_{G,k}( λ) = EV_{K,k}( λ_{K}^{e} ) ,

and for all positions h of H it is true that:

EV_{G,h}( λ) = EV_{H,h}( λ_{H} ) .

Proof. By induction on the structure of K. □

We can now define EV ⟨G, λ⟩ for a game ⟨G, λ⟩ ∈ J (L). Since every position is the starting position of a game we actually evaluate every position g of the game ⟨G, λ⟩.

Definition 6.6 Let ⟨G, λ⟩ ∈ J (L) be a game over L and let g be a position of G. We set:

EV_{⟨G,λ⟩}(g) = EV_{G,g}( λ) .

Moreover:

EV ⟨G, λ⟩ = EV_{⟨G,λ⟩}(g_{0}) .

Proposition 6.7 The function EV : J (L) ^{}L satisfies the properties of lemma 6.1. Hence, if it preserves the order, it induces a μ-lattice morphism EV_{L} : J_{L} ^{}L such that EV_{L} ∘ η_{L} = Id_{L}.

Proof. A reformulation of definition 6.2. □

In the next section we shall use the following properties of the evaluation of games and their positions.

Proposition 6.8 Let K[x] be a game-operator on J (L) and let H ∈ J (L) be a game over L. Let G = K[H] be the game obtained by substitution of H for x in K[x]. For all positions h of H it is true that:

EV_{G}(h) = EV_{H}(h) .

Moreover, if h_{0} is the root of H and e = EV_{H}(h_{0}), then for all positions k of K[x] it is true that:

EV_{G}(k) = EV_{K[e]}(g) .

Proof. A reformulation of proposition 6.5, observing that the game K[η(e)] is isomorphic to the game ⟨K[x], λ_{K}^{e}⟩. □

Proposition 6.9 Let G ∈ J (L) be a game with no returns and let g be a position of G. Then:

EV_{G}( g) = \{ \begin{matrix}λ(g), & ϵ(g) = 0, \\ ⋁_{g→g′} EV_{G}( g′), & ϵ(g) = σ, \\ ⋀_{g→g′} EV_{G}( g′), & ϵ(g) = π . \end{matrix}

Proof. The graph of G is a tree, hence for all g in G we can represent G as G = G_{g}[G^{g}] where G^{g} is the subtree of root g. The result is obtained using proposition 6.8 and the properties of the evaluation as in 6.1. □

Proposition 6.10 Let G[x] be a game-operator on J (L). For a position g ∈ G, the function EV_{G[z]}(g) which maps l ∈ L to EV_{G[l]}(g) is order preserving. Let μ = μ_{z}.EV_{G[z],g_{0}} and ν = ν_{z}.EV_{G[z],g_{0}}. For all positions g of μ_{x}.G[x] it is true that:

EV_{μ_{x}.G[x]}(g) = EV_{G[μ]}(g) ,

and for all positions g of ν_{x}.G[x] it is true that:

EV_{ν_{x}.G[x]}(g) = EV_{G[ν]}(g) .

Proof. Using a more detailed notation, we have to prove that if l ≤ l′ then EV_{G[x],g}( λ^{l}) ≤ EV_{G[x],g}( λ^{l′}), which is a consequence of λ^{l} ≤ λ^{l′} and the fact that EV_{G[x],g} is order preserving. For the same reason, we have seen that μ and ν exist and we must prove only the last part of the proposition. If g is not the initial position then it’s true by definition. If g is the initial position it’s a consequence of proposition 6.5. □

6.2 Evaluation strategies

The general tool for proving the main result 6.14 is the following. Given a game G ∈ J (L), where L is a μ-lattice, either the game G is acyclic, i.e. its underlying graph is a tree with no returns, or G contains a return. In the latter case we shall look for a minimal return x, leading to a representation of G as:

G = G_{x}[ Q_{x}.G^{S(x)}[x] ] ,

where G_{x}[x] and G^{S(x)}[x] are two game-operators. Q = μ or Q = ν depending on the fact that ϵ(x) = σ or ϵ(x) = π; in the first case we shall say that x is a μ-return, in the latter that x is a ν-return. Given an evaluation strategy S, i.e. a winning strategy in a game {G, H} similar to ⟨G, H⟩, we shall transform it into a set of strategies {S_{i}}_{i∈I}, each one on a game of the form {G_{x}[ l], H} or {G^{S(x)}[ l′], H}, with l, l′ ∈ L well chosen. We obtain the strategies S_{i} by cutting transitions s → s′ in S related to moves (x, h) → (S(x), h) in the game {G, H}. The games G_{x}[ l] and G^{S(x)}[ l′] have strictly less returns than G and we can use an induction hypothesis. The previous study of the evaluation of games and positions has been necessary, since evaluation strategies depend on it.

Definition 6.11 Let G, H be games in J (L). An evaluation strategy on {G, H} is a pair (S, ψ) where S is a finite reachable pointed graph and ψ : S ^{}⟨G, H⟩ is a morphism of graphs. The following conditions are satisfied:

1. If s ∈ S is a final vertex, i.e. { s′ | s → s′ } = ∅, such that ψ(s) = (g, h), then EV_{G}(g) ≤ EV_{H}(h).

2. If s is not a final vertex, ϵ(ψ(s)) = π, and ψ(s) → (g, h), then there exists a unique transition s → s′ of S such that ψ(s → s′) = ψ(s) → (g, h).

3. Every proper cycle γ of S induces a winning cycle ψ ∘ γ in ⟨G, H⟩, meaning that either the projection of ψ ∘ γ on G is a proper cycle where the minimal return is a μ-return, or the projection of ψ ∘ γ on H is a proper cycle where the minimal return is a ν-return.

Remark 6.12 An evaluation strategy is essentially a bounded memory winning strategy for Mediator in a game {G, H}, played on the same boards and with the same rules as for the game ⟨G, H⟩, except that both players have the right to stop the game at any position (g, h). In such a case, Mediator wins if EV_{G}(g) ≤ EV_{H}(h) and the Opponents win if EV_{G}(g) ≰ EV_{H}(h). The initial position of the games {G, H} is not necessarily the pair (g_{0}, h_{0}). Indeed we do not require that ψ(s_{0}) = (g_{0}, h_{0}), if s_{0} is the point of S.

Lemma 6.13 Let ⟨S, K, ψ⟩ be a bounded memory winning strategy for Mediator in the game ⟨G, H⟩ and let ψ_{S} be the restriction of ψ to S. The pair (S, ψ_{S}) is an evaluation strategy on {G, H}.

Proof. Recall that ⟨K, ψ⟩ is a finite cover of ⟨G, H⟩ and S is a memoryless winning strategy in K, i.e. a sub-graph of K containing the initial position k_{0} of K, reachable from k_{0}, with the following additional properties: ψ(k_{0}) = (g_{0}, h_{0}); if s ∈ S, ϵ(s) = π and s → k is a move of K, then s → k is also a transition of S; if s ∈ S and ϵ(s) = σ, then there exists a transition s → s′ in S; every infinite path in S is a winning play for player σ in K. It is easily checked that all the conditions defining an evaluation strategy are satisfied. □

Proposition 6.14 Let G, H be games in J (L) and let (S, ψ) be an evaluation strategy on {G, H}. For every vertex s of S, if ψ(s) = (g, h), then EV_{G}(g) ≤ EV_{H}(h).

Before the proof of the proposition, we shall glance over its consequences.

Theorem 6.15 Let G, H be games in J (L) such that G ≤ H. Then EV (G) ≤ EV (H).

Proof. If G ≤ H then there exists a winning strategy for Mediator in the game ⟨G, H⟩. By the results of section 5 we can suppose that it is a bounded memory strategy ⟨S, K, ψ⟩, and, according to the lemma 6.13, the pair (S, ψ_{S}) is an evaluation strategy on {G, H}, where ψ_{S} is the restriction of ψ to S. The initial point k_{0} of S is such that ψ(k_{0}) = (g_{0}, h_{0}), hence, because of proposition 6.14, it is true that EV_{G}(g_{0}) ≤ EV_{H}(h_{0}). Because EV (G) = EV_{G}(g_{0}) and EV (H) = EV_{H}(h_{0}), we obtain the result. □

Theorem 6.16 Let P be an ordered set. The ordered set J_{P} is the free μ-lattice over P.

Proof. Let L be a μ-lattice. We have seen that if f : P ^{}L is order preserving, then J_{f} : J_{P} ^{}J_{L} is a μ-lattice morphism. It is enough then to show that there exists a morphism of μ-lattices ϵ_{L} : J_{L} ^{}L such that ϵ_{L} ∘ η_{L} = Id_{L}, because in this case we obtain a morphism of μ-lattices ϵ_{L}∘J_{f} : J_{P} ^{}L such that ϵ_{L}∘J_{f} ∘η_{P} = f. This morphism is surely unique among those morphism f′ : J_{P} ^{}L such that f′∘η_{P} = f, because J_{P} is generated by P. The function EV : J (L) ^{}L induces a morphism of μ-lattices EV_{L} : J_{L} ^{}L with the desired property EV_{L} ∘ η_{L} = Id_{L} if it is well defined on equivalence classes, which is the same as saying it preserves the order of J (L). Theorem 6.15 states exactly that. □

We shall need the following definition.

Definition 6.17 Let ⟨G_{0}, G_{1}⟩ be a graph and let g_{0} ∈ G_{0}. The subgraph K of G is defined by saying that a vertex g ∈ G_{0} is in K_{0} if and only if there exists a path from g_{0} to g in ⟨G_{0}, G_{1}⟩, and that a transition τ ∈ G_{1} is in K_{1} if and only if dom(τ) ∈ K_{0}. We shall denote the pointed graph K by \overline{⟨G_{0}, G_{1}⟩, g_{0}} and call it the sub-graph of G reachable from g_{0}.

Proof of proposition 6.14. Let ρ(G) be the number of returns in a game G, the proof is by induction on ρ(G) + ρ(H). Suppose first that ρ(G) + ρ(H) = 0. Let (S, ψ) be a given evaluation strategy. In this case S is a well founded graph, i.e. there are no infinite paths s_{0} → s_{1} → … in S. Such a path would induce, by projections, an infinite path on G or an infinite path on H, which is impossible in both cases. We can prove the proposition by induction on the well founded structure of S. Let s ∈ S be such that ψ(s) = (g, h).

If s is a final vertex then the proposition is true by the definition of evaluation strategy. Let s be a vertex which is not final. If ϵ(ψ(s)) = σ, choose a transition s → s′ and suppose that ψ(s → s′) = (g, h) → (g, h′). Then ϵ(h) = σ and EV_{H}(h) = ⋁_{h→h′} EV_{H}(h′). Because EV_{G}(g) ≤ EV_{H}(h′) and EV_{H}(h′) ≤_{H} EV (h) we obtain that EV_{G}(g) ≤ EV_{H}(h). A similar argument is used in case ψ(s → s′) = (g, h) → (g′, h). If ϵ(ψ(s)) = π, then ϵ(g) = σ or ϵ(h) = π; (ϵ(g), ϵ(h)) ≠ (0, 0) because s is not final. Consider the case where ϵ(h) = π. Let {h_{i}}_{i∈I} be the set of successors of h and recall that EV_{H}(h) = ⋀_{i∈I} EV_{H}(h_{i}). For all i ∈ I (g, h) → (g, h_{i}) is a transition of ⟨G, H⟩, hence this transition is lifted to a transition s → s_{i} with ψ(s_{i}) = (g, h_{i}). By the inductive hypothesis EV_{G}(g) ≤ EV_{H}(h_{i}), for all i ∈ I, therefore EV_{G}(g) ≤ EV_{H}(h). A similar argument is used if ϵ(g) = σ. Suppose now that ρ(G) + ρ(H) > 0. We shall distinguish two cases:

1. either there exists a μ-return among minimal returns of G, or there exists a ν-return among minimal returns of H.

2. every minimal return of G is a ν-return and every minimal return of H is a μ-return.

First case, suppose there exists a μ-return among minimal returns of G, call it x. We can cut the game G into two game-operators G_{x}[x] and G^{S(x)}[x], with starting positions g_{0} and g_{1} = S(x) respectively, so that G = G_{x}[ μ_{x}.G^{S(x)}[x] ]. Let (S, ψ) be an evaluation strategy on {G, H}, and call A ⊆ S_{1} the set of transitions s → s′ such that ψ(s → s′) = (x, h) → (g_{1}, h) for some h. If α ∈ A we write ψ(α) = (x, h_{α}) → (g_{1}, h_{α}). We consider the graph S′, where S′_{0} = S_{0} and S′_{1} = S_{1} \ A: by cutting transitions of A we possibly transform vertexes of the form dom(α), α ∈ A, into final ones. For all α ∈ A let S_{α} = \overline{S′, cod(α)} be the sub-graph of S′ reachable from cod(α). The restriction of ψ to S_{α} induces an evaluation strategy (S_{α}, ψ) on {G^{S(x)}[ l], H} where:

l = EV_{G}(x) ∧ ⋀_{α∈A} EV_{H}(h_{α}) .

Observe that this meet exists because the set {h_{α}}_{α∈A} is finite. That each (S_{α}, ψ) is an evaluation strategy is easily seen. Essentially we must check that a final vertex s of S_{α} such that ψ(s) = (g, h) satisfies EV_{G^{S(x)}[ l]}(g) ≤ EV_{H}(h). Now s could be a new final vertex in which case g = x and h = h_{α} for some α. Hence EV_{G^{S(x)}[ l]}(x) = l ≤ EV_{H}(h_{α}), by the choice of l. Or s could be an old final vertex, in which case we know that EV_{G}(g) ≤ EV_{H}(h). But then, since l ≤ EV_{G}(x), setting e = EV_{G}(x) and using the properties of the evaluation, we obtain that EV_{G^{S(x)}[ l]}(g) ≤ EV_{G^{S(x)}[ e]}(g) = EV_{G}(g) ≤ EV_{H}(h).

Since ρ(G^{S(x)}[ l]) < ρ(G) we can use the inductive hypothesis and deduce that the proposition is true for the vertex cod(α), for each α. ψ(cod(α)) = (g_{1}, h_{α}) and, because of EV_{G^{S(x)}[ l]}(g_{1}) = EV (G^{S(x)}[ l]), for all α ∈ A we obtain:

EV (G^{S(x)}[ l]) ≤ EV_{H}(h_{α}) .

Moreover, because of l ≤ EV_{G}(x) and EV_{G}(x) = μ_{z}.EV (G^{S(x)}[z]), we see that:

EV (G^{S(x)}[ l]) ≤ EV_{G}(x) .

Hence:

EV (G^{S(x)}[ l]) ≤ EV_{G}(x) ∧ ⋀_{α∈A} EV_{H}(h_{α}) ,

i.e. l = EV_{G}(x) ∧ ⋀_{α∈A} EV_{H}(h_{α}) is a prefix-point of the operator EV (G^{S(x)}[z]) and its least prefix-point EV_{G}(x) is less then l. Since l ≤ EV_{H}(h_{α}) we deduce that for all α ∈ A:

EV_{G}(x) ≤ EV_{H}(h_{α}) . (1)

Consider now the sub-graphs S_{0} = \overline{S, s_{0}} of S′ reachable from s_{0} and, for each α ∈ A, the sub-graphs S_{α} of S′ reachable from cod(α). Because of relation 1, the pairs (S_{0}, ψ), (S_{α}, ψ) are evaluation strategies on either {G_{x}[e], H} or {G^{S(x)}[e], H}, where now:

e = EV_{G}(x) .

Because both ρ(G_{x}[e]) < ρ(G) and ρ(G^{S(x)}[e]) < ρ(G), the proposition is true for (S_{0}, ψ) and for all the (S_{α}, ψ), α ∈ A. Because S is reachable, each vertex s ∈ S is in one of the (S_{j}, ψ), j ∈ {0} ∪ A, and, eventually, if ψ(s) = (g, h) we obtain that EV_{G}(g) ≤ EV_{H}(h) since EV_{G_{x}[e]}(g) = EV_{G}(g) and EV_{G^{S(x)}[e]}(g) = EV_{G}(g). A dual argument is used in case there exists a ν-return among minimal returns of H. Second case, every minimal return in G is a ν-return and every minimal return in H is a μ-return.

Let (S, ψ) be an evaluation strategy on {G, H}, and let A be the set of transitions s → s′ such that ψ(s → s′) = (x, h) → (S(x), h) or ψ(s → s′) = (g, y) → (g, S(y)), for a minimal return x in G or a minimal return y in H. If α ∈ A, let S^{α} = \overline{S, cod(α)} be the sub-graph of S reachable from cod(α); moreover let S^{0} = S. We shall consider the collection of pointed graphs {S^{i}}_{i∈A∪{0}} and prove the implication

∀_{j}( S^{j} ⊂ S^{i} ⇒ P (S^{j}) ) ⇒ P (S^{i}) ,

where ⊂ is the strict inclusion as sub-graphs of S, i.e. S^{j} ⊂ S^{i} if and only if S^{j} ⊆ S^{i} but S^{j} ≠ S^{i}, and P (S^{j}) is the property stating that every vertex s of S^{j} is such that ψ(s) = (g, h) implies EV_{G}(g) ≤ EV_{H}(h). Choose i ∈ A ∪ {0} and suppose that for all α ∈ A such that S^{α} is a proper sub-graph of S^{i} it has been proved that if s is a vertex of S^{α} and ψ(s) = (g, h), then EV_{G}(g) ≤ EV_{H}(h). Let A^{i} ⊆ A be the set of those transitions α of S^{i} such that S^{α} ⊂ S^{i} and define as usual the graph S′ by cutting transitions of A^{i} from S^{i}, i.e. S′_{0} = S_{0}^{i}, S′_{1} = S_{1}^{i} \ A^{i}; eventually, define S_{i} = \overline{S′, s_{0}^{i}} as the sub-graph of S′ reachable from the point s_{0}^{i} of S^{i}. Using the restriction of ψ to S_{i}, we shall enrich S_{i} with an evaluation strategy structure on {G′, H′}, where G′, H′ are two games obtained from G and H respectively, such that ρ(G′) + ρ(H′) < ρ(G) + ρ(H) and such that EV_{G′}(g) = EV_{G}(g) and EV_{H′}(h) = EV_{H}(h) for all positions g ∈ G′ and h ∈ H′. Using the inductive hypothesis, we will be able to deduce that if s is a vertex of S^{i} and ψ(s) = (g, h), then EV_{G}(g) ≤ EV_{H}(h). We first claim that: either there exists a minimal return x from G such that if α ∈ A is a transition of S_{i}, then ψ(α) ≠ (x, h) → (S(x), h), or there exists a minimal return y from H such that if α ∈ A is a transition of S_{i}, then ψ(α) ≠ (g, y) → (g, S(y)). To see this, suppose first that ρ(G) > 0 and ρ(H) > 0. If there are two transitions α_{1}, α_{2} from A in S_{i} then they are related to the same minimal return. That’s because S^{α_{1}} = S^{i} = S^{α_{2}} whence we can find paths s_{0}^{i} →^{∗} dom(α_{k}), cod(α_{k}) →^{∗} s_{0}^{i}, k = 1, 2, and a proper cycle γ on which both α_{1} and α_{2} lie. If ψ(α_{1}) = (x, h) → (S(x), h), then also ψ(α_{2}) = (x, h′) → (S(x), h′). If the return of α_{2} were on H, then the cycle γ would contradict the condition on cycles for an evaluation strategy. Hence the return of α_{2} is on G, and by minimality it is the same return of α_{1}. In order to satisfy the claim, we can choose a minimal return from H, because ρ(H) > 0. If ψ(α_{1}) = (g, y) → (g, S(y)), then we can choose a minimal return from G. Similarly, suppose that ρ(G) = 0 or ρ(H) = 0, say the latter.

We claim that there are no transitions α from A in S_{i}. In such a case, from S^{α} = S^{i} we deduce the existence of paths s_{0}^{i} →^{∗} dom(α) and cod(α) →^{∗} s_{0}^{i} and hence the existence of a proper cycle γ on which α lies; however γ contradicts the condition on cycles, since there are no possible ν-returns on H. In order to satisfy the claim, we can choose any minimal return from G. Suppose that there exists a minimal return y from H such that if α ∈ A is a transition of S_{i}, then ψ(α) ≠ (g, y) → (g, S(y)); represent then H as H_{y}[ μ_{y}.H^{S(y)}[y] ]. Let e = EV_{H}(y), the restriction of ψ to S_{i} induces an evaluation strategy (S_{i}, ψ) on {G, H′} where H′ = H_{y}[e] or H′ = H^{S(y)}[e], depending on the fact that ψ(s_{0}^{i}) = (g, h) and h is a position of H_{y} or H^{S(y)}. In order to make sure that (S_{i}, ψ) is an evaluation strategy, observe that EV_{H′}(h) = EV_{H}(h) for all positions h of H′ and that a new final vertex s is of the form dom(α) for some α ∈ A such that S^{α} ⊂ S^{i}. If ψ(α) = (x′, h) → (S(x′), h), then EV_{G}(x′) = EV_{G}(S(x′)) ≤ EV_{H}(h) = EV_{H′}(h); if ψ(α) = (g, y′) → (g, S(y′)), then EV_{G}(g) ≤ EV_{H}(S(y′)) = EV_{H}(y′) = EV_{H′}(y′). We can reason similarly if we find a minimal return x from G with the property that if α ∈ A is a transition of S_{i} then ψ(α) ≠ (x, h) → (S(x), h) in order to enrich S_{i} with an evaluation strategy structure with the desired properties. □

7 A completeness theorem

In this section we shall show that a free μ-lattice can be embedded into a complete lattice. There are two different senses in which this result can be thought of as a completeness theorem. The first part of the theorem simply emphasizes the fact that a class of μ-lattices, which we call founded μ-lattices, can be embedded into complete lattices. On the other hand, by showing that free μ-lattices are founded and, consequently, that they can be embedded into complete lattices, the theorem says also that complete lattices generate the quasivariety of μ-lattices. From a logical perspective one would say that a particular semantics for μ-lattice terms, i.e. the semantics of complete lattices, is complete. An interesting principle, as well as its dual, is a consequence of completeness: if you want to prove that a property is universally true about the least prefix-point of a unary operator ϕ built up from meets, joins and fix-point operators, you can do it by assuming that:

μ_{z}.ϕ(z) = ⋁_{α∈Ord} ϕ^{α}(⊥) ,

where ϕ^{α}(⊥) is defined in the usual way in 7.6 below. Essentially, you are allowed to reason by transfinite induction. The above relation between μ-lattices and complete lattices is surprising. For example, it is well known that free complete lattices do not exist, while partially ordered proper classes, with every set-indexed join and meet and with the desired universal property, can be described as in [Hal64]. These proper classes need not to have the structure of a μ-lattice: the usual formula expressing the least fix-point of an order preserving function as the meet of all its prefix-points is no longer useful, since the prefix-points could form a proper class too. Whitman’s proof [Whi42] that the polynomial

ϕ(z) = a ∨ (b ∧ (c ∨ (a ∧ (b ∨ (c ∧ z)))))

has no fix-point in the free lattice on three generators a, b, c can be generalized to show that the same polynomial has no fix-point in what could be called (in an abuse of definition) the free complete lattice on three generators.

Proposition 7.1 Suppose the Opponents have a winning strategy in the game ⟨μ_{x}.K[x], H⟩, then there exists an integer k ≥ 0 and a winning strategy for the Opponents in the game ⟨K^{k}[⊥], H⟩.

Proof. (cf. the proof of proposition 4.11.ii). We shall show that there exists a winning strategy for the Opponents in a game ⟨K_{σ}^{k}[⊥], H⟩, and the result will follow from the fact that the game K_{σ}^{k}[⊥] is equivalent to the game K^{k}[⊥], which is easily proved by induction. We consider again the cover ⟨K_{σ}^{ω}[⊥], ψ⟩ of the game μ_{x}.K[x] and the cover of ⟨μ_{x}.K[x], H⟩ induced by the operation ⟨ , H⟩. Recall also that ⟨K_{σ}^{k}[⊥], H⟩ is a sub-game of ⟨K_{σ}^{ω}[⊥], H⟩; by the covering relation, a winning strategy for the Opponents in ⟨μ_{x}.K[x], H⟩ induces a winning strategy for the Opponents in the game ⟨K_{σ}^{ω}[⊥], H⟩ and we want to know when this strategy can be restricted to a winning strategy for the Opponents in the game ⟨K_{σ}^{k}[⊥], H⟩.

Definition 7.2 Let γ : n̂ ^{}⟨μ_{x}.K[x], H⟩ be a play beginning at the initial position, i.e. such that γ(0) = (g_{0}, h_{0}) and let γ′ : n̂ ^{}⟨K_{σ}^{ω}[⊥], H⟩ be its unique lifting with the property that γ′(0) = (g_{0}, 0, h_{0}) and ⟨ψ, H⟩∘ γ′ = γ. Define #γ by saying that:

#γ = m if γ′(n) = (g, m, h) .

Lemma 7.3 Let S be a winning strategy for the Opponents in the game ⟨μ_{x}.K[x], H⟩ such that every play γ, played according to S, is such that #γ ≤ k. Then S induces a winning strategy S′ for the Opponents in the game ⟨K_{σ}^{k}[⊥], H⟩.

Proof. Consider the commutative diagrams:

[figure: T ( ⟨K_{σ}^{k}[⊥], H⟩); i_{∗}; T ( ⟨K_{σ}^{ω}[⊥], H⟩); ⟨ψ,H⟩_{∗} ; ≅; T ( ⟨μ_{x}.K[x], H⟩); ⟨K_{σ}^{k}[⊥], H⟩; ev; i; ⟨K_{σ}^{ω}[⊥], H⟩; ev; ⟨ψ,H⟩; ⟨μ_{x}.K[x], H⟩; ev],

where f_{∗}(γ, n) = (f ∘ γ, n). Because ⟨ψ, H⟩ is a cover, ⟨ψ, H⟩_{∗} is the canonical isomorphism between the unfolding trees. Let S′ the tree of all liftings of paths in S. Since every path γ′ of length n of S′ is such that if γ′(n) = (g, m, h) then m ≤ k, we see that S′ is also a sub-tree of T ( ⟨K_{σ}^{k}[⊥], H⟩), hence also a sub-game of T ( ⟨K_{σ}^{k}[⊥], H⟩). It follows immediately that S′ is a π-game as a sub-game of T ( ⟨K_{σ}^{k}[⊥], H⟩), since this is a property that does not depend on the embedding of S′. For example, let γ′ be a play of length n of the strategy S′, let γ′(n) = (g, s, h) be the position so reached and suppose that ϵ(g, s, h) = π. Player π, the Opponents, can continue this play in the game ⟨K_{σ}^{ω}[⊥], H⟩, let’s say with a move (g, s, h) → (g′, s′, h′). This move is also a move of ⟨K_{σ}^{k}[⊥], H⟩ except in the case s′ > k, which is impossible by the assumptions on S. Also, in order to see that an infinite play γ′ is in W_{π}, it suffices to observe that i ∘ γ′ has been played according to S′ so that i ∘ γ′ is in W_{π}, and then use the fact that i is a morphism of games. Eventually, S′ is σ-open since S is σ-open in T ( ⟨K_{σ}^{ω}[⊥], H⟩) and so is T ( ⟨K_{σ}^{k}[⊥], H⟩) as a sub-game of T ( ⟨K_{σ}^{ω}[⊥], H⟩). To check the last assertion it is enough to check that ⟨K_{σ}^{k}[⊥], H⟩ is σ-open as a sub-game of ⟨K_{σ}^{ω}[⊥], H⟩: if (g, n, h) is a position of ⟨K_{σ}^{k}[⊥], H⟩ such that ϵ(g, n, h) = σ and if there exists a move (g, n, h) → (g′, n′, h′) then this move is a move of ⟨K_{σ}^{k}[⊥], H⟩. That’s because n ≤ k and if n′ = k + 1 then the move (g, n, h) → (g′, n′, h′) is (x, k, h) → (S(x), k + 1, h). However, ϵ(x, k, h) = π, because ϵ(x) = σ. □

Lemma 7.4 Let ⟨S, K, ψ⟩ be a bounded memory winning strategy for the Opponents in the game ⟨μ_{x}.K[x], H⟩. Define k as:

k = card ψ^{−1}{ (x, h) → (S(x), h) | h ∈ H_{0} } .

For all plays γ which are the outcome of playing according to S it is the case that #γ ≤ k.

Proof. Let γ be a finite play which is the outcome of playing according to S, say γ = ψ ∘ γ′ where γ′ is a path in the graph S, and suppose that #γ > k. We can deduce that γ′ has visited at least twice a move τ : k → k′ such that ψ(k → k′) = (x, h) → (S(x), h). We can factor γ′ as γ_{2} ∘ τ ∘ γ_{1} ∘ τ ∘ γ_{0}, and obtain an infinite play (γ_{1} ∘ τ)^{ω} in S by repeating infinitely often the proper cycle γ_{1} ∘ τ of S. However, this play visits infinitely often the move x → g_{0}, hence it is an infinite play which is a Mediator’s win in ⟨μ_{x}.K[x], H⟩. This contradicts the fact that ⟨S, K, ψ⟩ is a winning strategy for the Opponents. □

We can continue the proof of proposition 7.1. We obtain the proposition if we observe that if the Opponents have a winning strategy in the game ⟨μ_{x}.K[x], H⟩, then they have a bounded memory winning strategy ⟨S, K, ψ⟩ to win the game ⟨μ_{x}.K[x], H⟩. If k is as in the previous lemma, then the Opponents have a strategy in the game ⟨K_{σ}^{k}[⊥], H⟩. □

Proposition 7.5 In the μ-lattice J_{P} the following relations are true:

μ_{z}.ψ(z) = ⋁_{n≥0} ψ^{n}(⊥) ,
ν_{z}.ψ(z) = ⋀_{n≥0} ψ^{n}(⊤) ,

where ψ is a unary operator induced by a game-operator K[x] on J (P).

Proof. Let K[x] be such a game operator on J (P). It is clear that for all n ≥ 0 we have K^{n}[⊥] ≤ μ_{x}.K[x]. On the other hand, let H ∈ J (P) be such that for all n ≥ 0 K^{n}[⊥] ≤ H, i.e. Mediator has have a winning strategy in every game ⟨K^{n}[⊥], H⟩. If μ_{x}.K[x] ≰ H, by determinacy the Opponents have a winning strategy in the game ⟨μ_{x}.K[x], H⟩, hence a winning strategy in a game ⟨K^{n}[⊥], H⟩, because of proposition 7.1. Evidently it is not possible that both players have winning strategies in the same game, i.e. we get a contradiction. A proposition dual to proposition 7.1 is needed in order to show that the dual statement is also true. □

Definition 7.6 Let P be an ordered set with ⊥ and ⊤, and let ψ : P ^{}P be an operator. For every limit ordinal α define ψ^{α}(⊥) and ψ^{α}(⊤) by the formulas:

ψ^{α}(⊥) = ⋁_{β<α} ψ^{β}(⊥) ,
ψ^{α}(⊤) = ⋀_{β<α} ψ^{β}(⊤) .

Let L be a μ-lattice and say that it is founded if for every ϕ ∈ A such that a(ϕ) = n + 1, for every s = 1, …, n + 1 and every (l_{1}, …, l_{n}) ∈ L^{n}, ψ^{α}(⊥) and ψ^{α}(⊤) exist, where ψ(z) = ϕ(l_{1}, …, l_{s−1}, z, l_{s}, …, l_{n}).

Using the above notation, if L is founded μ-lattice, then the Knaster-Tarski relation:

μ_{z}.ψ(z) = ⋁_{α∈Ord} ψ^{α}(⊥)

is true as well as its dual. Proposition 7.5 shows that the μ-lattice J_{P} is founded. Also, every complete lattice is founded. In [San00, §B.5] a μ-lattice which is not founded is constructed as the inductive limit of founded μ-lattices. Say that a morphism of lattices is bicontinuous if it preserves arbitrary existing infima and suprema. Using lemma 3.5 it is easily seen that if f : L_{1} ^{}L_{2} is a bicontinuous morphism of lattices between two founded μ-lattices, then f is also a morphism of μ-lattices. We recall here the following proposition:

Proposition 7.7 [Mac37, MMT87, §2.2]. Given any lattice there exists a bicontinuous embedding into a complete lattice.

Theorem 7.8 There is an embedding of the free μ-lattice J_{P} into a complete lattice. Such embedding is a morphism of μ-lattices.

Theorem 7.9 Let l, m ∈ J_{P} be such that for every f : P ^{}L, where L is a complete lattice, it is true that f̃(l) ≤ f̃(m), where f̃ is defined by extending f to J_{P}. Then it is the case that l ≤ m. The class of complete lattices generates the quasivariety of μ-lattices.

Proof. Obvious, since we can embed free μ-lattices into complete lattices.

□

8 Conclusions

A complete interpretation, from the point of view of interactive computation and communication, of the algebraic results presented here has to be developed. It is our belief, however, that such interpretation will call for two kinds of generalization of the present work. The first will be to enrich the algebraic setting in order to include in the theory operators representing actions and coactions. The goal of this extension is to develop formal correspondences between our model of interactive computation, i.e. games for a free μ-lattice with operators, and existing models, for example the calculus of communicating systems [Mil80]. For the same reason, we are also led to consider μ-lattices enriched over quantales [Joy95c], hence to consider the theory of money games and to link the theory of interactive systems with the classical theory of games and economic behavior [vNM44]. The second generalization will be to introduce in the theory of games for free μ-lattices an algebra of winning strategies, the goal being that of providing an algebraic system for interactive programs with a built-in notion of program-equivalence. Under a proof-theoretic point of view, this step corresponds to focusing on the difference of proofs; from an algebraic point of view, it corresponds to lifting the results from μ-lattices to bicomplete categories where a bunch of definable functors have both initial algebras and final coalgebras. We would like develop other aspects of the present research. It is well known that the study of fix-points is of general interest to computer science and the results obtained here, as well as their possible generalizations, can be compared with previous work on the subject, for example to Lawvere-theories with fix-points [BÉ93] and to work on initial algebras of functors in categories [Lam68] and recursively defined types [RP93]. We believe that the description of the free μ-lattice will possibly help to prove that the alternation hierarchy for μ-lattice terms is strict, as it has been done for the propositional μ-calculus [Len96, Bra98]. Such problem is evidently related to the problem of characterizing fix-point free polynomials in free lattices [FJN95]. Eventually, strategies in the game ⟨G, H⟩ and what we called in the introduction circular proofs are mathematical objects related to tableaux for the propositional μ-calculus [Koz83, SW91, Bra92]; more precisely, they are related to refutations of [Wal95, NW96]. It is our belief that regular refutations can be lifted to a cut-free proof systems and that our techniques can be adapted in order to describe explicitely free boolean algebras with modal operators and fix-points. Acknowledgment. The research presented in this paper has been developed as part of a doctoral thesis in mathematics at the Université du Québec à Montréal. I would like to thank my supervisor Prof. André Joyal for his hints in developing this research and his help in obtaining these results.

References

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

[AJM94] S. Abramsky, R. Jagadeesan, and P. Malacaria. Full abstraction for PCF. In Theoretical Aspects of Computer Software, volume 789 of Lecture Notes in Computer Science, pages 1–15, 1994.

[Arn95] A. Arnold. An initial semantics for the μ-calculus on trees and Rabin’s complementation lemma. Theoret. Comput. Sci., 148(1):121–132, 1995.

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

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

[Bra92] J. C. Bradfield. Verifying temporal properties of systems. Birkhäuser Boston Inc., Boston, MA, 1992.

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

[Con76] J. H. Conway. On numbers and games. Academic Press [Harcourt Brace Jovanovich Publishers], London, 1976. London Mathematical Society Monographs, No. 6.

[Con78] J. H. Conway. Loopy games. Ann. Discrete Math., 3:55–74, 1978. Advances in graph theory (Cambridge Combinatorial Conf., Trinity College, Cambridge, 1977).

[EJ91] E. A. Emerson and C. S. Jutla. Tree automata, μ-calculus and determinacy. In Proc. FOCS 91, 1991.

[Fel86] W. Felscher. Dialogues as a foundation for intuitionistic logic. In D. Gabbay and F. Guenther, editors, Handbook of Philosophical Logic, Volume III, pages 341–372. D. Reidel Publishing Company, 1986.

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

[GH82] Y. Gurevich and L. Harrington. Trees, automata, and games. In Proc. 14th ACM Symp. on the Theory of Computation, pages 60–65, 1982.

[Gir87] J.-Y. Girard. Linear logic. Theoret. Comput. Sci., 50(1):101, 1987.

[Gir98] J.-Y. Girard. On the meaning of logical rules I/II. Manuscripts, 1998.

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

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

[HO94] J. M. E. Hyland and C.-H. L. Ong. On full abstraction for PCF: I, II and III. To appear in Information and Computation, 1994.

[Joy77] A. Joyal. Remarques sur la théorie des jeux á deux personnes. La Gazette des Sciences Mathématiques du Québec, 1(4), March 1977.

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

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

[Joy95c] A. Joyal. Free lattices, communication, and money games. In: Proceedings of the 10-th International Congress of Logic, Methodology, and Philosophy of Science, Firenze, 1995.

[Koz83] D. Kozen. Results on the propositional μ-calculus. Theoret. Comput. Sci., 27(3):333–354, 1983.

[Lam68] J. Lambek. A fixpoint theorem for complete categories. Math. Z., 103:151–161, 1968.

[Len96] 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.

[LS86] J. Lambek and P. J. Scott. Introduction to higher order categorical logic. Cambridge University Press, Cambridge, 1986.

[Mac37] H. MacNeille. Partially ordered sets. Trans. AMS, 42:416–460, 1937.

[McN93] R. McNaughton. Infinite games played on finite graphs. Ann. Pure Appl. Logic, 65(2):149–184, 1993.

[Mil80] R. Milner. A calculus of communicating systems. Springer-Verlag, Berlin, 1980.

[MMT87] R. McKenzie, G. F. McNulty, and W. F. Taylor. Algebras, lattices, varieties. Wadsworth & Brooks/Cole Advanced Books & Software, Monterey, Calif., 1987.

[Niw85] D. Niwiński. Equational μ-calculus. In Computation theory (Zaborów, 1984), volume 208 of Lecture Notes in Computer Science, pages 169–176. Springer, Berlin, 1985.

[Niw97] D. Niwiński. Fixed point characterization of infinite behavior of finite-state systems. Theoret. Comput. Sci., 189(1-2):1–69, 1997.

[NW96] D. Niwiński and I. Walukiewicz. Games for the μ-calculus. Theoret. Comput. Sci., 163(1-2):99–116, 1996.

[NYY92] A. Nerode, A. Yakhnis, and V. Yakhnis. Concurrent programs as strategies in games. In Logic from computer science (Berkeley, CA, 1989), pages 405–479. Springer, New York, 1992.

[Pra81] V. Pratt. A decidable μ-calculus. In 22nd Annual IEEE Symposum on Foundations of Computer Science (Nashville, TN, 1981), pages 421–427, 1981.

[Rab69] M. O. Rabin. Decidability of second order theories and automata on infinite trees. Trans. Am. Math. Society, 141:1–35, 1969.

[RP93] J. C. Reynolds and G. D. Plotkin. On functors expressible in the polymorphic typed lambda calculus. Inform. and Comput., 105(1):1–29, 1993.

[San00] L. Santocanale. Sur les μ-treillis libres. PhD thesis, Université du Québec à Montréal, July 2000.

[SW91] C. Stirling and D. Walker. Local model checking in the modal mu-calculus. Theoret. Comput. Sci., 89(1):161–177, 1991.

[Tar55] A. Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific J. Math., 5:285–309, 1955.

[Tho97] 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.

[vNM44] J. von Neumann and O. Morgenstern. Theory of Games and Economic Behavior. Princeton University Press, Princeton, New Jersey, 1944.

[Wal95] I. Walukiewicz. Completeness of Kozen’s axiomatizations of the propositional μ-calculus. In Proc. of the 10th IEEE Symp. on Logic in Computer Science, 1995.

[Wal96] I. Walukiewicz. Pushdown processes: Games and model checking. Technical Report RS-96-54, BRICS, December 1996.

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

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

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

Recent BRICS Report Series Publications

RS-00-28 Luigi Santocanale. Free μ-lattices. November 2000. 51 pp. Short abstract appeared in Proceedings of Category Theory 99, Coimbra, Portugal, July 19-24, 1999. Full version to appear in a special conference issue of the Journal of Pure and Applied Algebra.

RS-00-27 ZoltánÉsik and Werner Kuich. Inductive^{∗}-Semirings. October 2000. 34 pp.

RS-00-26 František Čapkovič. Modelling and Control of Discrete Event Dynamic Systems. October 2000. 58 pp.

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

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

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

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

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

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

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

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