Simon Castellan

Pierre Clairambault

Glynn Winskel

Symmetry in Concurrent Games

Behavioural symmetry is introduced into concurrent games. It expresses when plays are essentially the same. A characterization of strategies on games with symmetry is provided. This leads to a bicategory of strategies on games with symmetry. Symmetry helps allay the perhaps overly-concrete nature of games and strategies, and shares many mathematical features with homotopy. In the presence of symmetry we can consider monads for which the monad laws do not hold on the nose but do hold up to symmetry. This broadening of the concept of monad has a dramatic effect on the types concurrent games can support and allows us, for example, to recover the replication needed to express and extend traditional game semantics.

I. INTRODUCTION

In game semantics of programming languages a type of a program is represented by a game, and the program itself by a strategy in the game. The approach is very flexible: game semantics has managed to capture accurately a wide variety of features of higher-order programming languages, including state, control, exceptions, and many others. Game semantics follows the methodology of denotational semantics, and interprets complex programs compositionally in terms of interpretations of their components. Game semantics is also operational: moves in a game correspond to computation steps. As such it is increasingly exploited to provide a syntax-free operational semantics for programming languages, a much needed tool for the analysis and verification of programs.

Concurrency is a central concern in computer science. Reflecting the traditions of concurrency theory, game semantics for concurrent programs come in two styles: based on interleavings and on partial-orders. Of these, the historical focus has been on interleaving, giving models of various programming languages [START_REF] Ghica | Angelic semantics of fine-grained concurrency[END_REF], [START_REF] Laird | A game semantics of the asynchronous pi-calculus[END_REF], even a model-checking tool [START_REF] Ghica | Compositional model extraction for higher-order concurrent programs[END_REF]. Partial-order methods have the strength of supporting reasoning about dependency directly, but are at a more preliminary stage. Abramsky and Melliès proposed in [START_REF] Abramsky | Concurrent games and full completeness[END_REF] a framework for concurrent games based on closure operators, re-understood later by Melliès and Mimram in terms of asynchronous transition systems [START_REF] Melliès | Asynchronous games 2: The true concurrency of innocence[END_REF], [START_REF] Melliès | Asynchronous games: Innocence without alternation[END_REF]; Faggian and Piccolo have also presented strategies as partial orders [START_REF] Faggian | Partial orders, event structures and linear strategies[END_REF]. In [START_REF] Rideau | Concurrent strategies[END_REF], Rideau and Winskel gave a new foundation based on event structures, generalizing all previous approaches and allowing nondeterminism. It is this framework we refer to as concurrent games.

When developing a game semantics, one has to deal with the low-level aspect of games-some identities that hold operationally do not hold automatically in games. An important example of such phenomena occurs in the replication of resources in programming languages: whereas two accesses to the same resource might be indistinguishable operationally, they can correspond to different and unrelated events in the game. In this sense, games are overly-concrete. In the history of game semantics [START_REF] Abramsky | Full abstraction for PCF[END_REF], this has been alleviated by introducing symmetry into games. Informally, symmetry in a game concerns when one play of a game is essentially the same as another. Our treatment of symmetry in concurrent games, where plays can be highly-distributed, stems from earlier work on symmetry in event structures [START_REF] Winskel | Event structures with symmetry[END_REF] and makes use of a general method of open maps for defining bisimulation in a variety of models [START_REF] Joyal | Bisimulation from open maps[END_REF]. Briefly, a symmetry in a game is expressed as a bisimulation equivalence (given as a span of open maps) that says when two plays are similar according to the symmetry. This feature considerably enhances the mathematical theory of concurrent games. Symmetry comes to share many features with homotopy-symmetric plays are like homotopic paths-which plays a role in its mathematical development.

a) Contributions.: Firstly, we introduce concurrent games with symmetry. This involves a new definition of the copycat strategy and of composition, which now have to respect symmetry. As in [START_REF] Rideau | Concurrent strategies[END_REF], we characterize strategies, for which copycat behaves like an identity w.r.t. composition. This leads to the construction of a bicategory (up to symmetry) of concurrent games with symmetry and symmetry-respecting strategies. Secondly, we give two illustrations of how this framework can be used to model logics and programming languages. The first is a presentation within concurrent games of the construction of [START_REF] Baillot | Believe it or not, AJM's games model is a model of classical linear logic[END_REF], using an adaptation of AJM games [START_REF] Abramsky | Full abstraction for PCF[END_REF] to model classical linear logic (CLL). The second is a concurrent games presentation of HO games [START_REF] Hyland | On full abstraction for PCF: I, II, and III[END_REF], giving a concurrent and non-deterministic notion of innocent strategies (in the sense of Hyland and Ong), and a new proof that standard innocent strategies are stable under composition.

b) Related work.: In sequential games, the notion of symmetry that is closest to ours is that of AJM games [START_REF] Abramsky | Full abstraction for PCF[END_REF], and in particular its variant in [START_REF] Baillot | Believe it or not, AJM's games model is a model of classical linear logic[END_REF]. In asynchronous games, Melliès expressed symmetry by giving groups acting on the game [START_REF] Melliès | Asynchronous games 1: A group-theoretic formulation of uniformity[END_REF], reindexing the events. Restricting to a polarized deterministic setting, it should be possible to reformulate Melliès' approach in terms of concurrent games with symmetry-left however for future work. c) Outline.: In Section II, we present event structures, and their extension with symmetry and polarity. In Section III, we give the main contribution of this paper, the bicategory of concurrent games with symmetry and concurrent strategies. In Section IV we give two important applications: concurrent generalizations of AJM games and HO games, showing how concurrent games with symmetry extend the games of traditional game semantics.

II. PRELIMINARIES

A. Event structures

An event structure comprises (E, ≤, Con), consisting of a set E, of events which are partially ordered by ≤, the causal dependency relation, and a nonempty consistency relation Con consisting of finite subsets of E, which satisfy {e ′ e ′ ≤ e} is finite for all e ∈ E, {e} ∈ Con for all e ∈ E, Y ⊆ X ∈ Con ⇒ Y ∈ Con, and

X ∈ Con & e ≤ e ′ ∈ X ⇒ X ∪ {e} ∈ Con.
The (finite) configurations, C(E), of an event structure E consist of those finite subsets x ⊆ E which are Consistent: x ∈ Con, and Down-closed: ∀e, e ′ . e ′ ≤ e ∈ x ⇒ e ′ ∈ x. We say an event structure is elementary when the consistency relation consists of all finite subsets of events. For X ⊆ E we write [X] E for {e ∈ E ∃e ′ ∈ X. e ≤ e ′ }, the down-closure of X; note if X ∈ Con, then [X] E ∈ Con is a configuration. In games the relation of immediate dependency e e ′ , meaning e and e ′ are distinct with e ≤ e ′ and no event in between, will play a very important role. For configurations x, y, we use x-⊂y to mean y covers x, i.e. x ⊂ y with nothing in between, and x e -⊂y to mean x ∪ {e} = y for an event e ∉ x. We sometimes use x e -⊂, expressing that event e is enabled at configuration x, when x e -⊂y for some y. A (partial) map of event structures f ∶ E → E ′ is a partial function f ∶ E ⇀ E ′ from the events of E to the events of E ′ such that for all configurations x ∈ C(E),

f x ∈ C(E ′ ) & (∀e 1 , e 2 ∈ x. f (e 1 ) = f (e 2 ) ⇒ e 1 = e 2 ) .
Maps compose as functions. We say a map is total when it is total as a function; then f restricts to a bijection x ≅ f x on x ∈ C(E). Say a total map of event structures is rigid when it preserves causal dependency. We write E (resp. E p ) for the category of event structures with total (resp. partial). These two categories have coproducts, binary products and pullbacks.

Proposition 1. Finite configurations of a product

A × B in E correspond to secured bijections θ ∶ x ≅ y between configurations x ∈ C(A) and y ∈ C(B), such that the order generated on θ by taking (a, b) ≤ (a ′ , b ′ ) if a ≤ A a or b ≤ B b ′
is a partial order. The correspondence respects inclusion.

Individual configurations inherit an order from the ambient event structure and can themselves be regarded as finite elementary event structures. Viewed this way, an inclusion x ⊆ y between configurations induces a rigid map x ↪ y between the configurations regarded as event structures. The configurations of an event structure form a non-empty family of finite partial orders closed under rigid inclusions. Conversely, given such a rigid family, we can build an event structure: Proposition 2. Let Q be a rigid family, a non-empty family of finite partial orders closed under rigid inclusions, i.e. if q ∈ Q and q ′ ↪ q is a rigid inclusion (regarded as a map of event structures) then q ′ ∈ Q. The family Q determines an event structure Pr(Q) = def (P, ≤, Con):

• the events P are the finite partial orders in Q with a top element (the primes), • the causal dependency relation p ′ ≤ p holds when there is a rigid inclusion from p ′ ↪ p; • for any finite X ⊆ P , X ∈ Con iff there is q ∈ Q and rigid inclusions p ↪ q for all p ∈ X. If x ∈ C(P ) then ⋃ x, the union of the partial orders in x, is in Q. The function x ↦ ⋃ x is an order-isomorphism from C(P ), ordered by inclusion, to Q, ordered by rigid inclusions.

B. Symmetry

We endow event structures with symmetry. A relation of symmetry on an event structure expresses when two configurations are essentially the same and is expressed as a form of bisimulation equivalence, based on open maps [START_REF] Joyal | Bisimulation from open maps[END_REF].

1) Open maps: Open maps are a generalisation of functional bisimulations, known from transition systems. Let C be a category with a distinguished subcategory P of path objects with path-extension maps. A map

f ∶ A → B in C is open if it satisfies a path-lifting property: p / / m A f q / / ; ; B.
Any commuting square, with m ∶ p → q in P, factors into two commuting triangles as shown. Bisimulation is then expressed as a span of open maps.

2) Event structures with symmetry: The way we equip event structures with symmetry is an instance of the following general construction. Let X be an object of a category C. Recall that a relation on X is an object X and pair of maps l X , r X ∶ X → X-so forming a span-which are jointlymonic. A map between objects with relations f

∶ (X, X) → (Y, Ỹ ) is a map f ∶ X → Y in C for which there is a necessarily unique map f ∶ X → Ỹ in C such that f l X = l Y f
and f r X = r Y f . If C has products, then a relation on X can equivalently be given by a mono X ↣ X × X. If C has pullbacks we can formulate diagrammatically the requirement that X be an equivalence relation-see [START_REF] Winskel | Event structures with symmetry[END_REF].

If C is equipped with a class of open maps, we say that a relation l X , r X ∶ X → X is a symmetry in X if it is an equivalence relation with both l X and r X open; this amounts to X being a bisimulation equivalence. A map f ∶ (X, X) → (Y, Ỹ ) necessarily preserves symmetry. We obtain a category CS of objects with symmetry and symmetrypreserving maps. Given two maps f, g ∶ (X, X) → (Y, Ỹ ) they are equal up to symmetry, written f ∼ g, if there is a necessarily unique map h ∶ X → Ỹ in C such that f = l Y h and g = r Y h. The category CS is more fully described as enriched in the category of equivalence relations and so, because equivalence relations are a degenerate form of category, as a 2-category in which the 2-cells are instances of the equivalence. This view informs the constructions in such categories which are often very simple examples of the (pseudo-and bi-) constructions of 2-categories. In particular, objects A and B are equivalent, written A ≃ B, if there are maps f ∶ A → B and g ∶ B → A such that f g ∼ id B and gf ∼ id A .

We can take advantage of the concrete nature of event structures to give an explicit description of symmetries there, a characterization which is independent of whether the category of event structures carries rigid, total or partial maps, though for definiteness assume the category is E. A symmetry in an event structure E determines a mono Ẽ ↣ E × E, thus a subset of C(E × E), and so by Proposition 1 a family of bijections between finite configurations of E. In this way, a symmetry in an event structure E corresponds to an isomorphism family comprising a non-empty family of bijections θ ∶ x ≅ E y between pairs of finite configurations of E such that:

(i) for all identities id x ∶ x ≅ E x, where x ∈ C(E); if θ ∶ x ≅ E y, then the inverse θ -1 ∶ y ≅ E x; and if θ ∶ x ≅ E y and ϕ ∶ y ≅ E z, then their composition ϕ ○ θ ∶ x ≅ E z. (ii) for θ ∶ x ≅ E y whenever x ′ ⊆ x with x ′ ∈ C(E), then there is a (necessarily unique) y ′ ∈ C(E) with y ′ ⊆ y such that the restriction θ ′ ∶ x ′ ≅ E y ′ . (iii) for θ ∶ x ≅ E y whenever x ⊆ x ′ for x ′ ∈ C(E), there is an extension of θ to θ ′ so θ ′ ∶ x ′ ≅ E y ′ for some (not necessarily unique) y ′ ∈ C(E) with y ⊆ y ′ .
The isomorphism family makes precise the sense in which a symmetry expresses when two configurations are essentially the same. Note that (ii) implies that the bijections in the isomorphism family respect the partial order of causal dependency on configurations inherited from E; the bijections in an isomorphism family are isomorphisms between the configurations regarded as elementary event structures.

An event structure with symmetry A corresponds to an isomorphism family ≅ A of the underlying event structure of A [START_REF] Winskel | Event structures with symmetry[END_REF]. There are straightforward reformulations of what it means for a map to preserve symmetry or for two maps to be equal up to symmetry in terms of isomorphism families. A total map f ∶ A → B preserving symmetry amounts to

x θ ≅ A y implying f x f θ ≅ B f y, where f θ is the composite bijection f x ≅ x θ ≅ A y ≅ f y; while f ∼ g, for two total maps f, g ∶ A → B preserving symmetry, iff f x ϕx ≅ B gx for all x ∈ C(A), where ϕ x is the composite bijection f x ≅ x ≅ gx.
We define the category ES (resp. ES p ) to consist of event structures with symmetry, with total (resp. partial) maps.

Proposition 3. Any map f ∶ A → B in ES p has a partial-total factorization as a composite

A p V / / (A↓V ) f1 / / B
where:

V = def {a ∈ A f (a) is defined} is the domain of def- inition of f ; A ↓ V = def (V, ≤ V , Con V ) with v ≤ V v ′ iff v ≤ A v ′ & v, v ′ ∈ V and X ∈ Con V iff X ∈ Con A & X ⊆ V ; its isomorphism family is given by θ ∶ x ≅ A↓V y iff θ extends to θ ′ ∶ [x] A ≅ A [y] A ; the map p V ∶ A → A ↓ V
is the partial map acting as identity on V and undefined elsewhere; and f 1 is a total map acting as

f on V . If f ∼ g ∶ A → B in ES p ,
then the domains of definition of f and g are the same, V say, and

f 1 ∼ g 1 in their partial-total factorizations f = f 1 p V and g = g 1 p V .
Through the addition of symmetry event structures can represent a much richer class of categories than mere partial orders. The finite configurations of an event structure with symmetry can be extended by inclusion or rearranged bijectively under an isomorphism allowed by the symmetry. In this way an event structure with symmetry determines, in general, a category of finite configurations with maps those injections obtained by repeatedly composing the inclusions and allowed isomorphisms. By property (ii) in the definition of isomorphism family any such map factors uniquely as an isomorphism of the symmetry followed by an inclusion.

3) Constructions: We review from [START_REF] Winskel | Event structures with symmetry[END_REF] important constructions in ES.

a) Products: First, ES has binary products.

Theorem 4. Let A and B be objects in ES. Their product in ES is given by (A×B; l A ×l B , r A ×r B ∶ Ã× B → A×B), based on the product A × B in E, and sharing the same projections,

π 1 ∶ A × B → A and π 2 ∶ A × B → B. Let f, f ′ ∶ C → A and g, g ′ ∶ C → A in ES. If f ∼ f ′ and g ∼ g ′ , then ⟨f, g⟩ ∼ ⟨f ′ , g ′ ⟩.
b) Simple parallel composition: The operation of simple parallel composition of event structures A∥B which juxtaposes the two event structures A and B-with a finite set of events consistent if its overlaps with A and B are consistent-and acts similarly on maps, extends to a functor on ES. The symmetry on A∥B is Ã∥ B with left and right maps l A ∥l B and r A ∥r B . c) Pseudo pullbacks: It will have great bearing on this paper that, while ES does not have equalizers or pullbacks in general, it does have pseudo equalizers and pseudo pullbacks. We give their definition and refer the reader to [START_REF] Winskel | Event structures with symmetry[END_REF] for proofs.

Maps

f, g ∶ B → C have a pseudo equalizer i ∶ E → B, i.e. f i ∼ gi and for any map i ′ ∶ E ′ → A such that f i ′ ∼ gi ′ , there is a unique map h ∶ E ′ → E such that i ′ = ih.
The object E can be described as having configurations those x ∈ C(B) for which f x ϕx ≅ C gx, where ϕ x is the bijection induced by x; its isomorphism family is the restriction of that on B.

Maps f ∶ A → C, g ∶ B → C have a pseudo pullback given as the pseudo equalizer of f π 1 , gπ 2 ∶ A × B → C. We summarize its properties: The pseudo pullback comprises an object D and maps π 1 ∶ D → A and π 2 ∶ D → B such that f π 1 ∼ gπ 2 which satisfies the further property that for any object D ′ and maps

p 1 ∶ D ′ → A and p 2 ∶ D ′ → B such that f p 1 ∼ gp 2 , there is a unique map h ∶ D ′ → D such that p 1 = π 1 h and p 2 = π 2 h.

4) Homotopy:

We remark that the category ES has the structure of a homotopy category. In particular it has path objects. From the pseudo pullback

à l A r A A id A ∼ A id A A
we recover Ã, the symmetry on A, but as an object in ES itself equipped with symmetry Ã. This universal property is that associated with a path object generally written A I , where I stands for (a generalization of) the unit interval: asserting θ ∶ x ≅ A y, that a bijection between two configurations is in the isomorphism family of A, is analogous to specifying a path from x to y. (There are also cylinder objects in ES.)

Later, in defining the copycat strategy we shall make essential use of the fact that in (A, Ã), an event structure with symmetry, the symmetry à itself possesses a symmetry Ã. Concretely, a configuration of à corresponds to an element of the isomorphism family θ ∶ x≅ A y and a configuration of à to a pair ϕ 1 , ϕ 2 in a commuting square mediating between θ 1 and θ 2 in the isomorphism family of A:

x 1 ≅ ϕ1 A ≅ A θ1 y 1 ≅ ϕ2 A x 2 ≅ A θ2 y 2 Lemma 5. Let f ∶ A → B

C. Adding polarity

Games and strategies will be represented in terms of event structures where events are moves of Player or Opponent, signified by events carrying a polarity, + for Player andfor Opponent. Formally, an event structure with polarity comprises an event structure A with a function pol A ∶ A → {+, -} assigning a polarity to each event. Maps are assumed to preserve polarity.

The addition of polarity to an event structure A means that the ⊆-order on its finite configurations is now obtained as compositions (⊆ -∪ ⊆ + ) + of two more fundamental orders, where for x, y ∈ C ∞ (A),

x ⊆ -y iff x ⊆ y & pol A (y ∖ x) ⊆ {-} , and x ⊆ + y iff x ⊆ y & pol A (y ∖ x) ⊆ {+} .
More surprisingly there is a new partial order, the Scott order, between configurations which is intimately related to copycat strategies. The Scott order ⊑ A is defined to be (⊇ -∪ ⊆ + ) + .

(We use ⊇ -for the converse order to ⊆ -.) The Scott order possesses a unique factorization: for x, y ∈ C ∞ (A),

y ⊑ A x ⇐⇒ ∃!z ∈ C ∞ (A). y ⊇ -z ⊆ + x
-it is an easy exercise to show that z is necessarily x ∩ y. Not only do the configurations of copycat strategies of A correspond to pairs of configurations in the Scott order, but also strategies in A correspond to certain, simply-described, discrete fibrations over (C(A), ⊑ A )-see [START_REF] Winskel | Strategies as profunctors[END_REF] for the full story. Given this we can expect a variation on the Scott order to play a role in strategies in games with symmetry.

An event structure with polarity and symmetry (henceforth an e.p.s.) consists of (E, Ẽ), an event structure with polarity also endowed with a symmetry Ẽ. The categories EPS and EPS p of such objects have maps preserving both symmetry and polarity, which are respectively total and partial.

The addition of polarity and symmetry brings a new richness to the configurations of an event structure. The Scott order becomes a Scott category, Scott(A), of an e.p.s. A, where now maps between configurations are obtained as compositions of (partial injections) ⊇ -, ⊆ + and the isomorphism family ≅ A . Maps from y to x in Scott(A) have a unique factorization

y ⊇ -y 0 θ ≅ A x 0 ⊆ + x .
The unique factorization follows from property (ii) of isomorphism families and uniqueness of the factorization of the Scott order. A map f ∶ A → B in EPS p preserves ⊇ -, ⊆ + and isomorphism families so extends directly to a functor f ∶ Scott(A) → Scott(B) making Scott a functor to Cat.

III. GAMES WITH SYMMETRY

A concurrent game with symmetry is represented by an e.p.s.

A. A pre-strategy in A is a total map σ ∶ S → A in EPS. A map between pre-strategies, from σ ∶ S → A to σ ′ ∶ S ′ → A, is a map f ∶ S → S ′ in EPS such that S σ % % f / / S ′ σ ′ A commutes.
We say the two pre-strategies σ and σ ′ are equivalent, and write σ ≃ σ ′ , and sometimes f ∶ σ ≃ σ ′ , when there are maps f from σ to σ ′ , and g from σ ′ to σ determining an equivalence S ≃ S ′ , i.e. such that gf ∼ id S and f g ∼ id S ′ ; isomorphism σ ≅ σ ′ occurs when gf = id S and f g = id S ′ . A weak map from σ to σ ′ is a map f ∶ S → S ′ such that the triangle above commutes up to ∼ and analogously say σ and σ ′ are weakly equivalent when there are weak maps f and g making S ≃ S ′ .

Simple parallel composition extends directly to a functor A∥B on A and B in EPS. The dual of an e.p.s. A, written A ⊥ , has the same underlying event structure with symmetry but with a reversal of polarities.

Following Joyal [START_REF]Remarques sur la théorie des jeux à deux personnes[END_REF], a pre-strategy from A to B is a pre-strategy in the game A ⊥ ∥B. In refining the notion of pre-strategy to that of strategy we shall follow the guiding principle of [START_REF] Rideau | Concurrent strategies[END_REF]: a strategy is a pre-strategy for which copycat is an identity w.r.t. composition. The next few sections make this precise and culminate in the definition of strategy between concurrent games with symmetry.

A. Copycat

Let A be an e.p.s.. Configurations of CC A will correspond to maps in Scott(A). Recall a map from y to x in Scott(A) can be put into a unique form

y ⊇ -y 0 θ ≅ A x 0 ⊆ + x .
Define q(x, θ, y) to be the partial order with underlying set x∥y = def ({1}×x)∪({2}×y), causal dependency that inherited from A ⊥ ∥A with additional causal dependencies

{(a 1 , a 2 ) ∈ x 0 × y 0 pol A (a 2 ) = + & θ(a 1 ) = a 2 }∪ {(a 2 , a 1 ) ∈ y 0 × x 0 pol A ⊥ (a 1 ) = + & θ(a 1 ) = a 2 } .
That q(x, θ, y) is indeed a partial order follows as in [START_REF] Rideau | Concurrent strategies[END_REF]. The set of all such partial orders forms a rigid family Q. We define the event structure of CC A to be Pr(Q). Because Scott is a functor, the operation CC A is functorial in A. We define the symmetry on CC A as

CC A C C l A ← CC Ã C Cr A → CC A
Note, that in the construction of CC à we are using the fact that à possesses a symmetry Ã-see Section II-B4. The map γ A ∶ CC A → A ⊥ ∥A takes a prime order to its top event.

Lemma 6. The construction

(CC A , CC l A , CC r A ∶ CC Ã → CC A )
is an e.p.s. and γ A a pre-strategy.

In future we shall overload CC A and write CC A for the e.p.s. of Lemma 6. From the definitions, CC A = CC Ã .

B. Composition

Let σ ∶ S → A ⊥ ∥B and τ ∶ T → B ⊥ ∥C be pre-strategies between games A, B, C. To define their composition first form the pseudo pullback

P π1 x x π2 & & S∥C σ∥C & & ∼ A∥T A∥τ x
x A∥B∥C of the maps on the underlying event structures with symmetry, ignoring polarities, viz. σ ∶ S → A∥B and τ ∶ T → B∥C. There is an obvious partial map of event structures A∥B∥C → A∥C undefined on B and acting as identity on A and C. The partial maps from P to A∥C, given by following the diagram either way round the pseudo pullback,

A ∥ T A∥τ ' ' P π2 < < π1 " " ∼ A ∥ B ∥ C / / A ∥ C S ∥ C σ∥C 7 7
are defined on a common subset V ⊆ P -Proposition 3. Forming the partial-total factorization of either map (for preciseness take the left/lowest) we obtain

P → P ↓V → A∥C .
The resulting total map gives us the composition τ ⊙σ ∶ T ⊙S = def P ↓V → A ⊥ ∥C once we reinstate polarities to make τ ⊙σ a map in EPS. The projection operation P ↓ V hides all events not visible in A and C.

From Lemma 5, regarding e.g. T as itself an e.p.s., it follows that T ⊙S ≅ T ⊙ S and τ ⊙σ ≅ τ ⊙σ.

C. Strategies

We are interested in necessary and sufficient conditions on a pre-strategy σ ∶ S → A to ensure σ ≃ γ A ⊙σ. As we shall see σ should be equivalent to a pre-strategy which is strongreceptive, innocent and saturated. (If a pre-strategy σ ∶ S → A ⊥ ∥B satisfies these conditions, then σ ≃ γ B ⊙σ⊙γ A .)

1) Necessity: We show that for any pre-strategy σ ∶ S → A the pre-strategy γ A ⊙σ is necessarily strong-receptive, innocent and saturated.

A pre-strategy σ is receptive iff for all x ∈ C(S), σx

a -⊂ & pol A (a) = -implies ∃!s ∈ S. x s -⊂ & σ(s) = a .
The pre-strategy σ ∶ S → A, as a map in EPS preserves symmetry, so is associated with a map σ ∶ S → Ã. Say σ is strongreceptive if σ, and so also σ, is receptive. A pre-strategy σ is innocent when s s ′ and (pol (s) = + or pol (s ′ ) = -) implies σ(s) σ(s ′ ).

To specify when a pre-strategy σ ∶ S → A is saturated we need some background. Form the pseudo pullback

S × A A π1 z z π2 $ $ S σ $ $ ∼ A id A y y A .
The operation taking σ to its saturation π 2 is part of a monad on pre-strategies in A. Clearly

S id S σ S σ A id A A commutes.
Hence there is a unique map η ∶ S → S × A A such that π 1 η = id S and π 2 η = σ-thus η is a map from σ to π 2 . We say σ is saturated when η is part of an equivalence σ ≃ π 2 , i.e. there is a map act ∶ S × A A → S such that

S × A A π2 # # act / / S σ A
commutes and act η ∼ id S with η act ∼ id S× A A . Concretely, a finite configuration of S × A A can be identified with a pair (x, θ) where x ∈ C(S) and θ ∶ σx ≅ A y. The action of act is to transport the configuration x across θ it to a configuration x ′ = def act(x, θ) with ϕ ∶ x ≅ S x ′ and σϕ = θ.

Certain compositions are automatically saturated: Proof. The construction of CC A directly ensures the innocence and receptivity of γ A . The way symmetry of copycat is obtained from CC Ã makes γ A equal γ Ã so receptive, guaranteeing strong-receptivity of γ A . To see γ A is saturated we require a map act ∶ CC A × A∥A A∥A → CC A . A configuration of CC A × A∥A A∥A corresponds to a configuration of CC A , so a map in Scott(A)

x ⊇ + x 0 θ ≅ A y 0 ⊆ -y ,
and a configuration of A∥A, so a pair v, w, for which ϕ 1 ∶ x ≅ A v and ϕ 2 ∶ y ≅ A w . This data and the factorization properties in Scott(A) yield:

x ≅ ϕ1 A ⊇ + x 0 ≅ A ≅ A θ y 0 ≅ A ⊆ - y ≅ ϕ2 A v ⊇ + v 0 ≅ A θ ′ w 0 ⊆ - w
We take the configuration of CC A got via act to be that corresponding to

v ⊇ + v 0 ≅ A θ ′ w 0 ⊆ -w .
The map act together with η ∶ CC A → CC A × A∥A A∥A establishes the equivalence needed for γ A to be saturated.

Lemma 9 (Necessity). γ A ⊙σ is strong-receptive, innocent and saturated for any pre-strategy σ in A.

Proof. The composition γ A ⊙σ inherits innocence and receptivity directly from that of γ A . Now γ A ⊙σ ≅ γ A ⊙σ ≅ γ Ã⊙σ whence γ A ⊙σ inherits receptivity from that of γ Ã, making γ A ⊙σ strong-receptive. The composition is saturated for general reasons-Proposition 7.

2) Sufficiency: We show the conditions strong-receptive, innocent and saturated are sufficient to ensure that a prestrategy σ is equivalent to its composition with copycat γ A ⊙σ. Lemma 10. Let σ ∶ S → A be a pre-strategy. There is a map I ∶ S → CC A ⊙S in EPS, unique up to symmetry, such that σ = (γ A ⊙σ)I.

Proof. We sketch the existence part of the proof by describing how I acts on configurations. Given x ∈ C(S), there is a secured bijection x∥σx ≅ q(σx, id σx , σx)-the bijection is that given by x ≅ σx between left components and id σx between the right. The secured bijection corresponds to a configuration z of the pseudo pullback (S∥A) × A∥A CC A . The result of the projection operation is to hide all those events not above the right component in A∥A, so from z yields a configuration of CC A ⊙S with image σx under γ A ⊙σ.

Lemma 11. If a pre-strategy σ is strong-receptive, innocent and saturated, then I ∶ σ ≃ γ A ⊙σ is an equivalence.

Proof. We require a map K ∶ CC A ⊙S → S that with I establishes an equivalence

γ A ⊙σ ≃ σ. Let u ∈ C(CC A ⊙S). Its down-closure [u] is a configuration in the pseudo pullback (S∥A) × A∥A CC A : (S∥A) × A∥A CC A π1 v v π2 ( ( S∥A σ∥A ( ( ∼ CC A γ A v v A∥A
As a configuration of the pseudo pullback, [u] corresponds to a triple, a configuration in S∥A and a configuration in CC A , mediated by an element of the isomorphism family of A∥Asee Section II-B3c. A configuration of S∥A corresponds to a pair of configurations x of S and w of A; a configuration of CC A to configurations of A in the relations z 1 ⊇ + z ′ 1 ≅ A z ′ 2 ⊆ - z 2 ; and the mediating element of the isomorphism family to a pair σx ≅ A z 1 and w ≅ A z 2 . From this data we obtain the composite map

σx ≅ A z 1 ⊇ + z ′ 1 ≅ A z ′ 2 ⊆ -z 2 ≅ A w in Scott(A). This factors uniquely into σx ⊇ + y 1 θ ≅ A y 2 ⊆ -w .
From innocence it follows (see Lemma 1 of [START_REF] Winskel | Strategies as profunctors[END_REF]) that there is a unique x 1 ∈ C(S) for which x ⊇ + x 1 and σx 1 = y 1 . Now, the pair x 1 and θ ∶ y 1 ≅ A y 2 can be identified with a configuration of S × A A. Hence we can apply act to obtain act(x 1 , θ) ∈ C(S) with σact(x 1 , θ) = y 2 .

Define p(u) = def act(x 1 , θ). By considering how it acts on isomorphism families, p extends to a monotonic function

p ∶ C( CC A ⊙S) → C( S) such that ∀u ∈ C(CC A ⊙S). σ p(u) ⊆ -γ A ⊙σ u .
Using Lemma 23 of [START_REF] Rideau | Concurrent strategies[END_REF] and the strong-receptivity of σ, we obtain a unique total map K ∶ CC S ⊙S → S such that ∀u ∈ C(CC A ⊙S). p(u) ⊆ -Ku and γ A ⊙σ = σK. On checking KI ∼ id S and IK ∼ id C C A ⊙S we have the desired equivalence.

Define a strategy to be a pre-strategy which is strongreceptive, innocent and saturated.

A strategy σ ∶ S → A induces a fibration σ ∶ Scott(S) → Scott(A). In fact, ⊇ -and ⊆ + maps in Scott(A) have cartesian liftings again as ⊇ -and ⊆ + maps, respectively, in Scott(S) because σ is receptive and innocent [START_REF] Winskel | Strategies as profunctors[END_REF]-with strong-receptivity ensuring the appropriate uniqueness-while ≅ A maps have cartesian liftings in ≅ S because σ is saturated.

Lemma 12. If σ and τ are strategies, so is τ ⊙σ.

Proof. The composition inherits innocence and receptivity from σ and τ . Because τ ⊙σ ≅ τ ⊙σ it also inherits strong receptivity. Its saturation obtains via Proposition 7 and the saturation of τ .

3) A ∼-bicategory of games with symmetry: Combining the above results, we do not quite obtain a bicategory but rather Strat, a "bicategory up to symmetry" in the following sense:

• its objects are e.p.s.'s-the games;

• its arrows from A to B are strategies σ ∶ A + / / B related by maps of pre-strategies-Strat(A, B) is thus a category enriched with equivalence relations ∼;

• horizontal composition is given by composition of strategies ⊙, which extends to functors Strat(B, C) × Strat(A, B) → Strat(A, C) via the universality of pseudo pullback;

• there is a natural isomorphism (derived from the universality of pseudo pullback) to express the associativity of composition, but only natural equivalences (derived from the equivalence of Lemma 11) for left and right identity laws;

• of the usual coherence axioms for bicategories, that for identity only commutes up to ∼.

Because categories of event structures with symmetry are degenerate 2-categories, the above describes a special case of weak 3-category, which we call a ∼-bicategory as it is morally a bicategory but where the axioms hold up to ∼.

Strat is rich in structure. Observe the duality: a strategy σ ∶ A + / / B corresponds to a strategy σ ⊥ ∶ B ⊥ + / / A ⊥ . There is a bijective correspondence between strategies A∥B + / / C and strategies A + / / (B ⊥ ∥C), making Strat monoidal closed, and in fact compact closed, in an extended sense.

To be more precise, and to relate to standard game semantics, we can quotient out the higher-dimensional structure to obtain a category. The category Strat ≃ has e.p.s.'s as objects, and ≃-equivalence classes of strategies σ ∶ S → A ⊥ ∥ B as morphisms from A to B. The ∼-bicategorical structure ensures that equivalence of strategies is preserved by composition, so we get a category Strat ≃.

Proposition 13. The category Strat ≃ is compact closed, with tensor product ∥ and dual (-) ⊥ .

The compact closed structure of Strat ≃ is not so surprising: the category is defined in a similar fashion to Joyal's category of Conway games [START_REF]Remarques sur la théorie des jeux à deux personnes[END_REF], which is compact closed as well. As compact closed categories, they are * -autonomous and hence models of Multiplicative Linear Logic (MLL) [START_REF] Melliès | Categorical semantics of linear logic[END_REF].

4) Weak strategies: A weak strategy is a pre-strategy which is weakly equivalent to γ A ⊙σ; so, directly from this definition, any weak strategy is weakly equivalent to a strategy. (We do not have a direct characterization of weak strategies.)

As we shall see, it is sometimes convenient to work with weak strategies (which need not be saturated) and then compose with copycat to obtain the strategies they represent.

Another potential advantage of weak strategies is that they are closed under a more general composition than that of strategies. We can build a ∼-bicategory of weak strategiesbiequivalent to the ∼-bicategory of strategies-in which instead composition is based on a choice of bipullbacks rather than pseudo-pullbacks. (See [START_REF] Winskel | Event structures with symmetry[END_REF] for the definition of bipullbacks of event structures with symmetry.) This extra latitude in the choice of definition of composition is likely to have technical advantages when working with sub ∼-bicategories of games, for which the saturation of strategies seems unnecessary or unnatural. Lemma 14. If two saturated pre-strategies are weakly equivalent they are equivalent. A fortiori, if two strategies are weakly equivalent they are equivalent.

IV. APPLICATIONS

Once we have symmetry in games we can support a rich repertoire of (pseudo) monads on e.p.s.'s, and e.g. all the monads of [START_REF] Winskel | Event structures with symmetry[END_REF] are undisturbed by the presence of polarity. Monads to support copying w.r.t. maps of e.p.s.'s can often translate to monads w.r.t. strategies, and so by duality also to comonads w.r.t. strategies. Following Girard's work on linear logic [START_REF] Girard | Linear logic[END_REF], this opens up the possibility of modelling programming languages that are not resource-sensitive, in that (copies of) the same resource can be used multiple times. We describe, in particular, how AJM games [START_REF] Abramsky | Full abstraction for PCF[END_REF] and HO games [START_REF] Hyland | On full abstraction for PCF: I, II, and III[END_REF] generalize and can be recovered from concurrent games. The (co)monads involved rely pivotally on the presence of symmetry. Their structure lifts from simple structural maps.

A. Maps as strategies

A structural pair f = (f L , f R ) ∶ A → B comprises • f L ∶ A → B,
a total map of e.p.s.'s, as left component, and • f R ∶ B → A, an injective, partial map of event structures, not necessarily preserving symmetry, as right component, such that f R ○ f L = id A . (Such pairs correspond to Kahn and Plotkin's rigid embeddings if we ignore symmetry.)

A structural pair f ∶ A → B, lifts to a strategy f ∶ S(f ) → A ⊥ ∥B, obtained via a rigid family Q. Whenever

x ⊇ + x ′ f L ↦ f L x ′ θ ≅ B y ′ ⊆ -y ,
with x, x ′ ∈ C(A) and y, y ′ ∈ C(B), define a typical q(x, θ, y) ∈ Q to have underlying set x ∥ y, and causal dependency that inherited from A ⊥ ∥ B with additional causal dependencies

{(a, θ(f L a)) ∈ x ′ × y ′ pol A ⊥ (a) = -}∪ {(θ(f L a), a) ∈ y ′ × x ′ pol A ⊥ (a) = +} .
The event structure S(f ) is then defined as Pr(Q), and the strategy-as-map f ∶ S(f ) → A ⊥ B by f (q) = a, where a is the top element of the prime q ∈ S(f ). Elements of the isomorphism family of S(f ) correspond to isomorphisms

x 1 ≅ ϕ1 A ⊇ + x ′ 1 ≅ ϕ2 A f ↦ f x ′ 1 ≅ f ϕ2 B θ ≅ B y ′ 1 ⊆ - ≅ ϕ3 B y 1 ≅ ϕ4 B x 2 ⊇ + x ′ 2 f ↦ f x ′ 2 θ ≅ B y ′ 2 ⊆ - y 2 .
This induces an isomorphism family because f L preserves symmetry, which by construction is preserved by f . Additionally, one can check that f is strong-receptive, innocent and saturated, so a strategy. Note that this lifting operation also preserves equivalence: if f ∼ g then it is easy to show that f and g are weakly equivalent, so equivalent by Lemma 14.

The following lemma relates composition of maps to that of their lifts as strategies.

Lemma 15. Let σ ∶ T → A be a strategy and f ∶ A → B be a structural pair. Then the pre-strategy

f L ○σ ∶ T → B is weakly equivalent to the strategy f ⊙ σ ∶ S(f ) ⊙ T → B.
From this lemma it follows easily that lifting is functorial. We also need to examine the composition of a strategy with the dual of one lifted from a structural pair. A right map f R ∶ B → A of a structural pair does not necessarily preserve symmetry, but it does preserve a sub-symmetry, in the sense that the set of isomorphisms

x θ ≅ B y, such that f R x f R θ ≅ A f R
y, forms an isomorphism family. Then B can be restricted to make f R a total map preserving symmetry. Write (B ↾ f R ) for the event structure with events those on which f R is defined and with isomorphism family that part preserved by f R . Obviously, f R ∶ (B ↾ f R ) → A is a total map preserving symmetry. Lemma 16. Let σ ∶ T → B be a strategy and f ∶ A → B a structural pair. Then f R ○ σ preserves a sub-symmetry, and

f R ○ σ ∶ (T ↾ f R ○ σ) → A is a strategy equivalent to the strategy (f ) ⊥ ⊙ σ ∶ S(f ) ⊙ T → A.

B. AJM games

We have not assumed that games are polarized, i.e. that initial moves share the same polarity, a condition imposed in most presentations of games. Non-polarized games are useful because they permit an account of negation as just polarityreversal, and hence model directly the involutive negation of Classical Linear Logic. In contrast, polarized games lose involutive negation and are restricted to modelling "polarized" logics, such as Intuitionistic Linear Logic (ILL). Through concurrent games we can give a concurrent version of the construction in [START_REF] Baillot | Believe it or not, AJM's games model is a model of classical linear logic[END_REF] of a non-polarized adaptation of AJM games [START_REF] Abramsky | Full abstraction for PCF[END_REF] to model CLL.

A categorical model of Multiplicative Exponential Linear Logic (MELL) is a * -autonomous category (C, ⊗) (such as Strat ≃) with a linear exponential comonad, i.e. a monoidal comonad (!, ǫ, δ, m) with monoidal natural transformations e A ∶ !A → 1 and d A ∶ !A → !A ⊗ !A such that each (!A, e A , d A ) is a commutative comonoid, e A and d A are coalgebra maps and any coalgebra map between free coalgebras is also a comonoid morphism. We aim to build this structure on Strat ≃. There is one proviso however. Just as in [START_REF] Baillot | Believe it or not, AJM's games model is a model of classical linear logic[END_REF], the absence of polarization means that the naturality of weakening e A ∶!A + / / I will be missing, so we model CLL in the sense of [START_REF] Baillot | Believe it or not, AJM's games model is a model of classical linear logic[END_REF] and not quite MELL. If we restrict to negatively polarized games the naturality of e A is recovered at the cost of selfduality, yielding a model of ILL.

From a game A, we form the game !A comprising ω similar copies of A. Its events are pairs (i, a) where a ∈ A and i ∈ ω, with causal dependency

(i 1 , a 1 ) ≤ (i 2 , a 2 ) ⇔ i 1 = i 2 & a 1 ≤ A a 2
and consistency relation

Con !A = ⋃ i∈I {i} × X i ,
where I is a finite subset of ω, and for each i ∈ I, X i ∈ Con A . Polarity is inherited from A. We describe its symmetry as an isomorphism family. If x, y ∈ C(!A), we have x θ ≅ !A y if, writing x = ⋃ i∈I {i}×x i and y = ⋃ j∈J {j}×y j with each x i and y j nonempty, there is a bijection π ∶ I ≅ J so x i θi ≅ A y π(i) for each i ∈ I, where θ((i, a)) = (π(i), θ i (a)) for all (i, a) ∈ x.

The construction extends to a functor on EPS: if f ∶ A → B then !f ∶ !A → !B sends (i, a) to (i, f (a)). It is convenient to investigate the monad/monoid structure of ! in EPS first, their duals will be eventually deduced by duality in Strat. In EPS, we have:

η A ∶ A → !A e A ∶ 1 → !A µ A ∶ !!A → !A m A ∶ !A ∥ !A → !A q A,B ∶ !(A ∥ B) → !A ∥ !B
where η A sends any event a to (0, a); µ A tracks an arbitrary bijection between ω×ω and ω; q A,B is the obvious distribution map; e A is the empty map; and m A tracks an arbitrary bijection between ω + ω and ω. All these maps are natural in their parameters in the category EPS. In particular, (!, η, µ) forms a monad on EPS.

The functors ∥ and ! on EPS extend to functors on strategies written ∥ S and ! S for disambiguation: given strategies

σ 1 ∶ S 1 → A ⊥ 1 ∥ B 1 and σ 2 ∶ S 2 → A ⊥ 2 ∥ B 2 , we have σ 1 ∥ S σ 2 ∶ S 1 ∥ S 2 → (A 1 ∥ A 2 ) ⊥ ∥ (B 1 ∥ B 2 )
given by the obvious map of EPS. To define ! S σ, the obvious choice is the composition

q A ⊥ 1 ,B1 ○ !σ ∶ !S → !A ⊥ 1 ∥ !B 1
, which we must then compose with copycat to obtain a strategy. These yield a bifunctor ∥ S and a functor ! S on strategies, using the fact that ! and ∥ preserve pseudo-pullbacks.

The natural tranformations above all have adjoints together with which they form structural pairs. By the techniques of Section IV-A, lifting maps to strategies, they become (apart from e A ) natural as families of strategies: Lemma 17. The strategies ǫ A , δ A , d A and q A,B are natural in A, B in the category Strat ≃.

Proof. Each of these maps f has an adjoint f • making (f, f • ) a structural pair. By Lemmas 15 and 16 the compositions involved in the naturality squares can be computed by simple composition of maps, and the equivalences then amount to elementary verifications.

The monoid and monad laws follow from those in EPS by functoriality of lifting. The fact that algebra morphisms between free algebras (!A, µ A ) satisfy the laws needed to be morphisms of monoids follows from a simple diagram chase, using that µ A is an invertible monoid morphism and that this property remains true of µ A .

We have established that the natural transformations above define the dual of a linear exponential comonad, short of the naturality of e A . By self-duality of Strat ≃, we have: Theorem 18. The category Strat ≃ with ! is a model of CLL in the sense of [START_REF] Baillot | Believe it or not, AJM's games model is a model of classical linear logic[END_REF].

C. HO games and HO-innocence

Finally, we sketch an application of our setting to construct a notion of concurrent games with pointers, obtaining a concurrent generalization of HO games. An e.p.s. A is negative when all its minimal events have negative polarity.

1) Concurrent games with pointers: An arena is a countable forest (A, ≤ A , pol A ) with polarities (but without conflict or symmetry), which is also negative, and alternating in the sense that if a 1 a 2 then pol A (a 1 ) ≠ pol A (a 2 ). From an arena A, we now define a game ! ?A understood as "A with pointers". Its definition requires the notion of an exponential slice: a slice for an event a is a function α ∶ [a] → ω, giving a copy index to each event on which a depends. For two slices α ∶ [a] → ω and α ′ ∶ [a ′ ] → ω, we write α ⊑ α ′ when a ≤ a ′ and α(b) = α ′ (b) for all b ≤ a. The game ! ?A has:

• events, pairs (α, a) where α ∶

[a] → ω, • causal dependency, (α, a) ≤ (α ′ , a ′ ) iff α ⊑ α ′ ,
• consistency, all finite subsets of ! ?A, • polarity, inherited from A, and • isomorphism family, order-isos θ ∶ x ≅ y such that for all (α, a) ∈ x there is α ′ ∶ [a] → ω with θ(α, a) = (α ′ , a).

To convey the similarity with the plays with pointers of HO games, we could say that (α, a) "points to" (α ′ , a ′ ) when α ′ ⊑ α and a ′ a. However ! ?A leaves duplicated events causally unrelated whereas they would appear in some chronological order in a play with pointers. Configurations of ! ?A are more closely related to the thick subtrees of Boudes [START_REF] Boudes | Thick subtrees, games and experiments[END_REF].

Games of the form ! ?A are comonoids in Strat ≃. Indeed, we have maps of event structures m A ∶ ! ?A ⊥ ∥ ! ?A ⊥ → ! ?A ⊥ and e A ∶ 1 → ! ?A ⊥ satisfying monoid laws up to symmetry, and the lifting operation yields strategies m A ⊥ ∶ ! ?A + / / ! ?A ∥ ! ?A and e A ⊥ ∶ ! ?A + / / 1 in Strat ≃, satisfying comonoid laws. We will now describe a subcategory of Strat ≃ whose morphisms preserve this comonoid structure.

2) A cartesian closed category: A strategy σ ∶ S → ! ?A ⊥ ∥ ! ?B is single-threaded iff (1) for all s ∈ S, [s] has exactly one minimal event, which is negative, and (2) there is a map ⟨-, -⟩ ∶ S ∥ S → S such that σ ○ ⟨-, -⟩ = (m ⊥ A ∥ m B ) ○ (σ ∥ S σ), and such that for all x 1 , x 2 ∈ C(S) disjoint and compatible, the composite bijection x 1 ∪ x 2 ≅ x 1 ∥ x 2 ≅ ⟨x 1 , x 2 ⟩ is in the isomorphism family of S. Single-threaded strategies are stable under composition, and lifting yields single-threaded strategies (so copycat is single-threaded).

Condition [START_REF] Ghica | Angelic semantics of fine-grained concurrency[END_REF] expresses that causality is local to threads (i.e. configurations with a unique minimal event), it will be used to decompose configurations of S into threads. On the other hand, condition (2) allows us to merge a set of threads back into a configuration; (1) and (2) together allow us to prove the following key lemma.

Lemma 19. Single-threaded strategies are comonoid morphisms for the comonoids (

! ?A, m A ⊥ , e A ⊥ ) in Strat ≃.
Since we want a category of comonoids and comonoid morphisms, we will now restrict our attention to singlethreaded strategies between games of the form ! ?A. An HOstrategy from arena A to arena B is a single-threaded strategy σ ∶ S → ! ?A ⊥ ∥ ! ?B. There is a category HOStrat having arenas as objects, and HO-strategies as morphisms.

Arenas are closed under ∥, and there are obvious isomorphisms ! ?(A ∥ B) ≅ ! ?A ∥ ! ?B and ! ?1 ≅ 1. Using these, HOStrat inherits from Strat ≃ its symmetric monoidal structure and terminal object. Moreover, arenas also inherit a comonoid structure that HO-strategies preserve by Lemma 19, hence (see e.g. Corollary 17 in [START_REF] Melliès | Categorical semantics of linear logic[END_REF]) HOStrat is cartesian.

We also need HOStrat to be monoidal closed. For that we introduce the usual arrow arena construction [START_REF] Hyland | On full abstraction for PCF: I, II, and III[END_REF], that (following [START_REF] Harmer | Categorical combinatorics for innocent strategies[END_REF]) we denote by A --⊞ B:

• events, (∥ b∈min(B) A) ∥ B where min(B) denotes the set of minimal events of B, and

• causality, that of ∥ b∈min(B) A ⊥ ∥ B enriched with {((2, b), (1, (b, a))) a ∈ A & b ∈ min(B)}.
• polarity, inherited in B and reversed in A. HO-strategies from A to B can be represented as HOstrategies on A --⊞ B through the following proposition.

Proposition 20. For any arenas A, B, C there is a bijection (up to equivalence) Φ

A,B,C between single-threaded σ ∶ ! ?C + / / ! ?A ⊥ ∥ ! ?B and single-threaded σ ′ ∶ ! ?C + / / ! ?(A --⊞ B). Moreover Φ preserves composition, in the sense that for all τ ∶ ! ?D + / / ! ?C we have Φ(σ ⊙ τ ) = Φ(σ) ⊙ τ .
Using this, the category HOStrat inherits the closed structure of Strat ≃. Since its monoidal product is actually cartesian, it is cartesian closed, hence a model of the simply-typed λ-calculus. It has in fact much more structure and we hope to be able to recast and generalize within it various games models of programming languages. In this paper though, we will only show that it contains (a nondeterministic generalization of) the usual HO category of innocent strategies.

3) Sequential HO-innocence: An HO-strategy σ ∶ S → ! ?A is sequential HO-innocent (or an HOIS-strategy) if for any s ∈ S, (1) the prime [s] is a total order, and (2) if [s] extends by distinct positive events s 1 , s 2 , then [s] ∪ {s 1 , s 2 } ∈ Con S .

Intuitively, a prime [s] corresponds to a P-view: just like a P-view, a prime configuration of an HOIS-strategy cannot contain two negative events s 1 , s 2 whose mapping to ! ?A "point" to the same event (α, a): by innocence s 1 and s 2 would have to be concurrent in [s], which is impossible by condition [START_REF] Ghica | Angelic semantics of fine-grained concurrency[END_REF]. So similarly to standard HO innocence the condition (1) expresses that the strategy σ is blind to Opponent reopenings: every Player event contains in its causal history at most one Opponent event pointing to a specific Player event.

Proposition 21. Arenas and sequential HO-innocent strategies form a subCCC, HOISStrat of HOStrat.

Note in passing that condition (1) is stable under composition on its own, but is too restrictive to be a satisfactory notion of concurrent HO-innocence as it forbids natural concurrent strategies such as that for the parallel or. We leave for future work the design and study of a more satisfactory notion of concurrent HO-innocence. We now go on and isolate a deterministic subcategory of HOISStrat, isomorphic to the usual category of arenas and innocent strategies [START_REF] Hyland | On full abstraction for PCF: I, II, and III[END_REF].

An HOIS-strategy σ ∶ S → ! ?A is deterministic iff whenever x ϕ ≅ S y and x + -⊂x ′ and y-⊂y ′ , then x ′ ⊆ x ′′ and y ′ ⊆ y ′′ for some x ′′ , y ′′ ∈ C(S) with ϕ ′ ∶ x ′′ ≅ S y ′′ such that ϕ ⊆ ϕ ′ -this is a generalization of the notion of deterministic concurrent strategies [START_REF] Winskel | Deterministic concurrent strategies[END_REF] in the presence of symmetry. In turn, immediate dependency in A equips this sequence with pointers such that (by innocence) Opponent always points to the previous move. In other words, this is a P-view.

Applying this to all primes in S we get a set of P-views that is O-branching by receptivity, condition (2) of HOISstrategies, the extension operation on S and determinism; so a deterministic innocent strategy in the sense of HO games.

This operation has an inverse up to equivalence of strategies and preserves composition, yielding an isomorphism of categories with standard innocent strategies.

V. CONCLUSION

Concurrent games with symmetry have proved versatile enough to accommodate and extend in a single framework two radically different fundamental games models: the saturated AJM games model of CLL and the HO innocent games model of the simply-typed λ-calculus, with a generalization to nondeterminism-in the past, providing a notion of nondeterministic HO innocence has proved challenging [START_REF] Harmer | Games and full abstraction for non-deterministic languages[END_REF]. The framework is grounded in the mathematically-versatile setting of event structures with symmetry, with potentially fruitful connections to homotopy.

In future, we intend to exploit the framework introduced here to develop concurrent-games models for various programming languages. Its versatility and its proximity to traditional game semantics suggests that it is adequate to give precise partial-order semantics to complex concurrent programming language, including such features as higher-order procedures and shared memory-features which, to our knowledge, have only been modelled through interleaving.

  The pseudo pullback is defined up to isomorphism, and sometimes written A × C B. Concretely, a configuration in C(A × C B) corresponds to a a triple x, f x θ ≅ C gy, y where the composite x ≅ f x θ ≅ C gy ≅ y is a secured bijection between x ∈ C(A) and y ∈ C(B) in the sense of Proposition 1.

Proposition 7 .

 7 . The composition τ ⊙σ of pre-strategies σ ∶ ∅ + / / B and τ ∶ B + / / C is saturated. Proof. Adopt the notation of the diagram defining the composition τ ⊙σ in Section III-B, with A = ∅. Let u ∈ C(T ⊙S). Its down-closure [u] is a configuration in the pseudo pullback P , and so corresponds to a secured bijection x∥v ϕ ≅ y where x ∈ C(S), v ∈ C(C) and y ∈ C(T ). Because we define τ ⊙σ to be got via the left way round the pseudo pullback square the configuration u is sent to v via τ ⊙σ. Consequently, given θ ∶ v ≅ C v ′ we can define act(u, θ) to be that configuration u ′ ∈ C(T ⊙S) with down-closure x∥v ′ x∥θ ≅ x∥v ϕ ≅ y in the pseudo pullback. Lemma 8. γ A is strong-receptive, innocent and saturated.

Theorem 22 . 2 .

 222 The subcategory of HOISStrat having arenas as objects and deterministic sequential HO-innocent strategies as morphisms is isomorphic to the usual category of arenas and innocent strategies.Sketch. Let σ ∶ S → !?A be a deterministic HOIS-strategy. For s ∈ S positive, the prime configuration [s] needs to be a chain s - . . s + , by condition (1) of HOIS-strategies along with innocence and the alternation and negativity conditions of arenas. This induces a sequence of moves of A: π 2 σ(s 0 )π 2 σ(s 1 ) . . . π 2 σ(s)

Acknowledgements Thanks to Martin Hyland for advice and encouragement and to the ERC for Advanced Grant ECSYM.


Pascal Lefèvre
email: pascal.lefevre@euler.univ-artois.fr

Etienne Matheron
email: etienne.matheron@euler.univ-artois.fr

Pascal Lef

Étienne Matheron

THE BLUM-HANSON PROPERTY FOR C(K) SPACES

come

introduction

The following intriguing result is usually referred to as the Blum-Hanson theorem (see [START_REF] Blum | On the mean ergodic theorem for subsequences[END_REF] and [START_REF] Jones | A note on the Blum-Hanson theorem[END_REF]): if T is a linear operator on a Hilbert space H with }T} ¤ 1, and if x H is such that T n x Ñ 0 weakly as n Ñ V, then the sequence pT n xq is"strongly mixing", which means that every subsequence of pT n xq converges to 0 in the Cesáro sense; in other words, lim

KÑV 1 K K i1
T n i x 0 for any increasing sequence of integers pn i q. (The terminology "strongly mixing" comes from [START_REF] Berend | Mixing sequences in Hilbert spaces[END_REF]).

Accordingly, a Banach space X is said to have the Blum-Hanson property if the Blum-Hanson theorem holds true on X; that is, if T is linear operator on X such that }T} ¤ 1, then every weakly null T -orbit is strongly mixing. For example, it was shown rather recently in [START_REF] Müller | Quasi-similarity of power-bounded operators and Blum-Hanson property[END_REF] that p pNq has the Blum-Hanson property for any p r1, Vq. On the other hand, it is known since [START_REF] Akcoglu | A couterexample to Blum-Hanson theorem in general spaces[END_REF] that CpT 2 q, the space of all continuous real-valued functions on the torus T 2 , does not have this property. Further results and references can be found in [START_REF] Lefèvre | Smoothness, asymptotic smoothness and the Blum-Hanson property[END_REF].

In this short note, we address the Blum-Hanson property for CpKq spaces. Our main result is the following: Theorem 1.1. Let K be a metrizable compact space. Then CpKq has the Blum-Hanson property if and only if K has finitely many accumulation points.

This will be proved in the next Section. In Section 3, we obtain in much the same way one nonmetrizable result, namely that the space V pNq CpβNq fails the Blum-Hanson property. Our two results can be put together to get a single theorem on the Blum-Hanson property for spaces of bounded continuous functions, which is done in Section 4. We conclude the paper by stating explicitely the "general principle" underlying our proofs. For the "if" part of the proof, we will make use of a result from [START_REF] Lefèvre | Smoothness, asymptotic smoothness and the Blum-Hanson property[END_REF] which is stated as Lemma 2.1 below.

Let X be a Banach space. For any x X and t R , set r X pt, xq : sup

" lim sup nÑV }x ty n } * ,
where the supremum is taken over all weakly null sequences py n q X with }y n } ¤ 1. Since r X pt, xq is 1-Lipschitz with respect to t, the quantity r X pt, xq ¡ t is nonincreasing and hence it has a limit as t Ñ V, possibly equal to ¡V. Actually, this limit is nonnegative if X does not have the Schur property, i.e. there is at least one weakly null sequence in X which is not norm null.

For the needs of the present paper only, we shall say that the Banach space X has property (P) if, for every weakly null sequence px k q X, it holds that (1) lim kÑV lim tÑV pr X pt, x k q ¡ tq 0 .

The result we need is the following; for the proof, see the Remark just after Theorem 2.1 in [START_REF] Lefèvre | Smoothness, asymptotic smoothness and the Blum-Hanson property[END_REF].

Lemma 2.1. Property (P) implies the Blum-Hanson property.

An extreme example of a space with property (P) is X : c 0 pNq. Indeed, if x c 0 and if pz n q is a weakly null sequence in c 0 , then lim sup

nÑV }x z n } V maxp}x} V , lim sup }z n } V q .
It follows that (¦) r c 0 pt, xq maxp}x}, tq , so that r c 0 pt, xq ¡ t 0 whenever t ¥ }x}, for any x c 0 .

Let us also note the following useful stability property, whose proof is straightforward.

Remark 2.2. If X 1 , . . . , X N are Banach spaces with property (P), then the V direct sum X 1 ¤ ¤ ¤ X N also has (P).

We can now start the proof of theorem 1.1.

Proof of Theorem 1.1. Let us denote by K I the set of all accumulation points of K. We may assume that K I $ r, since otherwise K is finite and hence CpKq is finite-dimensional.

(a) Assume first that K I is finite say K I ta 1 , . . . , a N u, and let us show that X : CpKq has the Blum-Hanson property.

One may write K K 1 ¤ ¤ ¤K N , where the K i are pairwise disjoint compact sets and K I i ta i u. Then CpKq is isometric to the V direct sum CpK 1 q ¤ ¤ ¤ CpK N q, and each CpK i q is isometric to the space c of all convergent sequences of real numbers. Therefore (by Lemma 2.1 and Remark 2.2) it is enough to show that the space c has property (P).

We view c as the space CpN tVuq, so that c 0 is identified with the subspace of all f CpN tVuq such that f pVq 0. We have to show that if pf k q is a weakly null sequence in c, then lim kÑV lim tÑV pr c pt, f k q ¡ tq 0 . Observe first that since f k pVq Ñ 0 as k Ñ V, one can find a (weakly null) sequence p r f k q c such that r f k c 0 for all k and } r

f k ¡ f k } V Ñ 0: just set r f k : f k ¡ f k pVq1.
Let pg n q be a weakly null sequence in c with }g n } V ¤ 1. As above, choose a (weakly null) sequence pr g n q c such that }r g n ¡ g n } V Ñ 0 and r g n c 0 for all n. Since }g n } V ¤ 1, we may also asume that }r g n } V ¤ 1 for all n. Then, since f k and the r g n are living in c 0 , we get from p¦q above that for any t R and for each k N:

lim sup nÑV } r f k tr g n } V ¤ r c 0 pt, r f k q maxp} r f k } V , tq .
By the triangle inequality, it follows that lim sup

nÑV }f k tg n } V ¤ } r f k ¡ f k } V maxp} r f k } V , tq
for each k N and all t ¥ 0. This being true for any weakly null sequence pg n q with }g n } V ¤ 1, we conclude that lim

tÑV pr c pf k , tq ¡ tq ¤ } r f k ¡ f k } V for each k N,
and hence that lim kÑV lim tÑV pr c pt, f k q ¡ tq 0 .

(b) Now assume that K I is infinite. Since K is metrizable, it follows that K contains a compact set S of the following form:

S V ¤ k1 ts i,k ; i Nu ts V,k u ts V,V u ,
where all the points involved are distinct and

s i,k Ñ s V,k as i Ñ V for each fixed k ¥ 1; s V,k Ñ s V,V as k Ñ V;
the sets S k : ts i,k ; i Nu ts V,k u "accumulate to ts V,V u", i.e. they are eventually contained in any neighbourhood of s V,V .

Thus, we have S I ts V,k ; k ¥ 1u ts V,V u and S P ts V,V u.

The key point is now to construct a special continuous map θ : S Ñ S and to consider the associated composition operator C θ acting on CpSq. This is the same strategy as in [START_REF] Akcoglu | A couterexample to Blum-Hanson theorem in general spaces[END_REF], in our setting.

Fact 1. One can construct a continuous map θ : S Ñ S such that, denoting by θ n the iterates of θ, the following properties hold true.

(i) θ n psq Ñ s V,V pointwise on S as n Ñ V;

(ii) there exists an open neighbourhood V of s V,V in S such that sup sS #tn N; θ n psq V u V .

Proof. We define the map θ as follows:

$ ' ' ' ' ' ' & ' ' ' ' ' ' % θps V,V q s V,V θps i,k q s i,k¡1 if k ¥ 2 θps V,k q s V,k¡1 if k ¥ 2 θps i,1 q s i¡1,i¡1 if i ¥ 2 θps V,1 q s V,V θps 1,1 q s V,V It is clear that θ is continuous at each point s V,k , k ¥ 2. Moreover, since s i¡1,i¡1 Ñ s V,V as i Ñ V, the map θ is also continuous at s V,1 and at s V,V .
Since all other points of S are isolated, it follows that θ is continuous on S.

An examination of the orbits of θ reveals that for any s S, we have θ n psq s V,V for all but finitely many n N. Indeed, if s s V,k for some k N, then Orbps, θq ts V,k , s V,k¡1 , . . . , s V,1 , s V,V u, whereas if s s i,k for some pi, kq N ¢N, then Orbps, θq ts i,k , s i,k¡1 , . . . , s i,1 , s i¡1,i¡1 , . . . , s i¡1,1 , s i¡2,i¡2 . . . , s 1,2 , s 1,1 , s V,V u.

So property (i) is satisfied.

Set V : SzS 1 , where S 1 ts i,1 ; i Nu ts V,1 u. This is an open (actually clopen) neighbourhood of s V,V in S. For any N N, the orbit of s N : s N,1 contains exactly N points of SzV S 1 , namely s N,1 , s N ¡1,1 , . . . , s 1,1 . So property (ii) is satisfied as well.

From Fact 1, it is straightforward to deduce Fact 2. The space CpSq does not have the Blum-Hanson property.

Proof. Let θ : S Ñ S be given by Fact 1, and let C θ : CpSq Ñ CpSq be the composition operator associated with θ:

C θ u u ¥ θ for all u CpSq.
By property (i) above, we see that C n θ u Ñ ups V,V q1 weakly as n Ñ V, for every u CpSq.

Let us choose a function f CpSq such that f ps V,V q 0 and f 1 on F : SzV , where V satisfies (ii). Then C n θ f Ñ 0 weakly. On the other hand, since f 1 on F it follows from (ii) that one can find points s S such that #tn N; C n θ f psq 1u is arbitrarily large. So we have

1 #I ņI C n θ f V ¥ 1
for finite sets I N with arbitrarily large cardinality. From this, it is a simple matter to deduce that the sequence pC n θ f q is not strongly mixing, which concludes the proof of Fact 2.

It is now easy to conclude the proof of Theorem 1.1, by using the following trivial observation.

Fact 3. Let X be a Banach space, and let Z be a closed subspace of X. Assume that Z is 1 -complemented in X, i.e. there is a linear projection π : X Ñ Z such that }π} 1. If Z fails the Blum-Hanson property, then so does X. Proof. If T : Z Ñ Z and z Z witness that Z fails the Blum-Hanson property, then r T : T ¥ π : X Ñ Z X and z witness that so does X.

It is well known that since K is metrizable, there is an isometric linear extension operator J : CpSq Ñ CpKq: this is a classical result due to Dugundji [START_REF] Dugundji | An extension of Tietze's theorem[END_REF]. So the space CpSq is isometric to a 1 -complemented subspace of CpKq, namely Z : J rCpSqs.

By Fact 3, this concludes the proof of Theorem 1.1.

Remark 1. The above proof shows that the space CpSq fails the Blum-Hanson property in a very special way. Namely, there exists a composition operator C θ on CpSq all whose orbits are weakly convergent and such that some weakly null orbit is not strongly mixing. As shown in [START_REF] Akcoglu | A couterexample to Blum-Hanson theorem in general spaces[END_REF], the same is true for the space CpT 2 q. On the other hand, it is observed in [START_REF] Lefèvre | Smoothness, asymptotic smoothness and the Blum-Hanson property[END_REF] that this is not so in the space Cpr0, 1sq, for the following reason: if θ : r0, 1s Ñ r0, 1s is a continuous map and if the iterates θ n converge pointwise to some continuous map α : r0, 1s Ñ r0, 1s, then the convergence is in fact uniform.

Remark 2. Our proof gives in fact the following more precise result: if K has finitely accumulation points, then CpKq has property (P); and otherwise, one can find an operator T on CpKq with }T} ¤ 1 such that all T -orbits are weakly convergent and some wealy null orbit is not strongly mixing.

One nonmetrizable example

We have been unable to show without the metrizability assumption on K that CpKq fails the Blum-Hanson property if K has infinitely many accumulation points. Note that metrizability was used twice in the proof of Theorem 1.1: to ensure that if K I is infinite then K contains the special compact set S; and for the existence of an isometric (linear) extension operator J : CpSq Ñ CpKq.

It is known that the linear extension theorem may fail in the nonmetrizable case (see e.g. [START_REF] Pelczyński | On simultaneous extensions of continuous functions[END_REF]Remark 2.3]). It may also happen that a compact set K has infinitely many accumulation points and yet does not contain any compact set like S. For example, this holds for K βN (the Stone-Čech compactification of N) because there are no nontrivial convergent sequences in βN. However, in this (very) special case it is possible to adapt the proof of Theorem 1.1 to obtain the following result. Proof. It will be more convenient to view V as V pN ¢ Nq CpβpN ¢ Nqq.

Let θ : N ¢ N Ñ N ¢ N be essentially the same map as in the proof of Theorem 1.1 but ignoring the limit points:

$ & % θpi, kq pi, k ¡ 1q if k ¥ 2 θpi, 1q pi ¡ 1, i ¡ 1q if i ¥ 2 θp1, 1q p1, 1q
We denote by C θ the asociated composition operator acting on V V pN ¢ Nq, i.e C θ f pi, kq f pθpi, kqq for every pi, kq N ¢ N . Set f : 1 F V pN ¢ Nq, where F tpi, 1q; i ¥ 1uztp1, 1qu tpi, 1q; i ¥ 2u. Exactly as in the proof of Theorem 1.1, one checks that the sequence pC n θ f q is not strongly mixing in V pN ¢ Nq. So it is enough to show that, on the other hand,

C n θ f Ñ 0 weakly in V pN ¢ Nq.
Viewing V pN ¢ Nq as CpβpN ¢ Nqq, we have to show that C n θ f pUq Ñ 0 for every ultrafilter U on N ¢ N. Let us fix such an ultrafilter U.

Since C n θ f C n θ 1 F 1 θ ¡n pFq when considered as an element of V pN ¢ Nq, we have for any n N:

C n θ f pUq " 1 if θ ¡n pFq U 0 if θ ¡n pFq U So we need to prove that if n is large enough, then θ ¡n pFq U.
Observe first that if we set S 1 : N¢t1u, then θ ¡n pS 1 qS 1 is finite for every n N. This is readily checked from the definition of θ. Indeed, for each s pi, 1q S 1 , the first n N such that θ n psq S 1 is at least equal (in fact, exactly equal) to i; so for each fixed n there are at most n points s S 1 such that θ n psq S 1 .

Since F S 1 and θ is finite -to-one, it follows that θ ¡n pFq θ ¡n I pFq is finite whenever n $ n I . Now, assume without loss of generality that θ ¡n pFq U for more than one n N.

Then, by what we have just observed, U contain a finite set. Hence, U is a principal ultrafilter, defined by some point s 0 N ¢ N. On the other hand, we know from the definition of the map θ that θ n ps 0 q p1, 1q for all but finitely many n N. Since p1, 1q F , it follows that θ ¡n pFq U for all but finitely many n.

From Proposition 3.1, we immediately deduce Corollary 3.2. The space L V L V p0, 1q does not have the Blum-Hanson property.

Likewise, if His an infinite-dimensional Hilbert space, then the space BpHq of all bounded operators on H does not have the Blum-Hanson property.

Proof. This is clear since these two spaces contain a 1 -complemented isometric copy of V . To conclude this paper, and since this may be useful elsewhere, we isolate the following kind of criterion for detecting the failure of the Blum-Hanson property in C b pTq for a not necessarily metrizable topological space T . Lemma 4.2. Let T be a Hausdorff topological space. Assume that there exists a subset S of T which is normal as a topological space, such that the following properties hold true.

(1) One can find a continuous map θ : S Ñ S and a point a S such that (i) θ n psq Ñ a pointwise on S as n Ñ V; Since W V by (iii) and S is normal, one can choose a function f C b pSq such that f 0 on W and f 1 on F : SzV . By condition (ii) in (1), the sequence pC n θ f q is not strongly mixing; so we just need to check that C n θ f Ñ 0 weakly in C b pSq.

Being Hausdorff and normal, the space S is completely regular; so the space C b pSq is canonically isometric with CpβSq, where βS is the Stone-Čech compactification of S. The latter can be described as the space of all z-ultrafilters on S, i.e maximal filters of zero sets for functions in C b pSq, or, equivalently (since S is normal) maximal filters of closed subsets of S; see [START_REF] Gillman | Rings of continuous functions[END_REF]. Therefore, what we have to do is to show that lim nÑV lim U f pθ n psqq 0 for any z-ultrafilter U on S .

If U is a "principal" z-ultrafilter defined by some s 0 S, i.e. U is convergent with limit s 0 , then lim U f pθ n psqq f pθ n ps 0 qq for all n, so the result is clear since f pθ n ps 0 qq Ñ f paq 0 as n Ñ V by (i). Now, let us assume that U is not principal. Then U does not contain any finite set. Indeed, if a maximal filter of closed sets contains a finite union of closed sets F 1 ¤ ¤ ¤ F N , then it has to contain one of the F i by maximality; so, if U were to contain a finite set, then it would contain a singleton and hence would be principal in a trivial way. By (iii), it follows that θ ¡n pSzWq U for all but finitely many n N; and since U is a maximal filter of closed sets, this implies that θ ¡n pWq U for all but finitely many n. Since f 0 on W , it follows that lim U f pθ n psqq 0 for all but finitely many n, which concludes the proof.

Remark 1. This lemma would be much neater if condition (iii) above could be dispensed with; but we don't know how to prove the lemma without it. The proof of Theorem 1.1 shows that when S is compact, (i) and (ii) alone are enough for CpSq to fail the Blum-Hanson property. At the other extreme, the proof of Proposition 3.1

shows that when S is discrete (and infinite), one can find a map θ : S Ñ S satisfying (i), (ii) and a property stronger than (iii).

Remark 2. When S is compact, condition (iii) actually follows from (i). Indeed, let W be any open neighbourhood of a, and assume that (iii) fails for W and some infinite set N N. Then, by compactness we have nN θ ¡n pSzWq $ r. But if s nN θ ¡n pSzWq then θ n psq does not tend to a as n Ñ V, which contradicts (i).

1 2 .

 2 Proof of Theorem 1.1

Proposition 3 . 1 .

 31 The space V pNq CpβNq does not have the Blum-Hanson property.

4 .

 4 Further remarksFor any topological space E, let us denote by C b pEq the space of all real-valued, bounded continuous functions on E. Putting together Theorem 1.1 and Proposition 3.1, we obtain the following result.

Theorem 4 . 1 .

 41 If T is a metrizable topological space, then C b pTq has the Blum-Hanson property exactly when T is compact and has finitely many accumulation points. Proof. By Theorem 1.1, it is enough to show that if C b pTq has the Blum-Hanson property, then T is compact. Now, if T is not compact, it contains a countably infinite closed discrete set S (thanks to the metrizability assumption). By Dugundji's extension theorem, C b pTq then contains a 1 -complemented isometric copy of C b pSq. Since C b pSq is isometric to V pNq, it follows from Proposition 3.1 that C b pTq does not have the Blum-Hanson property.

( 2 )

 2 ii) there exists an open neighbourhood V of a such that sup sS #tn N; θ n psq V u V ; (iii) there exists a further open neighbourhood W of a with W V such that, for any infinite set N N, one can find n 1 , . . . , n p N such that the set θ ¡n 1 pSzWq ¤ ¤ ¤ θ ¡np pSzWq is finite. (There is a linear isometric extension operator J : C b pSq Ñ C b pTq. Then, one can conclude that the space C b pTq fails the Blum-Hanson property. Proof. By (2), it is enough to show that C b pSq does not have the Blum-Hanson property. This will of course be done by considering the composition operator C θ : C b pSq Ñ C b pSq.