Matteo Capucci

Neil Ghani

Clemens Kupke

Jérémy Ledent

Fredrik Nordvall Forsberg

Infinite Horizon Extensive Form Games, Coalgebraically

Introduction

Game theory is the study of how agents make decisions in order to maximise their outcomes [START_REF] Osbourne | A course in game theory[END_REF][START_REF] Leyton-Brown | Essentials of Game Theory: A Concise Multidisciplinary Introduction[END_REF]. A strategy profile describes how each agent will play the game, and is said to be a Nash equilibrium if no player has any incentive to deviate from their strategy; it is called subgame perfect if it is a Nash equilibrium in every subgame of the game. In a series of papers [START_REF] Bridges | Preference and utility: A constructive development[END_REF][START_REF] Bridges | The constructive theory of preference relations on a locally compact space[END_REF][START_REF] Bridges | The constructive theory of preference relations on a locally compact space II[END_REF][START_REF] Bridges | First steps in constructive game theory[END_REF], Douglas Bridges investigated constructive aspects of the theory of games where players move simultaneously (so-called normal form games), and their preference relations. This article is concerned with a constructive treatment of games where players move sequentially.

A common way to model sequential games is using their extensive form: a game is represented as a tree, whose branching structure reflects the decisions available to the players, and whose leaves (corresponding to a complete 'play' of the game) are decorated by payoffs for each player. When the number of rounds in the game is infinite (e.g. because a finite game is repeated an infinite number of times, or because the game may continue forever), the game tree needs to be infinitely deep. One way to handle such infinite trees is to consider them as the metric completion of finite trees, after equipping them with a suitable metric [START_REF] Mycielski | A compactification of the algebra of terms[END_REF]. However, as a definitional principle, this only gives a method to construct functions into other complete metric spaces, and the explicit construction as a quotient of Cauchy sequences (Bishop and Bridges, 1985, §4.3) can be unwieldy to work with. Instead, we prefer to treat the infinite as the dual of the finite, in the spirit of category theory and especially the theory of coalgebras [START_REF] Rutten | Universal coalgebra: a theory of systems[END_REF].

We are not the first to attack infinite extensive form games using coalgebraic methods. [START_REF] Lescanne | A simple case of rationality of escalation[END_REF][START_REF] Lescanne | Dependent types for extensive games[END_REF], [START_REF] Lescanne | Backward" coinduction, Nash equilibrium and the rationality of escalation[END_REF] and [START_REF] Abramsky | Coalgebraic analysis of subgame-perfect equilibria in infinite games without discounting[END_REF] define infinite two-player games coalgebraically, and show that coinductive proof methods can be used to constructively prove properties of games. However, their definition only assigns utility to finite plays. For that reason, they restrict attention to strongly convergent strategies, i.e., strategy profiles that always lead to a leaf of the tree in a finite number of steps. This restriction rules out infinitely repeated games, where utility could be assigned using discounted sums or limiting averages -both methods crucially making use of the entire infinite history of the game. Building on our on work on infinitely repeated open games [START_REF] Ghani | A compositional treatment of iterated open games[END_REF], we extend Lescanne's and Abramsky and Winschel's coalgebraic framework to not necessarily convergent strategies.

The one-shot deviation principle is a celebrated theorem of classical game theory. It asserts that a strategy is a subgame perfect equilibrium if and only if there is no profitable one-shot deviation in any subgame. While this principle holds for all finite games, in the case of infinite trees, it requires an extra assumption called continuity at infinity (see e.g. Fudenberg and Tirole (1991, Chapter 4.2)). Essentially, this property says that the actions taken in the distant future have a negligible impact on the current payoff. In the coalgebraic setting, [START_REF] Abramsky | Coalgebraic analysis of subgame-perfect equilibria in infinite games without discounting[END_REF] claim to prove the one-shot principle without continuity assumptions -we argue that this is not entirely the case. Indeed, they show that the natural coalgebraic equilibrium concept (which they call "SPE") satisfies the one-shot deviation principle. However they do not discuss how this coalgebraic concept relates to the traditional notion of subgame perfect Nash equilibria. As we show in Theorem 31, these two notions are indeed equivalent, but only assuming continuity of the utility function. In that regard, the predicate "SPE" of Abramsky and Winschel (called □Unimprov in our work) is in fact closer to a coalgebraic version of the one-shot equilibrium.

Our proof of the one-shot deviation principle extends the previous ones in several ways. Compared to the one of [START_REF] Abramsky | Coalgebraic analysis of subgame-perfect equilibria in infinite games without discounting[END_REF], it applies to games where infinite plays are possible; and it relates to the more standard definition of subgame-perfect Nash equilibrium, □Nash. Additionally, our theorem applies to any coalgebra of the extensive-form tree functor, whereas Abramsky and Winschel only work with the final coalgebra. Compared to the usual proofs found in the game theory literature, we carefully analyse the constructivity of the proof. The only extra assumption that we require is decidable equality on the set of players (which is typically finite), and decidability of the order relation on the set of payoffs (typically, the set of rational numbers). Moreover, continuity at infinity is usually expressed using uniform continuity; we remark that pointwise continuity suffices.

Structure of the paper

We recall the basics of coalgebras for endofunctors in Section 2. In Section 3, we define infinite extensive form games as final coalgebras, and use properties of coalgebras to define notions such as strategies, moves, payoffs and equilibria in a game. We then relate our coalgebraic notions with the existing notions from the literature in Section 4. Throughout the paper, we demonstrate how coinductive proof principles can be used to reason constructively about infinite games.

Notation We use P : Set → Set for the covariant powerset functor mapping a set to its set of subsets. Given a set-indexed collection of sets Y : I → Set and i ∈ I, we write interchangably Y i or Y (i) for the ith component of the collection. The dependent sum i∈I Y i is the disjoint union of all of the sets Y i in the collection, with elements pairs (i, y) where i ∈ I and y ∈ Y i , while the dependent function space i∈I Y i is the set of functions mapping an input i ∈ I to an element of Y i . We write A + B for the disjoint union of two sets A and B, with injections inl : A → A + B and inr : B → A + B. We denote the set of natural numbers by N, the set of positive natural numbers by N + , and write [n] = {0, . . . , n -1} for a canonical n-element set. We also write 1 = [1], 2 = [2] and so on for fixed small finite sets.

Coalgebraic Preliminaries

We assume familiarity with basic category theory.

Final coalgebras

Let C be a category and F : C → C an endofunctor. An F -coalgebra is a pair (A, α), where A is an object of C, and α : A → F A is a morphism. An Fcoalgebra homomorphism from (A, α) to (B, β) is a morphism f : A → B preserving the coalgebra structure, i.e. such that the following diagram commutes:

A α / / f F A F (f ) B β / / F B
F -coalgebras and F -coalgebra homomorphisms form a category. If F is well behaved (e.g. finitary), this category will have a final object, called the final F -coalgebra, and denoted (νF, out). Its universal property is a corecursion or coinduction principle: for every F -coalgebra (A, α), there exists a unique coalgebra homomorphism unfold : (A, α) → (νF, out). We will make use of Lambek's Lemma, which says that for a final coalgebra (νF, out), the map out : νF → F (νF ) is an isomorphism.

Coinductive families and predicates

Let I be a set. The category Set I of I-indexed families of sets is the category whose objects are functors from I (viewed as a discrete category) to Set, and whose morphisms are natural transformations. In other words, given two I-indexed families P and Q, a morphism f : P → Q in Set I is a family of functions f i : P i → Q i for each i ∈ I.

A coinductive family indexed by I is the final coalgebra νG of an endofunctor G on Set I . Its corresponding "coinduction principle" says that for every G-coalgebra (P, g), there exists a unique morphism unfold : P → νG making the following diagram in Set I commute:

P g / / unfold G(P ) G(unfold) νG out / / G(νG)
Let us spell out this principle. It says that for every I-indexed family P , if there is a family of functions g i : P i → G(P ) i , then there is a unique family of morphisms unfold i : P i → νG i commuting with the coalgebra maps.

In particular, we will be interested in coinductive families indexed by the carrier X of a coalgebra (X, γ) of a functor F : Set → Set, in which case there is a canonical way to obtain coinductive families via predicate liftings of F , as we now explain.

A (proof-relevant) predicate lifting of a functor F : Set → Set is a natural transformation {φ X : Set X → Set F X } X∈Set . Given an F -coalgebra (X, γ : X → F X) and a predicate lifting φ of F , we can define an endofunctor on Set X by Set X φ X / / Set F X -•γ / / Set X and consider its final coalgebra. Similarly, in Section 3.3, we also use proofirrelevant predicate liftings {φ X : P(X) → P(F X)} X∈Set .

Infinite Extensive Form Games

In the game theory literature [START_REF] Kuhn | Extensive games and the problem of information[END_REF][START_REF] Selten | Reexamination of the perfectness concept for equilibrium points in extensive games[END_REF][START_REF] Leyton-Brown | Essentials of Game Theory: A Concise Multidisciplinary Introduction[END_REF], extensive form games are typically defined using a non-recursive formulation. We take advantage of a more categorical presentation, as it is more compact, supports (co-)recursive function definitions and (co-)inductive reasoning, and smoothly generalises to richer semantic domains, e.g. metric, probabilistic and topological spaces. Throughout this section, let P be a finite set of players.

In this work we separate the description of an extensive form game into its 'tree' part, representing the dynamical structure of the game, and its 'payoff' part, classically given as a decoration on the leaves. The reason we do so stems from our goal of treating infinite games, where plays may be infinite. In that case, the correspondence between leaves and paths in the tree breaks down, making decorations on the leaves an ill-suited device to specify payoff functions.

Below we define first the tree part of a game (Definition 1), then the family of payoffs over a given extensive form tree (Definition 10), and finally an "extensive form game" as a combination a given tree part with a payoff over it (Definition 13). During our journey to the latter definition, we also define the set of moves of a game as paths in its tree (Definition 7), and the set of strategy profiles as choices of a branch for each node of the tree (Definition 4). These are fundamental ingredients in the description and analysis of a game. Definition 1. The set ETree ∞ of infinite extensive form game trees with players P is the final coalgebra (ETree ∞ , out ETree ∞ ) of the functor F ETree : Set → Set defined by

F ETree (X) = 1 + P × n∈N + X n .
This supports the Haskell-like data type

data ETree ∞ = Leaf | Node P (n : N + ) ([n] → ETree ∞ )
Concretely a tree T ∈ ETree ∞ is either a leaf, indicating no further plays are possible, or an internal node labeled with a player p ∈ P who is to play at that point in the game, and an arity n ∈ N + representing the number of different moves available, followed by n subtrees. Crucially, being a final coalgebra, ETree ∞ includes paths of infinite depth.

Example 2 (Dollar Auction). The Dollar auction is an infinite game introduced by [START_REF] Shubik | The dollar auction game: A paradox in noncooperative behavior and escalation[END_REF] to exemplify a situation of 'rational escalation'. The game has two players, A and B, bidding over a dollar bill. Player A bids first and then players alternate turns. At each turn, a player chooses between two actions:

• quit, in which case the game ends and the other player wins the $1.

• bid, which costs $0.1, and yields the turn to the other player.

turn A turn B turn A • • • ($0, $1) ($0.9, $0) (-$0.1, $0.9) • • • bid quit bid quit bid quit
Notice that when players bid, they immediately pay and are not refunded in case they lose the auction. The tree part of this game can be defined by mutual corecursion:

Dollar A = Node A 2 (Leaf, Dollar B ) Dollar B = Node B 2 (Leaf, Dollar A )
Then Dollar := Dollar A , as A moves first. As an F ETree -coalgebra, Dollar is defined starting from the coalgebra (D, δ), where D = {turn A , turn B , end}, P = {A, B} and δ is defined by:

δ : D -→ 1 + P × n∈N + D n δ turn A = inr (A, 2, (end, turn B )) δ turn B = inr (B, 2, (end, turn A )) δ end = inl *
The coalgebra (D, δ) can be represented by the automaton below, where the two elements of 2 are named quit and bid: By terminality of (ETree ∞ , out ETree ∞ ), there is a unique map unfold (D,δ) : (D, δ) → (ETree ∞ , out ETree ∞ ), and we define Dollar := unfold (D,δ) (turn A ). Thus, Dollar is the following infinite tree:

Node A Node B Node A Node B • • • Leaf Leaf Leaf Leaf bid quit bid quit bid quit bid quit
The payoff decoration making this into the dollar auction game will be discussed later in Example 11.

Example 3 (Repeated games). Let T be a finite, perfect-information, extensive-form game, with set of players P . Such games (without utility information) are represented as the elements of the initial algebra of F ETree (see Capucci et al. (2021, Section 2)). Any such tree can be converted to an F ETree -coalgebra given by the automaton whose states and transitions correspond, respectively, to nodes and branches of T .

If we now identify the final states (given by leaves of T ) with the initial state (given by the root of T ) of the automaton, we get another F ETreecoalgebra (Rep T , ρ T ): the repeated game coalgebra.

By terminality of (ETree ∞ , out ETree ∞ ), there is a unique map

unfold (Rep T ,ρ T ) : (Rep T , ρ T ) → (ETree ∞ , out ETree ∞
), and we define

T ∞ := unfold (Rep T ,ρ T ) (root).
One concrete example is the Market Entry game [START_REF] Selten | The chain store paradox[END_REF], a game with players P = {A, B} described by the extensive-form tree M (here with payoff-labeled leaves):

A B (2, 2) (1, 5) (0, 0) in out accom fight
Player A decides whether to enter a new market or not. If staying out, the game ends, but if A enters then player B has to decide whether to accommodate or fight the incumbent. In this case (Rep T , ρ T ) corresponds to the automaton:

A B in out accom fight
The induced infinite tree M ∞ is then given by Throughout the section, let (X, γ) be an F ETree -coalgebra.

A B A B • • • A • • • A • • • A • • • A • • • . . . . . . . . . . . .

Strategy profiles

A strategy profile for the coalgebra (X, γ) at state x ∈ X consists of a choice of an action at each node in the game tree induced by (X, γ). Recall that an element of F ETree (X) is either a leaf (of the form inl * ) or an internal node of the form inr (q, n, f ), where q is a player, n ∈ N + , and f :

[n] → X.
February 26, 2024 20:58 ws-rv9x6 Book Title main page 9

Infinite Horizon Extensive Form Games, Coalgebraically Definition 4. We define the family of strategy profiles prof (X,γ) : X → Set as the final coalgebra associated with the predicate lifting

φ prof,X : (X → Set) → F ETree (X) → Set φ prof,X P (inl * ) = 1 φ prof,X P (inr (q, n, f )) = [n] × a∈[n] P f (a)
i.e. we define prof (X,γ) as the final coalgebra of the functor

F Prof : Set X → Set X defined by F Prof (P ) = φ prof,X (P ) • γ.
That prof (X,γ) is the final coalgebra implies that for every x ∈ X, there is an isomorphism s

x : prof (X,γ) (x) → φ prof,X (prof (X,γ) )(γ(x)). If γ(x) = inr (q, n, f ), we thus have s x (σ) ∈ [n] × a∈[n] prof (X,γ) (f a)
and we write s x (σ) = (now σ, next σ). Intuitively, now σ ∈ [n] is the branch chosen by player q in the current node x of the game tree; and next σ is a function assigning, for every branch a ∈ [n] -not only the one chosen by player q -a strategy profile next σ a ∈ prof (X,γ) (f (a)) starting at node f (a).

Example 5 (Dollar Auction (continues from Example 2)). For the Dollar game of Example 2, we would expect the set of strategy profiles to be isomorphic to 2 N , since a strategy profile selects, for every node of the game, an action in 2 ∼ = {bid, quit}.

Formally, we check that prof (D,δ) : D → Set is the following family of sets, where (D, δ) is the coalgebra that defines the Dollar game in Example 2.

prof (D,δ) (x) ∼ = 1 if x = end 2 N if x = turn A , turn B
Indeed, a function σ ∈ 2 N contains exactly the data of a strategy profile in prof (D,δ) (turn A ), since we can define

now σ = σ(0) ∈ 2 next σ quit = * ∈ 1 ∼ = prof (D,δ) (end) next σ bid = (n → σ(n + 1)) ∈ 2 N ∼ = prof (D,δ) (turn B )
and similarly for a profile σ ∈ prof (D,δ) (turn B ). It is straightforward (but cumbersome) to check that this satisfies the universal property of the final coalgebra of F Prof .

Example 6 (Repeated games (continues from Example 3)). For a finite game T , we have defined in Example 3 its repeated game coalgebra (Rep T , ρ T ), whose unfolding is the infinitely repeated game T ∞ . A strategy profile for (Rep T , ρ T ) with initial state x is the greatest solution to

prof (Rep T ,ρ T ) (x) ∼ = {strategy profiles of T | x } × ℓ∈leaves x prof (Rep T ,ρ T ) (root)
where T | x is the subtree of T starting at x ∈ Rep T , root is the state corresponding to the root of the tree T , and leaves x denotes the set of leaves in the subtree T | x . In the concrete case of the market entry game, this becomes (where we put prof M = prof (Rep M ,ρ M ) to ease notation):

prof M (A) ∼ = {in, out} × {fight, accom} × prof M (A) × prof M (A) × prof M (A) 3 leaves accessible from A prof M (B) ∼ = {fight, accom} × prof M (A) × prof M (A) 2 leaves accessible from B Therefore prof M (A) is the final coalgebra of the functor X → {in, out} × {fight, accom} × X 3 3.1.2. Moves
The set of moves in the game is the set of paths in the tree, which is another coinductive family.

Definition 7. We define the family of moves moves : X → Set as the final coalgebra associated with the predicate lifting

φ moves,X : (X → Set) → F ETree (X) → Set φ moves,X P (inl * ) = 1 φ moves,X P (inr (q, n, f )) = a∈[n] P f (a)
i.e. we define moves (X,γ) as the final coalgebra of the functor F moves : Set X → Set X defined by F moves (P ) = φ moves,X (P ) • γ.

Again, for every x ∈ X, we have an isomorphism m Note that, as m x is iso, if γ(x) = inr (q, n, f ) then for each a ∈ [n] and π ′ ∈ moves (X,γ) (f a) there is a unique element cons(a, π ′ ) ∈ moves (X,γ) (x) such that m x (cons(a, π ′ )) = (a, π ′ ). Intuitively, cons(a, π ′ ) represents a path in the game tree starting at node x, where the first chosen branch is a ∈ [n], and the following branches are chosen according to the path π ′ .

x : moves (X,γ) (x) → φ moves,X (moves (X,γ) )(γ(x)). If γ(x) = inr (q, n, f ), we have m x (π) ∈ a∈[n] moves (X,γ) (f a)
Example 8 (Dollar Auction (continues from Example 5)). The moves of Dollar are given by the final coalgebra of X → 1 + X, i.e. moves(Dollar) ∼ = 1 + moves(Dollar) The final coalgebra of this functor is known as the conatural numbers (N ∞ , pred), which include all finite natural numbers and an 'infinite' number ω. The map pred sends 0 ∈ N ∞ to inl * and every other natural number to the right injection of its predecessor. The predecessor of ω is itself, pred ω = inr ω. Note that it is not decidable if a given conatural number x is finite or infinite; however, by applying pred a finite number of times, we can decide if x ≥ n for any finite natural number n.

We interpret n ∈ moves(Dollar) as the path starting from the root and ending at the n-th leaf, i.e. the play where players bid n times before one of them * decides to quit. The unique infinite play ω corresponds to infinite escalation, with players never quitting.

Similarly, moves (D,δ) is given by These are all accessible from A, therefore M ∞ has set of moves specified by the final coalgebra of X → 3 × X which is readily seen to be 3 N . Indeed, a move of the repeated game is a move for every stage game. On the other hand, only moves 2 and 3 are accessible from B, therefore we get

moves (D,δ) (x) ∼ = 1 if x = end N ∞ if x = turn A ,
moves (Rep M ,ρ M ) (x) ∼ = 3 × 3 N if x = A 2 × 3 N if x = B *
The player who quits can be determined from the parity of n.

Evaluating strategies

In order to compare strategies, we need a way to assign a payoff to them. This is done in two steps: the play function turns a strategy profile into a sequence of moves; and the payoff function explains how outcomes turn into rewards for the players. This will allow us, in Section 3.3, to define several equilibrium concepts, i.e., predicates on strategy profiles that express when all players are happy with their given rewards.

The Play Function

We can use the universal property of final coalgebras to define a play function play (X,γ) : prof (X,γ) → moves (X,γ) which computes the sequence of moves generated by playing according to a strategy profile.

To define play (X,γ) : prof (X,γ) → moves (X,γ) , we use the finality of moves (X,γ) , i.e., we want to give prof (X,γ) a F moves -coalgebra structure. It is sufficient to give, for X) , which we can do as follows.

Q ∈ Set X , a natural transformation p Q : φ prof,X (Q) → φ moves,X (Q) in Set F ETree (
p Q (inl * ) * = * p Q (inr (q, n, f )) (a, σ) = (a, σ(a))
Instantiating at component Q = prof (X,γ) and composing with the isomorphism s x gives prof (X,γ) a F moves -coalgebra structure, as required. Hence there is a unique family of functions play (X,γ) (x) : prof (X,γ) (x) → moves (X,γ) (x), which, up to the isomorphisms s x and m x , satisfies the following definition.

play ∈ x∈X prof (X,γ) (x) → moves (X,γ) (x) play(x, * ) = * when γ(x) = (inl * )
play(x, (a, σ)) = (a, play(f (a), σ(a))) when γ(x) = inr (q, n, f )

Payoff functions and the game coalgebra

From now on, let R be a set of 'rewards' or 'payoffs'. Common choices are R = Q, the rational numbers or R = R, the real numbers, but dealing with infinite plays quickly leads to contemplating infinite rewards (negative and positive) as well. We assume R is ordered, and eventually, we will need to assume that this order is trichotomous. Recall that we denote by P the set of players. We write R P for the set of functions R → P , representing choices of payoffs for each of the players.

February 26, 2024 20:58 ws-rv9x6 Book Title main page 13

Infinite Horizon Extensive Form Games, Coalgebraically Definition 10. A payoff function for an F ETree -coalgebra (X, γ) at state x ∈ X is a function

u : moves (X,γ) (x) → R P .
The set of payoff functions for each x ∈ X is denoted by pay (X,γ) (x).

Example 11 (Dollar Auction (continues from Example 8)). Recall that moves (D,δ) (turn p ) is given by the conatural numbers. The payoff function for the Dollar Auction game (where R = [-∞, +∞) † ) can be defined in two steps. First, we coinductively define a map into colists ‡ of payoffs List ∞ R P (which we think of as 'ledgers'):

led ∈ x∈D moves (D,δ) (x) → List ∞ R P led end * = Empty led turn A m = (A → 0, B → 1) :: Empty pred m = inl * (A → -0.1, B → 0) :: (led turn B n) pred m = inr n led turn B m = (A → 1, B → 0) :: Empty pred m = inl * (A → 0, B → -0.1) :: (led turn A n) pred m = inr n
Then the actual utility function is given by summing up componentwise all the payoffs collected by the players during the game:

u Dollar m = +∞ n=0 p i , where p = led turn A m
Here p i is defined to be zero when i is greater than the length of p.

In the case of m = ω, this will unfold into an infinite sum where the summands alternate between (A → -0.1, B → 0) and (A → 0, B → -0.1), therefore yielding the payoff vector (A → -∞, B → -∞).

Example 12 (Repeated games (continues from Example 9)). The payoff function of an infinitely repeated game is obtained similarly to the previous example: 'partial' payoffs are summed at each iteration of the stage game. Unlike the Dollar Auction however, in an infinitely repeated game all plays are infinite, therefore discounting has to be adopted. This means that at each stage of the game, payoff vectors are uniformly scaled by a discount † We assume that -∞ + m = -∞ for every m ∈ R. ‡ Colists of A are 'possibly infinite lists', i.e. terms of the final coalgebra of X → 1+A×X for a given A. We denote inl * as Empty and inr (a, x) as a :: x. factor 0 < δ < 1. Discounting reflects the real-world tendency to value future payoffs less than present ones.

Thus let v T ∈ x∈Rep T leaves(x) → R P be the utility function of the (finite) stage game T (such as the one represented by the diagram of M in Example 3). For a given discount factor δ, we get a payoff function

u δ T ∞ ∈ x∈Rep T moves (Rep T ,ρ T ) (x) → R P by setting (recall that moves (Rep T ,ρ T ) (x) = (leaves x) × (leaves root) N ): u δ T ∞ x (m 0 , ms) := (v T x m 0 ) + +∞ i=0 δ i+1 • (v T x (ms i)).
The assumption of |δ| < 1 guarantees the convergence of such a sum.

We are now ready to define the "game coalgebra" -an F ETree -coalgebra which will enable us to study equilibria. We do this by collecting all the information needed: the current state of the game, a strategy profile, and a payoff function.

Definition 13. Let (X, γ) be an F ETree -coalgebra. The game coalgebra (Z (X,γ) , Γ) is the F ETree -coalgebra with carrier set

Z (X,γ) = x∈X prof (X,γ) (x) × pay (X,γ) (x)
and dynamics given by the map Γ defined by

Γ(x, σ, u) = inl * if γ(x) = inl * inr (q, n, a → (f a, next σ a, u a )) if γ(x) = inr (q, n, f )
where u a (π ′ ) = u(cons(a, π ′ )), for a ∈ [n] and π ′ ∈ moves (X,γ) (f a).

Equilibrium concepts

We are now going to introduce the equilibrium concepts for our games: a 'one-shot' equilibrium concept that expresses that no player can improve their payoff by unilaterallty deviating from their strategy in exactly one state, and the usual Nash equlibrium that expresses that none of the players can change their strategy unilaterally (at possibly arbitrarily many places) such that their overall payoff increases. Before we are able to introduce the 'one-shot' equilibrium concept, we will first introduce a modal operator that allows to specify properties that should hold everywhere in the game tree.

February 26, 2024 20:58 ws-rv9x6

Book Title main page 15

Infinite Horizon Extensive Form Games, Coalgebraically 3.3.1. The 'Everywhere' modality

Notions from game theory such as subgame perfection require a predicate to hold at every node of a tree (i.e., in every subgame). This is achieved by the so-called 'everywhere' or 'henceforth' modality. Using standard techniques from coalgebra, we can construct it using a proof-irrelevant predicate lifting as follows:

Definition 14. Let (X, γ) be an F ETree -coalgebra. Consider the predicate lifting φ □ : P(X) → P(F ETree X) defined by

φ □ (Q) = {inl * } ∪ {inr(q, n, f ) | (∀a ∈ [n]) f (a) ∈ Q}
and for a predicate P ∈ P(X), define □P to be the greatest fixpoint of

F □,P (U ) = P ∩ γ -1 (φ □ (U )).
A detailed discussion of this operator can be found e.g. in Jacobs ( 2016) where □ is referred to as the "henceforth" operator. Intuitively, given a predicate P , □P holds at a state x of a coalgebra if x itself and all its descendants satisfy P , i.e., P is invariably true in the game starting at x. The □-operator satisfies the properties one would expect from basic modal logic.

Lemma 15. The modality □ is monotone, i.e. if P implies Q then □P implies □Q. Furthermore □P ⊆ P and □P ⊆ □□P .

Proof. Assume P ⊆ Q. To show □P ⊆ □Q, we use the finality of □Q to conclude □P ⊆ □Q by showing that □P ⊆ F □,Q (□P ). This follows since □P ⊆ F □,P (□P ) and P ⊆ Q. In the same way, □P ⊆ P and □P ⊆ □□P .

Unimprovability

A very simple equilibrium concept is the following: at each node of the game, the current player cannot improve their payoff by changing their action at the current node. We call this the 'one-shot' equilibrium concept. Formally, we can encode it as follows. First we define a predicate Unimprov which verifies that, at a node in Z (X,γ) , the current strategy is unimprovable for the current player. We then ask that this predicate holds everywhere in the tree using the 'everywhere' modality. M. Capucci, N. Ghani, C. Kupke, J. Ledent, and F. Nordvall Forsberg Definition 16. We define the predicate Unimprov on Z (X,γ) by:

(x, σ, u) ∈ Unimprov if γ(x) = inl * or γ(x) = inr (q, n, f ) and now σ ∈ argmax(a → π q (u a (play (f a) (next σ a))))
The 'one-shot' equilibrium concept can now be defined as □Unimprov.

In words, (x, σ, u) ∈ Unimprov holds if x is a leaf, or if x is an internal node and now σ gives the best payoff for the current player q at the node according to the utility function u, assuming that all players continue to play according to σ. This equilibrium concept also occurs in [START_REF] Lescanne | Backward" coinduction, Nash equilibrium and the rationality of escalation[END_REF] and [START_REF] Abramsky | Coalgebraic analysis of subgame-perfect equilibria in infinite games without discounting[END_REF], who call it "subgame perfect equilibria". We prefer to reserve that name for the predicate □Nash that we will define in the next section.

Nash Equilibria and Subgame Perfection

The predicate Unimprov from the previous section says that a player cannot improve their payoff by changing their action at the current node only. In contrast, Nash equilibria are concerned with deviations where a player may change their action at several nodes simultaneously. The only restriction is that all such nodes must belong to the same player. So, we first define a predicate ≡ p which characterises when two strategy profiles are the same, except for deviations by one player p. Since we want to allow an infinite number of deviations by player p, we define this as a coinductive predicate.

Definition 17. For each player p ∈ P and state x ∈ X, we define a family of relations

≡ p ⊆ prof (X,γ) (x) × prof (X,γ) (x)
as the maximal family such that for all σ, σ ′ ∈ prof (X,γ) (x) and x ∈ X, we have σ ≡ p σ ′ if and only if one of the following is satisfied:

(1) γ(x) = inl * , or (2) γ(x) = inr (p, n, f ) and next σ a ≡ p next σ ′ a for all a ∈ [n], or (3) γ(x) = inr (q, n, f ) with q ̸ = p, now σ = now σ ′ and next σ a ≡ p next σ ′ a for all a ∈ [n].
We can use the universal property of ≡ p to deduce the following:

Lemma 18. Assume the set of players P has decidable equality. For each player p ∈ P , the relation ≡ p is reflexive.

February 26, 2024 20:58 ws-rv9x6 Book Title main page 17

Infinite Horizon Extensive Form Games, Coalgebraically

Using ≡ p to talk about deviations, we can now formulate the Nash equilibrium concept. Unlike the 'one-step' equilibrium, the definition of a Nash equlibrium relies on a global quantification over all possible alternative strategies of a player rather than a local quantification over transitions in the game coalgebra. Consequently, Nash is neither an inductive nor a coinductive predicate.

Definition 19. In the game coalgebra (Z (X,γ) , Γ) we define

(x, σ, u) ∈ Nash if ∀p ∈ P. ∀σ ′ ∈ prof (X,γ) (x). (σ ≡ p σ ′ ) → (π p u(play x σ) ≥ π p u(play x σ ′ ))
In other words, given an initial node x and payoff function u, the strategy profile σ is a Nash equilibrium if every possible deviation σ ′ by player p yields a payoff for p which is smaller than the one of σ.

We can now succinctly define the solution concept of subgame perfect Nash equilibria simply as □Nash -a strategy profile is subgame perfect if it is a Nash equilibrium in every subgame of the tree.

Relating Unimprovability and Subgame Perfect Nash Equilibria

In this section, we relate the coalgebraic subgame perfect Nash equilibria □Nash and the one-deviation equilibrium □Unimprov, thus connecting our coalgebraic treatment with the standard notions from game theory. One direction is almost immediate:

Lemma 20. Assume the set of players P has decidable equality. Let (x, σ, u) be a state of the game coalgebra (Z (X,γ) , Γ). If (x, σ, u) ∈ □Nash then (x, σ, u) ∈ □Unimprov.

Proof. Since □ is monotone by Lemma 15, it is sufficient to show that (x, σ, u) ∈ Nash implies (x, σ, u) ∈ Unimprov. If γ(x) = inl * , this is trivial, so we concentrate on the case when γ(x) = inr (q, n, f ). By definition, we have to show that

π q (u now σ (play (f (now σ)) (next σ (now σ)))) ≥ π q (u a (play (f a) (next σ a)))
for every a ∈ [n]. For each a, let σ a be the strategy profile with now σ a = a and next σ a = next σ. By Lemma 18, σ ≡ q σ a , and the conclusion follows from the assumption that (x, σ, u) ∈ Nash.

For the other direction, we need to assume that the utility function is suitably well behaved; this is known as continuity at infinity in the game theory literature (Fudenberg and Tirole, 1991, Chapter 4.2). We formulate it more generally for arbitrary F moves -coalgebras.

Continuity at infinity

To formally define continuity at infinity we assume that the set of payoffs R is a metric space and R P is the P -fold product of this metric space obtained via taking the maximum. To obtain a metric on a F moves -coalgebra we use the projections into the terminal sequence of F moves . This technique can be formulated for arbitrary functors on indexed families of sets.

Definition 21. Let H : Set X → Set X a functor, and (A, γ) an H-coalgebra. Recall that ⊤ X (x) = 1 is the terminal object in Set X . We define a family of natural transformations (γ i : A → H i (⊤ X )) i∈N inductively by:

A A ⊤ X HA H i+1 ⊤ X γ Hγ i γ i+1 γ 0
where γ 0 := ! A is the unique morphism from A into the terminal object. We call states a, a ′ ∈ A(x) n-step equivalent, and we write a ∼ n a ′ , when γ n x (a) = γ n x (a ′ ). This induces a pseudometric on A(x) by putting

d x (A,γ) (a, a ′ ) = 2 -m , where m = sup{n | a ∼ n a ′ }.
If H is finitary, i.e. determined by its action on finitely presentable objects [START_REF] Adamek | Locally Presentable and Accessible Categories[END_REF], then if two states in an H-coalgebra (A, γ) agree for all finite observations, they are equal. Hence in this case d x (A,γ) is actually a metric:

Lemma 22. Let H : Set X → Set X be a finitary functor. For each Hcoalgebra (A, γ) and x ∈ X, d x (A,γ) is a metric on A(x).

The lemma is a straightforward consequence of a similar result for Setfunctors [START_REF] Barr | Terminal coalgebras in well-founded set theory[END_REF][START_REF] Worrell | On coalgebras and final semantics[END_REF]. We apply the above lemma to the functor F moves : Set X → Set X from Definition 7, which is finitary. As a result, we are now ready to define continuity at infinity coalgebraically.

Definition 23. Let (X, γ) be an F ETree -coalgebra. We call u ∈ pay (X,γ) (x) continuous at infinity if u : moves (X,γ) (x) → R P is uniformly continuous as Infinite Horizon Extensive Form Games, Coalgebraically a map between metric spaces, i.e., if

∀ε > 0. ∃δ > 0. ∀m, m ′ . d x moves (X,γ) (m, m ′ ) < δ → d R P (u(m), (u m ′ )) < ε
Remark 24. This generalises the usual formulation of continuity at infinity from the game theory literature (see e.g. Fudenberg and Tirole (1991, Def. 4.1)) to coalgebras. We observe that the weaker assumption of pointwise continuity would be sufficient to prove Theorem 31 (or the corresponding traditional statement (Fudenberg and Tirole, 1991, Theorem 4.2)).

Classically, moves (X,γ) (x) is compact [START_REF] Kurz | Definability, canonical models, compactness for finitary coalgebraic modal logic[END_REF], and the distinction disappears, but this is of course not constructively valid.

Spelling out the definition of d x moves (X,γ) and d R P , we arrive at the following concrete definition of continuity at infinity: Proposition 25. Let (X, γ) be an F ETree -coalgebra. A payoff function u ∈ pay (X,γ) (x) is continuous at infinity if and only if By applying tan at both sides ¶ of d R ((u A m), (u A m ′ )) < ε, our thesis becomes

∀ε > 0. ∃n ∈ N. ∀m, m ′ . (m ∼ n m ′ ) → ∀p ∈ P. d R (π p (u m), π p (u m ′ )) < ε
∀ε > 0. ∃n ∈ N. ∀m, m ′ . m ∼ n m ′ → |(u A m) -(u A m ′ )| 1 + (u A m)(u A m ′ ) < tan ε. (1)
Observe that, when m, m ′ → +∞,

g((u A m), (u A m ′ )) -→ 0 where g(x, y) = |x -y| 1 + xy . §
We cannot use the traditional Euclidean metric on R = R since |-∞ -r| = +∞ for finite r ∈ R. Any well-defined metric that makes R into a bounded space is equivalent. ¶ The function tan, by virtue of being monotone on the domain (-π/2, +π/2), preserves inequalities for small enough ε (and, by previous considerations on the diameter of (R, d R ), for every value of d R ((u A m), (u A m ′ ))).

since (u A m), (u A m ′ ) → -∞ by the definition of u A and g(x, y) → 0 as x, y → -∞. This convergence gives an n ∈ N for each chosen tan ε > 0. Suppose now m ∼ n m ′ . In this particular example, this can happen if and only if either m, m ′ < n and m = m ′ , or m, m ′ ≥ n. In the first case, d R P ((u A m), (u A m ′ )) = 0 < tan ε. In the second case, we have chosen n to satisfy d R P ((u A m), (u A m ′ )) < tan ε. Thus we conclude that (1) is satisfied.

Example 27 (Repeated games (continues from Example 12)). The utility function of a repeated game with discounting is almost immediately seen to be continuous. Setting v = π p • (v T A) (using notation from Example 12), we see that we are tasked to prove:

∀ε > 0. ∃n ∈ N. ∀(m 0 , ms), (m ′ 0 , ms ′ ). (m 0 , ms ′ ) ∼ n (m ′ 0 , ms ′ ) → (v(m 0 ) -v(m ′ 0 )) + +∞ i=0 δ i+1 (v(ms i) -v(ms ′ i)) < ε
In this case, (m 0 , ms ′ ) ∼ n (m ′ 0 , ms ′ ) holds exactly when m 0 and m ′ 0 agree and (if n > 0) if ms and ms ′ also agree on their first n entries. When this happens, the first n + 1 terms of the series cancel out. By convergence of said series (easily obtainable by comparison with a geometric series), we can make that quantity as small as we need to by eliding enough leading terms.

The one-shot deviation principle

The one-shot equilibrium concept states that there is no profitable singlenode deviation. As an intermediate step towards subgame perfect Nash equilibria, we can also consider profitable deviations in a finite number of nodes. Following Lescanne (2013, §5), this concept can be formalised as an inductive definition as follows:

Definition 28. Let p ∈ P be a player, x ∈ X a state, and (X, γ) an F ETreecoalgebra. We define a family of relations ≡ fin p ⊆ prof (X,γ) (x) × prof (X,γ) (x) inductively as the least family such that for all σ, σ ′ ∈ prof (X,γ) (x) and x ∈ X we have σ ≡ fin p σ ′ iff one of the following is satisfied

(1) σ = σ ′ , or (2) γ(x) = inl * , or (3) γ(x) = inr p n f and next σ a ≡ fin p next σ ′ a for all a ∈ [n], or (
4) γ(x) = inr q n f with q ̸ = p, now σ = now σ ′ and next σ a ≡ fin p next σ ′ a for all a ∈ [n].

Thus strategies with σ ≡ fin p σ ′ can differ in their choice of action now σ ̸ = now σ ′ at p-nodes; since the definition is inductive, this can only happen a finite number of times before reaching a base case. Given two strategies σ and σ ′ , we can "truncate" σ after n rounds by replacing it with σ ′ , resulting in a new strategy ⌈σ⌉ σ ′ n .

Lemma 29. If σ ≡ p σ ′ , then σ ≡ fin p ⌈σ ′ ⌉ σ n for any n ∈ N. Conversely, if the set of players P has decidable equality, then σ ≡ fin p σ ′ implies σ ≡ p σ ′ .

Proof. The first statement follows by induction on n. Since ⌈σ ′ ⌉ σ 0 = σ, we have by σ ≡ fin p ⌈σ ′ ⌉ σ 0 by (1). For the step case, consider the form of the proof σ ≡ p σ ′ : if σ ≡ p σ ′ because γ(x) = inl * , we immediately have σ ≡ fin p ⌈σ ′ ⌉ σ n+1 ; otherwise p = q or p ̸ = q, and in either case next σ a ≡ p next σ ′ a for all a ∈ [m], hence by the induction hypothesis next σ a ≡ fin p ⌈next σ ′ a⌉ next σ a n for every a, and by either (3) or ( 4) and how ⌈σ⌉ σ ′ n is defined, we have σ ≡ fin p ⌈σ ′ ⌉ σ n+1 as required. The second statement follows easily by induction on the proof that σ ≡ fin p σ ′ , using decidable equality on P to invoke Lemma 20 for the base case (1).

Although allowing a finite number of deviations might seem like a stronger notion of equilibrium than allowing just one, they turn out to be equivalent. This is because the one-shot equilibrium concept is quantified on every subgame: assuming a player can improve their payoff with a finite number of deviations, we can find a single profitable deviation by restricting to the subgame starting at the last deviation. Recall that an order relation < is trichotomous if, for every pair of elements x, y, it is decidable whether x < y or or x = y or x > y.

Lemma 30. Let (x, σ, u) be a state of the game coalgebra (Z (X,γ) , Γ). Assume that the order relation < on R is trichotomous. If there is a player p and a strategy σ ′ such that σ ≡ fin p σ ′ and π p (u(play x σ ′ )) > π p (u(play x σ)) then (x, σ, u) ∈ ¬□Unimprov.

Proof. By induction on the proof that σ ≡ fin p σ ′ , we can find a strategy σ ′′ that differs from σ (and agrees with σ ′ ) a minimum number of times, whilst still being a profitable deviation. In addition, there is a deepest node where σ ′′ differs from σ; let σ ′′′ be the strategy that agrees with σ everywhere but at this node, where it agrees with σ ′ . By trichotomy, we either have π p (u(play x σ ′′′ )) > π p (u(play x σ)) or π p (u(play x σ ′′′ )) ≤ π p (u(play x σ)). If the former, then this contradicts Unimprov at this node as required, so we only need to show that the latter is impossible. This is so, because the latter case violates the assumption that σ ′′ is minimal.

Armed with this lemma, we can now tackle the difficult direction of the one-shot deviation principle, assuming the payoff function is continuous. For simplicity, we only state the theorem for R = Q with the standard metric d Q (x, y) = |x -y|. Note that the order on Q certainly is trichotomous.

Theorem 31. Assume the set of players P has decidable equality. Let (x, σ, u) be a state of the game coalgebra (Z (X,γ) , Γ) with rewards R = Q. If u is continuous at infinity and (x, σ, u) ∈ □Unimprov, then (x, σ, u) ∈ □Nash.

Proof. Since □P ⊆ □□P and □ is monotone by Lemma 15, it is sufficient to show that (x, σ, u) ∈ □Unimprov implies (x, σ, u) ∈ Nash. Hence, assume a player p and a strategy σ ′ with σ ≡ p σ ′ are given; by trichotomy of <, it is enough the show that u p (play x σ) < u p (play x σ ′ ) where we write u p (m) = π p (u(m)), is impossible. By continuity of u with ε = u p (play x σ ′ ) -u p (play x σ), we find n such that if m ∼ n play x σ ′ then |u p (play x σ ′ ) -u p (m)| < ε. Consider the history m = play x σ ′′ , where σ ′′ = ⌈σ ′ ⌉ σ n is σ ′ up to depth n, and σ thereafter. By construction, m ∼ n play x σ ′ . We claim that σ ′′ is still a strictly profitable deviation, i.e. u p (play x σ) < u p (play x σ ′′ ), by trichotomy of < again: if u p (play x σ) ≥ u p (play x σ ′′ ) then both |u p (play x σ ′ ) -u p (play x σ ′′ )| ≥ ε and |u p (play x σ ′ ) -u p (play x σ ′′ )| < ε, which is absurd. Hence we have found a profitable finite deviation, which by Lemmas 29 and 30 contradicts the assumption that (x, σ, u) ∈ □Unimprov. Therefore, we must instead have u p (play x σ) ≥ u p (play x σ ′ ) as required.

Conclusions and future work

In this paper, we have built on Lescanne's and Abramksy and Winschel's coalgebraic treatment of infinite extensive form games to also consider plays that go on forever, rather than just convergent strategies that eventually lead to a terminal node. We are thus able to treat games such as infinitely repeated games, in addition to the games previously considered. We also connected the coalgebraic and traditional notions of equilibria by proving them equal under the assumption that the payoff function is continuousa well-known result in the game theory literature, here extended to more general coalgebras. In future work, we plan to exploit techniques from coalgebra and automata theory to use our framework to solve various infinitehorizon games, i.e., to compute the set of equilibria for some given notion of equilibrium -Nash, sub game perfect equilibria, etc. We also hope to extend our recent translation of finite extensive form games into the framework of open games [START_REF] Capucci | Translating extensive form games to open games with agency[END_REF] to infinite games; since open games are well-suited for software implementation, this might point to another approach for computing the equilibria of infinite extensive form games in practice.

February

  fight

  fight→ * , forming the set 3. These are all accessible from A, therefore M ∞ has set of moves specified by the final coalgebra of X → 3 × X which is readily seen to be 3 N . Indeed, a move of the repeated game is a move for every stage game. On the other hand, only moves 2 and 3 are accessible from B, therefore we get

February

Example 26 (

 26 Dollar Auction (continues from Example 11)). We claim the payoff function for Dollar is continuous at infinity. It will suffice to focus on one component, say u A = π A • u, since π B • u is the same up to a shift. Let us begin by specifying a metric on R = [-∞, +∞): § d R (r, r ′ ) = | arctan r -arctan r ′ | This choice of metric makes R into a bounded space, since evidently diam(R) = π. In particular, d R ((u A m), (u A m ′ )) is finite for every m, m ′ ∈ moves (D,δ) (x).

Book Title main page 23

Acknowledgements We would like to thank Pierre Lescanne for discussions about coinduction and games, and Philipp Zahn about the one-step deviation principle. Thanks also to the anonymous reviewer, whose comments and suggestions helped improve the paper.


Jérémy Ledent

Brief Announcement: Variants of Approximate Agreement on Graphs and Simplicial Complexes

Keywords: CCS Concepts:, Theory of computation → Distributed algorithms distributed computing, approximate agreement, simplicial complex ACM Reference

Approximate agreement is a weaker version of consensus where two or more processes must agree on a real number within a distance 𝜀 of each other. Many variants of this task have been considered in the literature: continuous or discrete ones; multi-dimensional ones; as well as agreement on graphs and other spaces. We focus on two variants of approximate agreement on graphs, edge agreement and clique agreement. We show that both tasks arise as special cases of a more general, higher-dimensional, approximate agreement task, where the processes must agree on the vertices of a simplex in a given simplicial complex. This new point of view gives rise to a novel topological perspective on the solvability of clique agreement.

INTRODUCTION

Approximate agreement [START_REF] Dolev | Reaching approximate agreement in the presence of faults[END_REF] is a weaker variant of the consensus task, which is solvable in the wait-free read/write registers model. Many variants of approximate agreement have been considered, with a similar structure. Fix a finite number 𝑛 of processes (𝑃 𝑖 ) 𝑖 ∈ [𝑛] . Each process 𝑃 𝑖 starts the computation with an input value 𝑥 𝑖 ∈ V, where V is some set of values. At the end of the computation, each process decides on an output value 𝑦 𝑖 ∈ V, subject to some task-specific constraints, known as validity and agreement. Validity restricts the set of possible outputs depending on the set {𝑥 𝑖 | 𝑖 ∈ [𝑛]} of inputs values; and agreement says that the output values chosen by the processes should be "close from each other". Thus, the set V usually carries some additional structure (e.g. a metric space) in order to have a notion of "closeness" of the values 𝑦 𝑖 .

𝜀-Approximate agreement. Fix a real number 𝜀 > 0. The set of values is V = [0, 1], the set of real numbers between 0 and 1. The goal is to decide outputs 𝑦 𝑖 ∈ [0, 1] that are within distance 𝜀. This is formalized by two conditions, validity and agreement:

• Validity: for all 𝑖 ∈ [𝑛], min 𝑗 ∈ [𝑛] 𝑥 𝑗 ≤ 𝑦 𝑖 ≤ max 𝑗 ∈ [𝑛] 𝑥 𝑗 .
• Agreement: for all 𝑖, 𝑗 ∈ [𝑛], |𝑦 𝑖 -𝑦 𝑗 | ≤ 𝜀.

For the analysis of distributed algorithms, it is often easier to manipulate discrete data; so rather than working with the interval [0, 1], it is handy to use the following discrete reformulation.

Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses, contact the owner/author(s).

𝑁 -Approximate agreement. Fix some natural number 𝑁 ∈ N >0 , and take the set of values V = {0, 1, 2, . . . , 𝑁 }.

Processes start with input values 𝑥 𝑖 ∈ V and must decide outputs 𝑦 𝑖 ∈ V such that:

• Validity: for all 𝑖 ∈ [𝑛], min 𝑗 ∈ [𝑛] 𝑥 𝑗 ≤ 𝑦 𝑖 ≤ max 𝑗 ∈ [𝑛] 𝑥 𝑗 . • Agreement: for all 𝑖, 𝑗 ∈ [𝑛], |𝑦 𝑖 -𝑦 𝑗 | ≤ 1.
Thus, this is the same as the previous task for 𝜀 = 1 𝑁 , where the processes are restricted to choose values of the form 𝑘 𝑁 , 0 ≤ 𝑘 ≤ 𝑁 .

The 𝑁 -approximate agreement task can also be viewed as a special case of a graph agreement task. Let G be the graph with set of vertices V = {0, 1, 2, . . . , 𝑁 }, and edges of the form {𝑘, 𝑘 + 1} for each 0 ≤ 𝑘 < 𝑁 . The processes are given vertices of G as inputs, and must decide on a vertex of G so that the set of all outputs is an edge of G. There are actually several ways to generalize this task to a general graph G. In the two tasks below, we fix a finite graph G, and let the set of values V be the set of vertices of G.

Edge agreement. See e.g. [START_REF] Castañeda | Convergence and covering on graphs for wait-free robots[END_REF] and [START_REF] Alcantara | The topology of look-compute-move robot wait-free algorithms with hard termination[END_REF].

• Validity: if all input vertices are equal, then every process must output this vertex; if the input vertices span an edge, then every process must output a vertex of that edge.

• Agreement: the set of output values {𝑦 𝑖 | 𝑖 ∈ [𝑛]} is either a vertex or an edge of G.

Clique agreement. See e.g. [START_REF] Alcantara | The topology of look-compute-move robot wait-free algorithms with hard termination[END_REF], [START_REF] Nowak | Byzantine Approximate Agreement on Graphs[END_REF] and [START_REF] Alistarh | Wait-free approximate agreement on graphs[END_REF].

• Validity: if the set of inputs 𝑋 = {𝑥 𝑖 | 𝑖 ∈ [𝑛]} is a clique of G, then every output 𝑦 𝑖 must be in 𝑋 . • Agreement: the set of outputs {𝑦 𝑖 | 𝑖 ∈ [𝑛]} is a clique of G.
In the literature, edge agreement is known as graph convergence in [START_REF] Castañeda | Convergence and covering on graphs for wait-free robots[END_REF] and edge gathering in [START_REF] Alcantara | The topology of look-compute-move robot wait-free algorithms with hard termination[END_REF]. Clique agreement is called 1-gathering in [START_REF] Alcantara | The topology of look-compute-move robot wait-free algorithms with hard termination[END_REF], and variants of it (with a stronger validity condition) are monophonic approximate agreement in [START_REF] Nowak | Byzantine Approximate Agreement on Graphs[END_REF], and graphical approximate agreement in [START_REF] Alistarh | Wait-free approximate agreement on graphs[END_REF].

In the wait-free shared memory model, edge agreement is solvable for 𝑛 ≥ 3 processes if and only if the graph G is a tree [START_REF] Castañeda | Convergence and covering on graphs for wait-free robots[END_REF]. For clique agreement, a precise characterization of solvability is not known yet. In [START_REF] Nowak | Byzantine Approximate Agreement on Graphs[END_REF], an algorithm is given to solve clique agreement on chordal graphs for 𝑛 ≥ 3 processes; and in [START_REF] Alistarh | Wait-free approximate agreement on graphs[END_REF] on nicely bridged graphs. Clique agreement is unsolvable on large cycles [START_REF] Castañeda | Convergence and covering on graphs for wait-free robots[END_REF], and on graphs satisfying a so-called lower bound labelling condition [START_REF] Alistarh | Wait-free approximate agreement on graphs[END_REF].

Many other variants of approximate agreement have been studied. One of them is multi-dimensional approximate agreement [START_REF] Mendes | Multidimensional agreement in Byzantine systems[END_REF], where processes takes values in the 𝑚-dimensional Euclidean space V = R 𝑚 . As in the 1-dimensional case, processes must decide output values within a distance 𝜀 of each other. One could imagine similar tasks on various topological spaces (e.g. on a sphere or a torus), but most of them would be unsolvable. Indeed, Herlihy and Shavit [START_REF] Herlihy | The asynchronous computability theorem for t-resilient tasks[END_REF] have shown that in the case where the space V ⊆ R 𝑚 may contain holes, the corresponding approximate agreement task is not wait-free solvable.

Other notable examples of approximate agreement tasks include barycentric agreement [START_REF] Herlihy | Distributed Computing Through Combinatorial Topology[END_REF], which is a discrete counterpart of multi-dimensional agreement; rendezvous tasks [START_REF] Liu | Classifying rendezvous tasks of arbitrary dimension[END_REF], loop agreement [START_REF] Herlihy | The Decidability of Distributed Decision Tasks (Extended Abstract)[END_REF]; and more generally abstract approximate agreement [START_REF] Nowak | Byzantine Approximate Agreement on Graphs[END_REF] where V is an abstract convexity space.

Distributed computing model. Most of this paper is concerned with comparing task specifications, which is independent from the model used to solve the task. When we mention solvability, it will usually be in the wait-free shared memory model.

Contributions. Consider the simplex agreement task, which is a mild generalization of barycentric agreement1 . Fix a simplicial complex K, and let V be the vertices of K. Processes are given input values 𝑥 𝑖 ∈ V and must decide outputs 𝑦 𝑖 ∈ V such that:

• Validity: if the set of input values 𝑋 = {𝑥 𝑖 | 𝑖 ∈ [𝑛]
} is a simplex of K then every output 𝑦 𝑖 must be in 𝑋 .

• Agreement: the set of outputs values {𝑦 𝑖 | 𝑖 ∈ [𝑛]} must be a simplex of K.

We show that both edge agreement and clique agreement arise as special cases of this simplex agreement task.

In particular, clique agreement on a graph G is equivalent to simplex agreement on the complex of cliques of G, that we denote by 𝜅 (G). Thus, we argue that, despite being formulated on a graph, clique agreement is in fact of a multi-dimensional nature. More precisely, the dimension of the associated simplicial complex 𝜅 (G) is related to the clique number 𝜔 (G) of the graph by the formula: dim(𝜅

(G)) + 1 = 𝜔 (G).
This topological point of view sheds a new light on the solvability of clique agreement. Indeed, the chordality of a graph is known to be related to the contractibility of its complex of cliques [START_REF] Adiprasito | Higher chordality: From graphs to complexes[END_REF]. Thus, we conjecture that clique agreement is solvable on a graph G precisely when 𝜅 (G) is contractible. This would connect nicely with the continuous case, where multi-dimensional 𝜀-agreement in a subset V ⊆ R 𝑚 is known to be unsolvable if V contains a hole of radius larger than 𝜀 [START_REF] Herlihy | The asynchronous computability theorem for t-resilient tasks[END_REF].

Plan. In Section 2, we recall some basic definitions on graphs and simplicial complexes, and state the relationship between a graph and its complex of cliques as an adjunction between categories. Then in Section 3, we show that both edge and clique agreement are particular instances of the simplex agreement task. We highlight the relevance of this fact by looking at known results on graph agreement tasks through the lens of topology.

ADJUNCTIONS BETWEEN GRAPHS AND SIMPLICIAL COMPLEXES

We quickly recall the standard definitions of graphs and simplicial complexes. Note that our graphs are non-directed and simple, i.e., without self-loops or parallel edges. The main purpose of this section is to explain how every graph G can be turned into a simplicial complex 𝜅 (G), called the complex of cliques. This complex 𝜅 (G) is canonical, in the sense of Proposition 1. We use the language of category theory to formally study 𝜅, but a reader unfamiliar with those notions should not worry: understanding the definition of 𝜅 (G) is sufficient to follow the rest of the paper. Definition 1 (Simplicial complex). A simplicial complex is a pair K = (𝑉 , 𝑆), where 𝑉 is a finite set of vertices, and 𝑆 ⊆ P (𝑉 ) is a set of non-empty subsets of 𝑉 called simplices, such that:

• for every 𝑣 ∈ 𝑉 , {𝑣 } ∈ 𝑆, and

• 𝑆 is downward-closed, i.e., for every 𝑌 ∈ 𝑆 and for every non-empty subset 𝑋 ⊆ 𝑌 , 𝑋 ∈ 𝑆.

The dimension of a simplex 𝑋 ∈ 𝑆 is defined by dim(𝑋 ) = card(𝑋 ) -1. We often identify a vertex 𝑣 ∈ 𝑉 with the 0-dimensional simplex {𝑣 } ∈ 𝑆. Simplexes of dimension 1 are called edges, and simplices of dimension 2 are triangles. The dimension of a simplicial complex K is the maximal dimension of a simplex of K:

dim(K) = max{dim(𝑋 ) | 𝑋 ∈ 𝑆 }.
Definition 2 (Graph). A (non-directed, simple) graph G is a simplicial complex of dimension 1. Such a graph is uniquely determined by its set 𝑉 of vertices and its set 𝐸 of edges, so we write G = (𝑉 , 𝐸).

We assume the reader is familiar with the notions of "cycle" and "induced subgraph". A graph is chordal when it has no induced cycle of length ≥ 4. A clique of G is a set of vertices 𝑋 ⊆ 𝑉 such that for every 𝑢, 𝑣 ∈ 𝑋 , {𝑢, 𝑣 } ∈ 𝐸 is an edge of G. The clique-number of G, written 𝜔 (G), is the maximum number of vertices in a clique.

We denote by SimCpx the category of simplicial complexes (and simplicial maps), and Graph the category of graphs (and graph homomorphisms). Since we defined graphs as a special case of simplicial complexes, there is an inclusion functor 𝜄 : Graph → SimCpx. Conversely, there is a functor skel 1 : SimCpx → Graph that can turn every simplicial complex into a graph (called its 1-skeleton) by forgetting about the higher-dimensional simplices. Formally, for a simplicial complex K = (𝑉 , 𝑆), its 1-skeleton is the graph skel 1 (K) = (𝑉 , 𝐸) where 𝐸 = {𝑋 ∈ 𝑆 | dim(𝑋 ) = 1}. Finally, we define a third functor 𝜅 : Graph → SimCpx that associates with each graph G = (𝑉 , 𝐸) its complex of cliques,

defined by 𝜅 (G) = (𝑉 , 𝑆) where 𝑆 = {𝑋 ⊆ 𝑉 | 𝑋 is a clique of G}. Graph SimCpx SimCpx skel 1 skel 1

𝜄 𝜅

The relationship between these three functors is nicely summed up in the following (folklore) proposition.

Proposition 1. The functor 𝜄 is left adjoint to the 1-skeleton functor, and 𝜅 is its right adjoint: 𝜄 ⊣ skel 1 ⊣ 𝜅.

Finally, we mention the following topological characterization of chordal graphs in terms of contractibility.

Theorem 1 ([1]).

A graph G is chordal if and only if for every induced subgraph H of G, the complex of cliques 𝜅 (H ) is contractible.

Note that it is not true that a graph G is chordal if and only if 𝜅 (G) is contractible: the counter-example below depicts a non-chordal graph (left) whose clique complex (right) is contractible, since it is homeomorphic to a 2-dimensional disc.

𝜅

GRAPH AGREEMENT TASKS AND SIMPLEX AGREEMENT

We can now relate the three tasks defined in the introduction: edge agreement, clique agreement, and simplex agreement.

In the statement below, when we say that two tasks are the same, we mean that they have the same set of values V, and that their validity and agreement requirements are (respectively) equivalent. Theorem 2. Let G = (𝑉 , 𝐸) be a graph. Then:

(1) Edge agreement on the graph G is the same task as simplex agreement on the simplicial complex 𝜄 (G).

(2) Clique agreement on G is the same task as simplex agreement on its simplicial complex of cliques, 𝜅 (G).

Proof. By definition, both 𝜄 (G) and 𝜅 (G) have the same set of vertices 𝑉 as the graph G, therefore all four tasks use the same set of values V = 𝑉 . To prove (2), notice that a simplex of 𝜅 (G) is by definition a clique of G, so both validity and agreement conditions are the same. For (1), remark that a simplex of 𝜄 (G) can be either a vertex or an edge of G. Once again, this observation makes the two validity and agreement conditions equivalent. □

The purpose of Theorem 2 is to offer a new point of view on these two graph agreement tasks. While edge agreement is truly a graph task (because the complex 𝜄 (G) is 1-dimensional), we argue that clique agreement is better understood when we look at the complex of cliques of the graph G, to expose its topological nature. As an example, consider the following result of [START_REF] Nowak | Byzantine Approximate Agreement on Graphs[END_REF] A more recent paper [START_REF] Alistarh | Wait-free approximate agreement on graphs[END_REF] improved the solvability result of [START_REF] Nowak | Byzantine Approximate Agreement on Graphs[END_REF], in the wait-free model, to also work on some non-chordal graphs such as the hexagonal one depicted at the end of Section 2. They also proved an impossibility result: clique agreement is not wait-free solvable when the graph G satisfies a so-called lower bound labelling condition.

This mysterious condition can be understood topologically: it implies that the complex of cliques 𝜅 (G) is not simply connected. In fact, we conjecture that it is equivalent.

This topological point of view allows us to make the following conjecture, by analogy with the continuous case, where Herlihy and Shavit proved that 𝜀-approximate agreement is impossible whenever the space V ⊆ R 𝑚 contains holes of radius ≥ 𝜀 [START_REF] Herlihy | The asynchronous computability theorem for t-resilient tasks[END_REF].

Conjecture. Simplex agreement on a simplicial complex K is wait-free solvable if and only if K is contractible.

Methods based on algebraic topology are well established in distributed computing to prove impossibility results [START_REF] Herlihy | Distributed Computing Through Combinatorial Topology[END_REF].

In particular, the "only if" direction of the conjecture seems like it could be a direct consequence of the topological characterization of solvability for colorless tasks (also called convergence tasks in [START_REF] Borowsky | The BG distributed simulation algorithm[END_REF]), of which simplex agreement is an example.

For graphs, the conjecture implies that clique agreement on a graph G is solvable if and only if its complex of cliques 𝜅 (G) is contractible. This is consistent with the solvability result of [START_REF] Nowak | Byzantine Approximate Agreement on Graphs[END_REF], since chordal graphs have a contractible complex of cliques by Theorem 1. Our conjecture is also consistent with the impossibility result of [START_REF] Alistarh | Wait-free approximate agreement on graphs[END_REF], because graphs that admit a lower bound labelling have a non-simply connected complex of cliques (hence, non-contractible).

One case whose wait-free solvability is still unsettled is when the graph G is a triangulated sphere. For instance, take G to be the graph of edges of an icosahedron. Our conjecture says that, since the associated simplicial complex is not contractible, clique agreement on G should be unsolvable in the wait-free model.

CONCLUSION

We have shown that edge agreement and clique agreement both arise as particular cases of the simplex agreement task.

While edge agreement is truly of a graph-theoretic nature, clique agreement appears to be better understood through the lens of simplicial complexes. With this new point of view, one can replace the graph-theoretic notions of "clique number" and "chordality" by the topological ones of "dimension" and "contractibility". With this in mind, parallels can be drawn with various results on multi-dimensional approximate agreement, which gives a better understanding on the wait-free solvability of graph agreement tasks.

  about solving clique agreement for 𝑛 processes on a connected chordal graph G, in a message-passing model with Byzantine faults: Theorem 3 ([START_REF] Nowak | Byzantine Approximate Agreement on Graphs[END_REF]). For a chordal graph G, clique agreement is solvable with 𝑓 Byzantine faults if 𝑛 > (𝜔 (G) + 1)𝑓 . Now, observe that the simplicial complex 𝜅 (G) is of dimension 𝜔 (G) -1, where 𝜔 (G) denotes the clique number of G. Thus, the above result can be compared with the one of Mendes et al.[START_REF] Mendes | Multidimensional agreement in Byzantine systems[END_REF] for multidimensional agreement, which says that approximate agreement in R 𝑚 can be reached among 𝑛 processes with 𝑓 Byzantine faults if and only if 𝑛 > (𝑚 + 2)𝑓 . Hence, it appears that clique agreement behaves much like a discrete counterpart of the 𝑚-dimensional approximate agreement task, for 𝑚 = dim(𝜅 (G)).

Barycentric agreement is recovered when the simplicial complex K is chosen to be the iterated barycentric subdivision of a standard 𝑛-simplex.

All the tasks that we considered have a very permissive validity condition, where any output is allowed unless the input vertices already form a clique. By contrast, [12] and [3] have stronger validity conditions, requiring every output vertex to lie on a chordless or shortest path between the inputs. It would be insightful to study these conditions topologically, for example, to see whether they relate to notions of convex hull on manifolds.

ACKNOWLEDGMENTS

The author would like to thank Éric Goubault and Sergio Rajsbaum for helpful discussions on this topic.