# Infinite Horizon Extensive Form Games, Coalgebraically

Matteo Capucci, Neil Ghani, Clemens Kupke, Jérémy Ledent, Fredrik

Nordvall Forsberg

<figure><img src="image_1.png" /></figure>

## ► To cite this version:

Matteo Capucci, Neil Ghani, Clemens Kupke, Jérémy Ledent, Fredrik Nordvall Forsberg. Infinite Horizon Extensive Form Games, Coalgebraically. Mathematics for Computation, 2022, pp.195-222. 10.1142/9789811245220_0008. hal-04470718

HAL Id: hal-04470718

https://hal.science/hal-04470718v1

Submitted on 26 Feb 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>
# Chapter 1

## Infinite Horizon Extensive Form Games, Coalgebraically

Matteo Capucci, Neil Ghani, Clemens Kupke,

Jérémy Ledent, and Fredrik Nordvall Forsberg

*Mathematically Structured Programming group,*
*Department of Computer and Information Sciences,*

*University of Strathclyde*

### 1. Introduction

Game theory is the study of how agents make decisions in order to maximise their outcomes (Osbourne and Rubinstein, 1994; Leyton-Brown and Shoham, 2008). 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 (Bridges, 1982, 1989, 1994, 2004), 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 (Mycielski and Taylor, 1976). 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 (Rutten, 2000).

We are not the first to attack infinite extensive form games using coal-
gebraic methods. Lescanne (2013, 2018), Lescanne and Perrinel (2012)
and Abramsky and Winschel (2017) define infinite two-player games coal-
gebraically, and show that coinductive proof methods can be used to con-
structively 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 infi-
nite history of the game. Building on our on work on infinitely repeated
open games (Ghani et al., 2018), 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, Abramsky and Winschel (2017) 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 Abramsky and Winschel (2017),
it applies to games where infinite plays are possible; and it relates to the
more standard definition of subgame-perfect Nash equilibrium, □Nash. Ad-
ditionally, our theorem applies to any coalgebra of the extensive-form tree
functor, whereas Abramsky and Winschel only work with the final coalge-
bra. Compared to the usual proofs found in the game theory literature, we
carefully analyse the constructivity of the proof. The only extra assump-
tion 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 endofunc-
tors 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 coal-
gebraic 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 $\mathcal{P}: \mathbf{Set} \to \mathbf{Set}$ for the covariant powerset functor mapping a set to its set of subsets. Given a set-indexed collection of sets $Y: I \to \mathbf{Set}$ and $i \in I$, we write interchangeably $Y_i$ or $Y(i)$ for the $i$th component of the collection. The dependent sum $\sum_{i \in I} Y_i$ is the disjoint union of all of the sets $Y_i$ in the collection, with elements pairs $(i, y)$ where $i \in I$ and $y \in Y_i$, while the dependent function space $\prod_{i \in I} Y_i$ is the set of functions mapping an input $i \in I$ to an element of $Y_i$. We write $A + B$ for the disjoint union of two sets $A$ and $B$, with injections $\text{inl}: A \to A + B$ and $\text{inr}: B \to A + B$. We denote the set of natural numbers by $\mathbb{N}$, the set of positive natural numbers by $\mathbb{N}^+$, and write $[n] = \{0, \dots, n-1\}$ for a canonical $n$-element set. We also write $\mathbf{1} = [1]$, $\mathbf{2} = [2]$ and so on for fixed small finite sets.

## 2. Coalgebraic Preliminaries

We assume familiarity with basic category theory.

2.1. *Final coalgebras*

Let $\mathcal{C}$ be a category and $F: \mathcal{C} \to \mathcal{C}$ an endofunctor. An $F$-coalgebra is a pair $(A, \alpha)$, where $A$ is an object of $\mathcal{C}$, and $\alpha: A \to FA$ is a morphism. An $F$-coalgebra homomorphism from $(A, \alpha)$ to $(B, \beta)$ is a morphism $f: A \to B$
preserving the coalgebra structure, i.e. such that the following diagram commutes:

<figure><img src="image_3.png" /></figure>

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 $(\nu F, \text{out})$. Its universal property is a *corecursion* or *coinduction principle*: for every F-coalgebra $(A, \alpha)$, there exists a unique coalgebra homomorphism $\text{unfold} : (A, \alpha) \to (\nu F, \text{out})$. We will make use of Lambek's Lemma, which says that for a final coalgebra $(\nu F, \text{out})$, the map $\text{out} : \nu F \to F(\nu F)$ is an isomorphism.

## 2.2. Coinductive families and predicates

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

A *coinductive family* indexed by $I$ is the final coalgebra $\nu G$ of an endo-functor $G$ on $\text{Set}^I$. Its corresponding “coinduction principle” says that for every $G$-coalgebra $(P, g)$, there exists a unique morphism $\text{unfold} : P \to \nu G$ making the following diagram in $\text{Set}^I$ commute:

<figure><img src="image_4.png" /></figure>

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 \to G(P)_i$, then there is a unique family of morphisms $\text{unfold}_i : P_i \to \nu 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, \gamma)$ of a functor $F : \text{Set} \to \text{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 : \text{Set} \to \text{Set}$ is a natural transformation $\{\varphi_X : \text{Set}^X \to \text{Set}^{FX}\}_{X \in \text{Set}}$. Given an F-coalgebra $(X, \gamma :$
$X \to FX$) and a predicate lifting $\varphi$ of $F$, we can define an endofunctor on $\mathbf{Set}^X$ by

$$ \mathbf{Set}^X \xrightarrow{\varphi_X} \mathbf{Set}^{FX} \xrightarrow{-\circ\gamma} \mathbf{Set}^X $$

and consider its final coalgebra. Similarly, in Section 3.3, we also use proof-irrelevant predicate liftings $\{\varphi_X : \mathcal{P}(X) \to \mathcal{P}(FX)\}_{X \in \mathbf{Set}}$.

### 3. Infinite Extensive Form Games

In the game theory literature (Kuhn, 1953; Selten, 1975; Leyton-Brown and Shoham, 2008), 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 $\mathbf{ETree}^\infty$ of infinite extensive form game trees with players $P$ is the final coalgebra $(\mathbf{ETree}^\infty, \mathbf{out}_{\mathbf{ETree}^\infty})$ of the functor $F_{\mathbf{ETree}} : \mathbf{Set} \to \mathbf{Set}$ defined by

$$ F_{\mathbf{ETree}}(X) = \mathbf{1} + P \times \sum_{n \in \mathbb{N}^+} X^n. $$

This supports the Haskell-like data type

$$ \text{data } \mathbf{ETree}^\infty = \text{Leaf} \mid \text{Node } P(n: \mathbb{N}^+) ([n] \to \mathbf{ETree}^\infty) $$
Concretely a tree $T \in \mathbb{E}\mathit{Tree}^{\infty}$ is either a leaf, indicating no further plays are possible, or an internal node labeled with a player $p \in P$ who is to play at that point in the game, and an *arity* $n \in \mathbb{N}^{+}$ representing the number of different moves available, followed by $n$ subtrees. Crucially, being a final coalgebra, $\mathbb{E}\mathit{Tree}^{\infty}$ includes paths of infinite depth.

**Example 2 (Dollar Auction).** The Dollar auction is an infinite game introduced by Shubik (1971) 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.

<figure><img src="image_5.png" /></figure>

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:

$$ \text{Dollar}_A = \text{Node A 2 (Leaf, Dollar}_B) $$

$$ \text{Dollar}_B = \text{Node B 2 (Leaf, Dollar}_A) $$

Then Dollar := Dollar$_A$, as $A$ moves first. As an $F_{\mathbb{E}\mathit{Tree}}$-coalgebra, Dollar is defined starting from the coalgebra $(D, \delta)$, where $D = \{\text{turn}_A, \text{turn}_B, \text{end}\}$, $P = \{A, B\}$ and $\delta$ is defined by:

$$ \delta : D \to \mathbf{1} + P \times \sum_{n \in \mathbb{N}^{+}} D^{n} $$

$$ \delta \text{ turn}_A = \text{inr}(A, 2, (\text{end}, \text{turn}_B)) $$

$$ \delta \text{ turn}_B = \text{inr}(B, 2, (\text{end}, \text{turn}_A)) $$

$$ \delta \text{ end} = \text{inl} * $$

The coalgebra $(D, \delta)$ can be represented by the automaton below, where the two elements of **2** are named quit and bid:
<figure><img src="image_6.png" /></figure>

By terminality of $(ETree^\infty, \text{out}_{ETree}^\infty)$, there is a unique map $\text{unfold}_{(D,\delta)}$: $(D, \delta) \to (ETree^\infty, \text{out}_{ETree}^\infty)$, and we define Dollar := $\text{unfold}_{(D,\delta)}(\text{turn}_A)$. Thus, Dollar is the following infinite tree:

<figure><img src="image_7.png" /></figure>

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_{ETree}$-coalgebra ($\text{Rep}_T$, $\rho_T$): the *repeated game coalgebra*.

<figure><img src="image_8.png" /></figure>

By terminality of $(ETree^\infty, \text{out}_{ETree}^\infty)$, there is a unique map
$\mathit{unfold}_{(\mathit{Rep}_T, \rho_T)} : (\mathit{Rep}_T, \rho_T) \to (\mathit{ETree}^\infty, \mathit{out}_{\mathit{ETree}^\infty})$, and we define

$$T^\infty := \mathit{unfold}_{(\mathit{Rep}_T, \rho_T)}(\mathit{root}).$$

One concrete example is the Market Entry game (Selten, 1978), a game with players $P = \{A, B\}$ described by the extensive-form tree $M$ (here with payoff-labeled leaves):

$$ \begin{array}{ccc} A & \xrightarrow{\text{in}} & B \xrightarrow{\text{accom}} (2, 2) \\ \downarrow\text{out} & & \downarrow\text{fight} \\ (1, 5) & & (0, 0) \end{array} $$

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 $(\mathit{Rep}_T, \rho_T)$ corresponds to the automaton:

<figure><img src="image_9.png" /></figure>

The induced infinite tree $M^\infty$ is then given by

$$ \begin{array}{ccc} A & \xrightarrow{\text{in}} & B \xrightarrow{\text{accom}} A \xrightarrow{\text{in}} B \xrightarrow{\text{accom}} \dots \\ \downarrow\text{out} & & \downarrow\text{fight} & & \downarrow\text{fight} \\ A \xrightarrow{\text{in}} \dots & A \xrightarrow{\text{in}} \dots & A \xrightarrow{\text{in}} \dots & A \xrightarrow{\text{in}} \dots \\ \downarrow\text{out} & & \downarrow\text{out} & & \downarrow\text{out} \\ \vdots & \vdots & \vdots & \vdots & \vdots \end{array} $$

### 3.1. Strategies and moves

Throughout the section, let $(X, \gamma)$ be an $F_{\mathit{ETree}}$-coalgebra.

#### 3.1.1. Strategy profiles

A strategy profile for the coalgebra $(X, \gamma)$ at state $x \in X$ consists of a choice of an action at each node in the game tree induced by $(X, \gamma)$. Recall that an element of $F_{\mathit{ETree}}(X)$ is either a leaf (of the form $\text{inl}*$) or an internal node of the form $\text{inr}(q, n, f)$, where $q$ is a player, $n \in \mathbb{N}^+$, and $f : [n] \to X$.
**Definition 4.** We define the family of strategy profiles $\text{prof}_{(X,\gamma)}: X \to \text{Set}$ as the final coalgebra associated with the predicate lifting

$$ \varphi_{\text{prof},X}: (X \to \text{Set}) \to F_{\text{ETree}}(X) \to \text{Set} $$

$$ \varphi_{\text{prof},X} P (\text{inl} *) = \mathbf{1} $$

$$ \varphi_{\text{prof},X} P (\text{inr}(q, n, f)) = [n] \times \prod_{a \in [n]} P_{f(a)} $$

i.e. we define $\text{prof}_{(X,\gamma)}$ as the final coalgebra of the functor $F_{\text{Prof}}: \text{Set}^X \to \text{Set}^X$ defined by $F_{\text{Prof}}(P) = \varphi_{\text{prof},X}(P) \circ \gamma$.

That $\text{prof}_{(X,\gamma)}$ is the final coalgebra implies that for every $x \in X$, there is an isomorphism $s_x: \text{prof}_{(X,\gamma)}(x) \to \varphi_{\text{prof},X}(\text{prof}_{(X,\gamma)}(\gamma(x)))$. If $\gamma(x) = \text{inr}(q, n, f)$, we thus have

$$ s_x(\sigma) \in [n] \times \prod_{a \in [n]} \text{prof}_{(X,\gamma)}(f a) $$

and we write $s_x(\sigma) = (\text{now } \sigma, \text{next } \sigma)$. Intuitively, now $\sigma \in [n]$ is the branch chosen by player $q$ in the current node $x$ of the game tree; and next $\sigma$ is a function assigning, for every branch $a \in [n]$ — not only the one chosen by player $q$ — a strategy profile next $\sigma$ $a \in \text{prof}_{(X,\gamma)}(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 \cong \{\text{bid, quit}\}$.

Formally, we check that $\text{prof}_{(D,\delta)}: D \to \text{Set}$ is the following family of sets, where $(D, \delta)$ is the coalgebra that defines the Dollar game in Example 2.

$$ \text{prof}_{(D,\delta)}(x) \cong \begin{cases} \mathbf{1} & \text{if } x = \text{end} \\ \mathbf{2}^N & \text{if } x = \text{turn}_A, \text{turn}_B \end{cases} $$

Indeed, a function $\sigma \in 2^N$ contains exactly the data of a strategy profile in $\text{prof}_{(D,\delta)}(\text{turn}_A)$, since we can define

$$ \text{now } \sigma = \sigma(0) \in \mathbf{2} $$

$$ \text{next } \sigma \text{ quit} = * \in \mathbf{1} \cong \text{prof}_{(D,\delta)}(\text{end}) $$

$$ \text{next } \sigma \text{ bid} = (n \mapsto \sigma(n+1)) \in 2^N \cong \text{prof}_{(D,\delta)}(\text{turn}_B) $$

and similarly for a profile $\sigma \in \text{prof}_{(D,\delta)}(\text{turn}_B)$. It is straightforward (but cumbersome) to check that this satisfies the universal property of the final coalgebra of $F_{\text{Prof}}$.
10 M. Capucci, N. Ghani, C. Kupke, J. Ledent, and F. Nordvall Forsberg

**Example 6** (Repeated games (continues from Example 3)). For a finite game $T$, we have defined in Example 3 its repeated game coalgebra $(\mathrm{Rep}_T, \rho_T)$, whose unfolding is the infinitely repeated game $T^\infty$. A strategy profile for $(\mathrm{Rep}_T, \rho_T)$ with initial state $x$ is the greatest solution to

$$ \mathrm{prof}_{(\mathrm{Rep}_T, \rho_T)}(x) \cong \{\text{strategy profiles of } T|_x\} \times \prod_{\ell \in \text{leaves } x} \mathrm{prof}_{(\mathrm{Rep}_T, \rho_T)}(\text{root}) $$

where $T|_x$ is the subtree of $T$ starting at $x \in \mathrm{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 $\mathrm{prof}_M = \mathrm{prof}_{(\mathrm{Rep}_M, \rho_M)}$ to ease notation):

$$ \mathrm{prof}_M(A) \cong \{\text{in, out}\} \times \{\text{fight, accom}\} \times \underbrace{\mathrm{prof}_M(A) \times \mathrm{prof}_M(A) \times \mathrm{prof}_M(A)}_{3 \text{ leaves accessible from } A} $$

$$ \mathrm{prof}_M(B) \cong \{\text{fight, accom}\} \times \underbrace{\mathrm{prof}_M(A) \times \mathrm{prof}_M(A)}_{2 \text{ leaves accessible from } B} $$

Therefore $\mathrm{prof}_M(A)$ is the final coalgebra of the functor

$$ X \mapsto \{\text{in, out}\} \times \{\text{fight, accom}\} \times 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 : $X \to \mathrm{Set}$ as the final coalgebra associated with the predicate lifting

$$ \varphi_{\mathrm{moves},X} : (X \to \mathrm{Set}) \to F_{\mathrm{ETree}}(X) \to \mathrm{Set} $$

$$ \varphi_{\mathrm{moves},X} P (\mathrm{inl} | *) = \mathbf{1} $$

$$ \varphi_{\mathrm{moves},X} P (\mathrm{inr}(q, n, f)) = \sum_{a \in [n]} P_{f(a)} $$

i.e. we define $\mathrm{moves}_{(X,\gamma)}$ as the final coalgebra of the functor $F_{\mathrm{moves}} : \mathrm{Set}^X \to \mathrm{Set}^X$ defined by $F_{\mathrm{moves}}(P) = \varphi_{\mathrm{moves},X}(P) \circ \gamma$.

Again, for every $x \in X$, we have an isomorphism $m_x : \mathrm{moves}_{(X,\gamma)}(x) \to \varphi_{\mathrm{moves},X}(\mathrm{moves}_{(X,\gamma)})(\gamma(x))$. If $\gamma(x) = \mathrm{inr}(q, n, f)$, we have

$$ m_x(\pi) \in \sum_{a \in [n]} \mathrm{moves}_{(X,\gamma)}(f a) $$
Note that, as $m_x$ is iso, if $\gamma(x) = \text{inr}(q, n, f)$ then for each $a \in [n]$ and $\pi' \in \text{moves}_{(X,\gamma)}(fa)$ there is a unique element $\text{cons}(a, \pi') \in \text{moves}_{(X,\gamma)}(x)$ such that $m_x(\text{cons}(a, \pi')) = (a, \pi')$. Intuitively, $\text{cons}(a, \pi')$ represents a path in the game tree starting at node $x$, where the first chosen branch is $a \in [n]$, and the following branches are chosen according to the path $\pi'$.

**Example 8** (Dollar Auction (continues from Example 5)). The moves of Dollar are given by the final coalgebra of $X \mapsto 1 + X$, i.e.

$$ \text{moves}(\text{Dollar}) \cong \mathbf{1} + \text{moves}(\text{Dollar}) $$

The final coalgebra of this functor is known as the *conatural numbers* ($\mathbb{N}^{\infty}$, pred), which include all finite natural numbers and an 'infinite' number $\omega$. The map pred sends $0 \in \mathbb{N}^{\infty}$ to inl * and every other natural number to the right injection of its predecessor. The predecessor of $\omega$ is itself, pred $\omega = \text{inr} \omega$. 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 \ge n$ for any finite natural number $n$.

We interpret $n \in \text{moves}(\text{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 $\omega$ corresponds to infinite escalation, with players never quitting.

Similarly, $\text{moves}_{(D,\delta)}$ is given by

$$ \text{moves}_{(D,\delta)}(x) \cong \begin{cases} \mathbf{1} & \text{if } x = \text{end} \\ \mathbb{N}^{\infty} & \text{if } x = \text{turn}_A, \text{turn}_B \end{cases} $$

**Example 9** (Repeated games (continues from Example 6)). For any finite extensive-form game tree $T$, one has

$$ \text{moves}_{(\text{Rep}_T, \rho_T)}(x) \cong (\text{leaves } x) \times (\text{leaves root})^{\mathbb{N}}. $$

In the specific instance of the market entry game $M$, moves are three: 1: $A \xrightarrow{\text{out}} *$, 2: $A \xrightarrow{\text{in}} B \xrightarrow{\text{accom}} *$ and 3: $A \xrightarrow{\text{in}} B \xrightarrow{\text{fight}} *$, forming the set **3**. These are all accessible from $A$, therefore $M^{\infty}$ has set of moves specified by the final coalgebra of

$$ X \mapsto \mathbf{3} \times X $$

which is readily seen to be $\mathbf{3}^{\mathbb{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

$$ \text{moves}_{(\text{Rep}_M, \rho_M)}(x) \cong \begin{cases} \mathbf{3} \times \mathbf{3}^{\mathbb{N}} & \text{if } x = A \\ \mathbf{2} \times \mathbf{3}^{\mathbb{N}} & \text{if } x = B \end{cases} $$

<footnote>*The player who quits can be determined from the parity of $n$.</footnote>
## 3.2. 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.

### 3.2.1. The Play Function

We can use the universal property of final coalgebras to define a play function $\text{play}_{(X,\gamma)} : \text{prof}_{(X,\gamma)} \to \text{moves}_{(X,\gamma)}$ which computes the sequence of moves generated by playing according to a strategy profile.

To define $\text{play}_{(X,\gamma)} : \text{prof}_{(X,\gamma)} \to \text{moves}_{(X,\gamma)}$, we use the finality of $\text{moves}_{(X,\gamma)}$, i.e., we want to give $\text{prof}_{(X,\gamma)}$ a $F_{\text{moves}}$-coalgebra structure. It is sufficient to give, for $Q \in \text{Set}^X$, a natural transformation $p_Q : \varphi_{\text{prof},X}(Q) \to \varphi_{\text{moves},X}(Q)$ in $\text{Set}^{F_{\text{Tree}}(X)}$, which we can do as follows.

$$p_Q (\text{inl} *) * = * \\ p_Q (\text{inr} (q, n, f)) (a, \sigma) = (a, \sigma(a))$$

Instantiating at component $Q = \text{prof}_{(X,\gamma)}$ and composing with the isomorphism $s_x$ gives $\text{prof}_{(X,\gamma)}$ a $F_{\text{moves}}$-coalgebra structure, as required. Hence there is a unique family of functions $\text{play}_{(X,\gamma)}(x) : \text{prof}_{(X,\gamma)}(x) \to \text{moves}_{(X,\gamma)}(x)$, which, up to the isomorphisms $s_x$ and $m_x$, satisfies the following definition.

$$\text{play} \in \prod_{x \in X} (\text{prof}_{(X,\gamma)}(x) \to \text{moves}_{(X,\gamma)}(x))$$

$$\begin{array}{l@{\qquad}l} \text{play}(x, *) = * & \text{when } \gamma(x) = (\text{inl} *) \\ \text{play}(x, (a, \sigma)) = (a, \text{play}(f(a), \sigma(a))) & \text{when } \gamma(x) = \text{inr}(q, n, f) \end{array}$$

### 3.2.2. Payoff functions and the game coalgebra

From now on, let $R$ be a set of 'rewards' or 'payoffs'. Common choices are $R = \mathbb{Q}$, the rational numbers or $R = \mathbb{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 \to P$, representing choices of payoffs for each of the players.
**Definition 10.** A payoff function for an $F_{ETree}$-coalgebra $(X, \gamma)$ at state $x \in X$ is a function

$$u : \mathit{moves}_{(X,\gamma)}(x) \to \mathbb{R}^P.$$

The set of payoff functions for each $x \in X$ is denoted by $\mathit{pay}_{(X,\gamma)}(x)$.

**Example 11** (Dollar Auction (continues from Example 8)). Recall that $\mathit{moves}_{(D,\delta)}(\mathit{turn}_p)$ is given by the conatural numbers. The payoff function for the Dollar Auction game (where $R = [-\infty, +\infty)^{\dagger}$) can be defined in two steps. First, we coinductively define a map into colists$^\ddagger$ of payoffs $\mathit{List}^\infty \mathbb{R}^P$ (which we think of as ‘ledgers’):

$$\mathit{led} \in \prod_{x \in D} (\mathit{moves}_{(D,\delta)}(x) \to \mathit{List}^\infty \mathbb{R}^P)$$

$$\mathit{led end} * = \mathit{Empty}$$

$$\mathit{led turn}_A m = \begin{cases} (A \mapsto 0, B \mapsto 1) :: \mathit{Empty} & \mathit{pred} m = \mathit{inl} * \\ (A \mapsto -0.1, B \mapsto 0) :: (\mathit{led turn}_B n) & \mathit{pred} m = \mathit{inr} n \end{cases}$$

$$\mathit{led turn}_B m = \begin{cases} (A \mapsto 1, B \mapsto 0) :: \mathit{Empty} & \mathit{pred} m = \mathit{inl} * \\ (A \mapsto 0, B \mapsto -0.1) :: (\mathit{led turn}_A n) & \mathit{pred} m = \mathit{inr} n \end{cases}$$

Then the actual utility function is given by summing up componentwise all the payoffs collected by the players during the game:

$$u_{\mathit{Dollar}} m = \sum_{n=0}^{+\infty} p_i, \quad \text{where } p = \mathit{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 = \omega$, this will unfold into an infinite sum where the summands alternate between $(A \mapsto -0.1, B \mapsto 0)$ and $(A \mapsto 0, B \mapsto -0.1)$, therefore yielding the payoff vector $(A \mapsto -\infty, B \mapsto -\infty)$.

**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

<footnote>$^\dagger$We assume that $-\infty + m = -\infty$ for every $m \in \mathbb{R}$.</footnote>

<footnote>$^\ddagger$Colists of $A$ are ‘possibly infinite lists’, i.e. terms of the final coalgebra of $X \mapsto 1+A \times X$ for a given $A$. We denote $\mathit{inl} *$ as Empty and $\mathit{inr} (a, x)$ as $a :: x$.</footnote>
14 M. Capucci, N. Ghani, C. Kupke, J. Ledent, and F. Nordvall Forsberg

factor $0 < \delta < 1$. Discounting reflects the real-world tendency to value future payoffs less than present ones.

Thus let $v_T \in \prod_{x \in \text{Rep}_T} (\text{leaves}(x) \to \mathbb{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 $\delta$, we get a payoff function $u_{T,\delta}^\infty \in \prod_{x \in \text{Rep}_T} (\text{moves}_{(\text{Rep}_T, \rho_T)}(x) \to \mathbb{R}^P)$ by setting (recall that $\text{moves}_{(\text{Rep}_T, \rho_T)}(x) = (\text{leaves } x) \times (\text{leaves root})^N$):

$$u_{T,\delta}^\infty x(m_0, ms) := (v_T x m_0) + \sum_{i=0}^{+\infty} \delta^{i+1} \cdot (v_T x (ms i)).$$

The assumption of $|\delta| < 1$ guarantees the convergence of such a sum.

We are now ready to define the “game coalgebra” — an $F_{\text{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, \gamma)$ be an $F_{\text{ETree}}$-coalgebra. The game coalgebra $(Z_{(X,\gamma)}, \Gamma)$ is the $F_{\text{ETree}}$-coalgebra with carrier set

$$Z_{(X,\gamma)} = \sum_{x \in X} \text{prof}_{(X,\gamma)}(x) \times \text{pay}_{(X,\gamma)}(x)$$

and dynamics given by the map $\Gamma$ defined by

$$\Gamma(x, \sigma, u) = \begin{cases} \text{inl} * & \text{if } \gamma(x) = \text{inl} * \\ \text{inr} (q, n, a \mapsto (f a, \text{next } \sigma a, u_a)) & \text{if } \gamma(x) = \text{inr} (q, n, f) \end{cases}$$

where $u_a(\pi') = u(\text{cons}(a, \pi'))$, for $a \in [n]$ and $\pi' \in \text{moves}_{(X,\gamma)}(f a)$.

### 3.3. 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 unilaterally deviating from their strategy in exactly one state, and the usual Nash equilibrium 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.
### 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, \gamma)$ be an $F_{ETree}$-coalgebra. Consider the predicate lifting $\varphi_{\square}: \mathcal{P}(X) \to \mathcal{P}(F_{ETree}X)$ defined by

$$ \varphi_{\square}(Q) = \{\mathrm{inl} *\} \cup \{\mathrm{inr}(q, n, f) \mid (\forall a \in [n]) f(a) \in Q\} $$

and for a predicate $P \in \mathcal{P}(X)$, define $\square P$ to be the greatest fixpoint of

$$ F_{\square,P}(U) = P \cap \gamma^{-1}(\varphi_{\square}(U)). $$

A detailed discussion of this operator can be found e.g. in Jacobs (2016) where $\square$ is referred to as the “henceforth” operator. Intuitively, given a predicate $P$, $\square 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 $\square$-operator satisfies the properties one would expect from basic modal logic.

**Lemma 15.** The modality $\square$ is monotone, i.e. if $P$ implies $Q$ then $\square P$ implies $\square Q$. Furthermore $\square P \subseteq P$ and $\square P \subseteq \square\square P$.

*Proof.* Assume $P \subseteq Q$. To show $\square P \subseteq \square Q$, we use the finality of $\square Q$ to conclude $\square P \subseteq \square Q$ by showing that $\square P \subseteq F_{\square,Q}(\square P)$. This follows since $\square P \subseteq F_{\square,P}(\square P)$ and $P \subseteq Q$. In the same way, $\square P \subseteq P$ and $\square P \subseteq \square\square P$.

### 3.3.2. 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,\gamma)}$, the current strategy is unimprovable for the current player. We then ask that this predicate holds everywhere in the tree using the ‘everywhere’ modality.
16 M. Capucci, N. Ghani, C. Kupke, J. Ledent, and F. Nordvall Forsberg

**Definition 16.** We define the predicate Unimprov on $Z_{(X,\gamma)}$ by:

$$ (x, \sigma, u) \in \text{Unimprov} \text{ if } \gamma(x) = \text{inl} * \\ \text{or } \gamma(x) = \text{inr}(q, n, f) \\ \text{and } \text{now } \sigma \in \text{argmax}(a \mapsto \pi_q(u_a(\text{play}(f a) (\text{next } \sigma a)))) $$

The ‘one-shot’ equilibrium concept can now be defined as □Unimprov.

In words, $(x, \sigma, u) \in \text{Unimprov}$ holds if $x$ is a leaf, or if $x$ is an internal node and now $\sigma$ 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 $\sigma$. This equilibrium concept also occurs in Lescanne and Perrinel (2012) and Abramsky and Winschel (2017), who call it “subgame perfect equilibria”. We prefer to reserve that name for the predicate □Nash that we will define in the next section.

### 3.3.3. 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 $\equiv_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 \in P$ and state $x \in X$, we define a family of relations

$$ \equiv_p \subseteq \text{prof}_{(X,\gamma)}(x) \times \text{prof}_{(X,\gamma)}(x) $$

as the maximal family such that for all $\sigma, \sigma' \in \text{prof}_{(X,\gamma)}(x)$ and $x \in X$, we have $\sigma \equiv_p \sigma'$ if and only if one of the following is satisfied:

(1) $\gamma(x) = \text{inl} *$, or

(2) $\gamma(x) = \text{inr}(p, n, f)$ and $\text{next } \sigma a \equiv_p \text{next } \sigma' a$ for all $a \in [n]$, or

(3) $\gamma(x) = \text{inr}(q, n, f)$ with $q \neq p$, now $\sigma = \text{now } \sigma'$ and $\text{next } \sigma a \equiv_p \text{next } \sigma' a$ for all $a \in [n]$.

We can use the universal property of $\equiv_p$ to deduce the following:

**Lemma 18.** Assume the set of players $P$ has decidable equality. For each player $p \in P$, the relation $\equiv_p$ is reflexive. □
Using $\equiv_p$ to talk about deviations, we can now formulate the Nash equilibrium concept. Unlike the 'one-step' equilibrium, the definition of a Nash equilibrium 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,\gamma)}, \Gamma)$ we define

$$ (x, \sigma, u) \in \mathbf{Nash} $$

$$ \text{if } \forall p \in P. \forall \sigma' \in \mathbf{prof}_{(X,\gamma)}(x). $$

$$ (\sigma \equiv_p \sigma') \rightarrow (\pi_p u(\mathbf{play} x \sigma) \geq \pi_p u(\mathbf{play} x \sigma')) $$

In other words, given an initial node $x$ and payoff function $u$, the strategy profile $\sigma$ is a Nash equilibrium if every possible deviation $\sigma'$ by player $p$ yields a payoff for $p$ which is smaller than the one of $\sigma$.

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.

## 4. 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, \sigma, u)$ be a state of the game coalgebra $(Z_{(X,\gamma)}, \Gamma)$. If $(x, \sigma, u) \in \square\text{Nash}$ then $(x, \sigma, u) \in \square\text{Unimprov}$.

*Proof.* Since □ is monotone by Lemma 15, it is sufficient to show that $(x, \sigma, u) \in \text{Nash}$ implies $(x, \sigma, u) \in \text{Unimprov}$. If $\gamma(x) = \text{inl}*$, this is trivial, so we concentrate on the case when $\gamma(x) = \text{inr}(q, n, f)$. By definition, we have to show that

$$ \pi_q(u_{\text{now}\sigma}(\mathbf{play}(f(\text{now}\sigma)))(\text{next}\sigma(\text{now}\sigma))) \geq \pi_q(u_a(\mathbf{play}(f a))(\text{next}\sigma a)) $$

for every $a \in [n]$. For each $a$, let $\sigma_a$ be the strategy profile with now $\sigma_a = a$ and next $\sigma_a = \text{next}\sigma$. By Lemma 18, $\sigma \equiv_q \sigma_a$, and the conclusion follows from the assumption that $(x, \sigma, u) \in \text{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_{\text{moves}}$-coalgebras.

**4.1. 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_{\text{moves}}$-coalgebra we use the projections into the terminal sequence of $F_{\text{moves}}$. This technique can be formulated for arbitrary functors on indexed families of sets.

**Definition 21.** Let $H : \text{Set}^X \to \text{Set}^X$ a functor, and $(A, \gamma)$ an $H$-coalgebra. Recall that $\top_X(x) = 1$ is the terminal object in $\text{Set}^X$. We define a family of natural transformations $(\gamma^i : A \to H^i(\top_X))_{i \in \mathbb{N}}$ inductively by:

<figure><img src="image_10.png" /></figure>

where $\gamma^0 := !_A$ is the unique morphism from $A$ into the terminal object. We call states $a, a' \in A(x)$ $n$-step equivalent, and we write $a \sim_n a'$, when $\gamma_x^n(a) = \gamma_x^n(a')$. This induces a pseudometric on $A(x)$ by putting $d_{(A,\gamma)}^x(a, a') = 2^{-m}$, where $m = \sup\{n | a \sim_n a'\}$.

If $H$ is finitary, i.e. determined by its action on finitely presentable objects (Adamek and Rosicky, 1994), then if two states in an $H$-coalgebra $(A, \gamma)$ agree for all finite observations, they are equal. Hence in this case $d_{(A,\gamma)}^x$ is actually a metric:

**Lemma 22.** Let $H : \text{Set}^X \to \text{Set}^X$ be a finitary functor. For each $H$-coalgebra $(A, \gamma)$ and $x \in X$, $d_{(A,\gamma)}^x$ is a metric on $A(x)$.

The lemma is a straightforward consequence of a similar result for Set-functors (Barr, 1993; Worrell, 2000). We apply the above lemma to the functor $F_{\text{moves}} : \text{Set}^X \to \text{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, \gamma)$ be an $F_{\text{ETree}}$-coalgebra. We call $u \in \text{pay}_{(X,\gamma)}(x)$ continuous at infinity if $u : \text{moves}_{(X,\gamma)}(x) \to R^P$ is uniformly continuous as
a map between metric spaces, i.e., if

$$ \forall \varepsilon > 0. \exists \delta > 0. \forall m, m'. d_{\text{moves}_{(X,\gamma)}}^{x}(m, m') < \delta \rightarrow d_{R^P}(u(m), (u m')) < \varepsilon $$

**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 point-wise continuity would be sufficient to prove Theorem 31 (or the corresponding traditional statement (Fudenberg and Tirole, 1991, Theorem 4.2)). Classically, $\text{moves}_{(X,\gamma)}(x)$ is compact (Kurz and Pattinson, 2002), and the distinction disappears, but this is of course not constructively valid.

Spelling out the definition of $d_{\text{moves}_{(X,\gamma)}}^x$ and $d_{R^P}$, we arrive at the following concrete definition of continuity at infinity:

**Proposition 25.** Let $(X, \gamma)$ be an $F_{\text{ETree-coalgebra}}$. A payoff function $u \in \text{pay}_{(X,\gamma)}(x)$ is continuous at infinity if and only if

$$ \forall \varepsilon > 0. \exists n \in \mathbb{N}. \forall m, m'. (m \sim_n m') \rightarrow \forall p \in P. d_R(\pi_p(u m), \pi_p(u m')) < \varepsilon $$

□

**Example 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 = \pi_A \circ u$, since $\pi_B \circ u$ is the same up to a shift. Let us begin by specifying a metric on $R = [-\infty, +\infty):^§$

$$ d_R(r, r') = |\arctan r - \arctan r'| $$

This choice of metric makes $R$ into a bounded space, since evidently $\text{diam}(R) = \pi$. In particular, $d_R((u_A m), (u_A m'))$ is finite for every $m, m' \in \text{moves}_{(D,\delta)}(x)$.

By applying tan at both sides^¶ of $d_R((u_A m), (u_A m')) < \varepsilon$, our thesis becomes

$$ \forall \varepsilon > 0. \exists n \in \mathbb{N}. \forall m, m'. m \sim_n m' \rightarrow \frac{|(u_A m) - (u_A m')|}{1 + (u_A m)(u_A m')} < \tan \varepsilon. \quad (1) $$

Observe that, when $m, m' \rightarrow +\infty$,

$$ g((u_A m), (u_A m')) \rightarrow 0 \quad \text{where} \quad g(x, y) = \frac{|x - y|}{1 + xy} $$

<footnote>§We cannot use the traditional Euclidean metric on $R = \mathbb{R}$ since $| -\infty - r | = +\infty$ for finite $r \in \mathbb{R}$. Any well-defined metric that makes $R$ into a bounded space is equivalent.</footnote>

<footnote>¶The function tan, by virtue of being monotone on the domain $(-\pi/2, +\pi/2)$, preserves inequalities for small enough $\varepsilon$ (and, by previous considerations on the diameter of $(R, d_R)$, for every value of $d_R((u_A m), (u_A m'))$).</footnote>
since $(u_A m), (u_A m') \to -\infty$ by the definition of $u_A$ and $g(x, y) \to 0$ as $x, y \to -\infty$. This convergence gives an $n \in \mathbb{N}$ for each chosen $\tan \varepsilon > 0$. Suppose now $m \sim_n m'$. In this particular example, this can happen if and only if either $m, m' < n$ and $m = m'$, or $m, m' \ge n$. In the first case, $d_{R^P}((u_A m), (u_A m')) = 0 < \tan \varepsilon$. In the second case, we have chosen $n$ to satisfy $d_{R^P}((u_A m), (u_A m')) < \tan \varepsilon$. 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 = \pi_p \circ (v_T A)$ (using notation from Example 12), we see that we are tasked to prove:

$$ \begin{gathered} \forall \varepsilon > 0. \exists n \in \mathbb{N}. \forall (m_0, ms), (m'_0, ms'). \\ (m_0, ms') \sim_n (m'_0, ms') \to \\ \left| (v(m_0) - v(m'_0)) + \sum_{i=0}^{+\infty} \delta^{i+1} (v(ms_i) - v(ms'_i)) \right| < \varepsilon \end{gathered} $$

In this case, $(m_0, ms') \sim_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.

## 4.2. The one-shot deviation principle

The one-shot equilibrium concept states that there is no profitable single-node 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 \in P$ be a player, $x \in X$ a state, and $(X, \gamma)$ an $F_{\mathbb{E}Tree}$-coalgebra. We define a family of relations $\equiv_p^{\text{fin}} \subseteq \text{prof}_{(X,\gamma)}(x) \times \text{prof}_{(X,\gamma)}(x)$ inductively as the least family such that for all $\sigma, \sigma' \in \text{prof}_{(X,\gamma)}(x)$ and $x \in X$ we have $\sigma \equiv_p^{\text{fin}} \sigma'$ iff one of the following is satisfied

(1) $\sigma = \sigma'$, or

(2) $\gamma(x) = \text{inl} \ast$, or

(3) $\gamma(x) = \text{inr} p n f$ and $\text{next} \sigma a \equiv_p^{\text{fin}} \text{next} \sigma' a$ for all $a \in [n]$, or
(4) $\gamma(x) = \text{inr } q \ n \ f$ with $q \neq p$, now $\sigma = \text{now } \sigma'$ and $\text{next } \sigma a \equiv_p^{\text{fin}} \text{next } \sigma' a$ for all $a \in [n]$.

Thus strategies with $\sigma \equiv_p^{\text{fin}} \sigma'$ can differ in their choice of action now $\sigma \neq$ now $\sigma'$ 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 $\sigma$ and $\sigma'$, we can “truncate” $\sigma$ after $n$ rounds by replacing it with $\sigma'$, resulting in a new strategy $[\sigma]_n^{\sigma'}$.

**Lemma 29.** If $\sigma \equiv_p \sigma'$, then $\sigma \equiv_p^{\text{fin}} [\sigma']_n^\sigma$ for any $n \in \mathbb{N}$. Conversely, if the set of players $P$ has decidable equality, then $\sigma \equiv_p^{\text{fin}} \sigma'$ implies $\sigma \equiv_p \sigma'$.

*Proof.* The first statement follows by induction on $n$. Since $[\sigma']_0^\sigma = \sigma$, we have by $\sigma \equiv_p^{\text{fin}} [\sigma']_0^\sigma$ by (1). For the step case, consider the form of the proof $\sigma \equiv_p \sigma'$: if $\sigma \equiv_p \sigma'$ because $\gamma(x) = \text{inl} \*$, we immediately have $\sigma \equiv_p^{\text{fin}} [\sigma']_{n+1}^\sigma$; otherwise $p=q$ or $p \neq q$, and in either case $\text{next } \sigma a \equiv_p \text{next } \sigma' a$ for all $a \in [m]$, hence by the induction hypothesis $\text{next } \sigma a \equiv_p^{\text{fin}} [\text{next } \sigma' a]_n^{\text{next } \sigma a}$ for every $a$, and by either (3) or (4) and how $[\sigma]_n^{\sigma'}$ is defined, we have $\sigma \equiv_p^{\text{fin}} [\sigma']_{n+1}^\sigma$ as required.

The second statement follows easily by induction on the proof that $\sigma \equiv_p^{\text{fin}} \sigma'$, using decidable equality on $P$ to invoke Lemma 20 for the base case (1). $\square$

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 $< \in$ 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, \sigma, u)$ be a state of the game coalgebra $(Z_{(X,\gamma)}, \Gamma)$. Assume that the order relation $< \in$ on $R$ is trichotomous. If there is a player $p$ and a strategy $\sigma'$ such that $\sigma \equiv_p^{\text{fin}} \sigma'$ and $\pi_p(u(\text{play } x \sigma')) > \pi_p(u(\text{play } x \sigma))$ then $(x, \sigma, u) \in \neg\Box\text{Unimprov.}$

*Proof.* By induction on the proof that $\sigma \equiv_p^{\text{fin}} \sigma'$, we can find a strategy $\sigma''$ that differs from $\sigma$ (and agrees with $\sigma'$) a minimum number of times, whilst still being a profitable deviation. In addition, there is a deepest node where $\sigma''$ differs from $\sigma$; let $\sigma'''$ be the strategy that agrees with $\sigma$ everywhere
but at this node, where it agrees with $\sigma'$. By trichotomy, we either have $\pi_p(u(\text{play } x \sigma'')) > \pi_p(u(\text{play } x \sigma))$ or $\pi_p(u(\text{play } x \sigma'')) \le \pi_p(u(\text{play } x \sigma))$. 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 $\sigma''$ is minimal. $\square$

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 = \mathbb{Q}$ with the standard metric $d_{\mathbb{Q}}(x, y) = |x - y|$. Note that the order on $\mathbb{Q}$ certainly is trichotomous.

**Theorem 31.** Assume the set of players P has decidable equality. Let $(x, \sigma, u)$ be a state of the game coalgebra $(Z_{(X,\gamma)}, \Gamma)$ with rewards $R = \mathbb{Q}$. If $u$ is continuous at infinity and $(x, \sigma, u) \in \square\text{Unimprov}$, then $(x, \sigma, u) \in \square\text{Nash}$.

*Proof.* Since $\square P \subseteq \square\square P$ and $\square$ is monotone by Lemma 15, it is sufficient to show that $(x, \sigma, u) \in \square\text{Unimprov}$ implies $(x, \sigma, u) \in \text{Nash}$. Hence, assume a player $p$ and a strategy $\sigma'$ with $\sigma \equiv_p \sigma'$ are given; by trichotomy of $<$, it is enough the show that

$$u_p(\text{play } x \sigma) < u_p(\text{play } x \sigma')$$

where we write $u_p(m) = \pi_p(u(m))$, is impossible. By continuity of $u$ with $\varepsilon = u_p(\text{play } x \sigma') - u_p(\text{play } x \sigma)$, we find $n$ such that if $m \sim_n \text{play } x \sigma'$ then $|u_p(\text{play } x \sigma') - u_p(m)| < \varepsilon$. Consider the history $m = \text{play } x \sigma''$, where $\sigma'' = [\sigma']_n^\sigma$ is $\sigma'$ up to depth $n$, and $\sigma$ thereafter. By construction, $m \sim_n \text{play } x \sigma'$. We claim that $\sigma''$ is still a strictly profitable deviation, i.e. $u_p(\text{play } x \sigma) < u_p(\text{play } x \sigma'')$, by trichotomy of $<$ again: if $u_p(\text{play } x \sigma) \ge u_p(\text{play } x \sigma'')$ then both $|u_p(\text{play } x \sigma') - u_p(\text{play } x \sigma'')| \ge \varepsilon$ and $|u_p(\text{play } x \sigma') - u_p(\text{play } x \sigma'')| < \varepsilon$, which is absurd. Hence we have found a profitable finite deviation, which by Lemmas 29 and 30 contradicts the assumption that $(x, \sigma, u) \in \square\text{Unimprov}$. Therefore, we must instead have $u_p(\text{play } x \sigma) \ge u_p(\text{play } x \sigma')$ as required. $\square$

## 5. 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 continuous—
a well-known result in the game theory literature, here extended to more
general coalgebras. In future work, we plan to exploit techniques from coal-
gebra and automata theory to use our framework to *solve* various infinite-
horizon 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 (Capucci et al., 2021) 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.

**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.

References

Abramsky, S. and Winschel, V. (2017). Coalgebraic analysis of subgame-perfect equilibria in infinite games without discounting, *Math. Struct. Comput. Sci.* **27**, 5, pp. 751–761, doi:10.1017/S0960129515000365.

Adamek, J. and Rosicky, J. (1994). *Locally Presentable and Accessible Categories*, London Mathematical Society Lecture Note Series, Cambridge University Press, doi:10.1017/CBO9780511600579.

Barr, M. (1993). Terminal coalgebras in well-founded set theory, *Theoretical Computer Science* **114**, 2, pp. 299–315, doi:10.1016/0304-3975(93)90076-6.

Bishop, E. and Bridges, D. (1985). *Constructive Analysis*, Springer.

Bridges, D. S. (1982). Preference and utility: A constructive development, *Journal of Mathematical Economics* **9**, 1, pp. 165–185, doi:10.1016/0304-4068(82) 90025-8.

Bridges, D. S. (1989). The constructive theory of preference relations on a locally compact space, *Indagationes Mathematicae* **92**, 2, pp. 141–165, doi: 10.1016/S1385-7258(89)80023-X.

Bridges, D. S. (1994). The constructive theory of preference relations on a locally compact space II, *Mathematical Social Sciences* **27**, 1, pp. 1–9, doi:10.1016/0165-4896(94)00718-7.

Bridges, D. S. (2004). First steps in constructive game theory, *Mathematical Logic Quarterly* **50**, 4-5, pp. 501–506.
Capucci, M., Ghani, N., Ledent, J. and Nordvall Forsberg, F. (2021). Translating extensive form games to open games with agency, in *Applied Category Theory '21*.

Fudenberg, D. and Tirole, J. (1991). *Game Theory*, MIT Press, Cambridge, MA.

Ghani, N., Kupke, C., Lambert, A. and Forsberg, F. N. (2018). A compositional treatment of iterated open games, *Theor. Comput. Sci.* **741**, pp. 48–57, doi:10.1016/j.tcs.2018.05.026.

Jacobs, B. (2016). *Introduction to Coalgebra: Towards Mathematics of States and Observation*, Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, doi:10.1017/CBO9781316823187.

Kuhn, H. W. (1953). Extensive games and the problem of information, in H. W. Kuhn and A. W. Tucker, eds., *Contributions to the theory of games, Volume II (Annals of Mathematics Studies, 28)*, pp. 193–216, Princeton University Press.

Kurz, A. and Pattinson, D. (2002). Definability, canonical models, compactness for finitary coalgebraic modal logic, *Electronic Notes in Theoretical Computer Science* **65**, 1, pp. 135–155, doi:10.1016/S1571-0661(04)80363-3.

Lescanne, P. (2013). A simple case of rationality of escalation, in R. Heckel and S. Milius, eds., *CALCO '13, LNCS*, Vol. 8089, Springer, pp. 191–204, doi: 10.1007/978-3-642-40206-7\_15.

Lescanne, P. (2018). Dependent types for extensive games, *J. Formaliz. Reason.* **11**, 1, pp. 1–17, doi:10.6092/issn.1972-5787/7517.

Lescanne, P. and Perrinel, M. (2012). “Backward” coinduction, Nash equilibrium and the rationality of escalation, *Acta Informatica* **49**, 3, pp. 117–137, doi: 10.1007/s00236-012-0153-3.

Leyton-Brown, K. and Shoham, Y. (2008). *Essentials of Game Theory: A Concise Multidisciplinary Introduction*, Morgan & Claypool.

Mycielski, J. and Taylor, W. (1976). A compactification of the algebra of terms, *Algebra Universalis* **6**, pp. 159–163.

Osbourne, M. and Rubinstein, A. (1994). *A course in game theory*, MIT Press.

Rutten, J. (2000). Universal coalgebra: a theory of systems, *Theoretical Computer Science* **249**, 1, pp. 3–80, doi:10.1016/S0304-3975(00)00056-6.

Selten, R. (1975). Reexamination of the perfectness concept for equilibrium points in extensive games, *International Journal of Game Theory* **4**, pp. 25–55, doi:10.1007/BF01766400.

Selten, R. (1978). The chain store paradox, *Theory and decision* **9**, 2, pp. 127–159, doi:10.1007/BF00131770.

Shubik, M. (1971). The dollar auction game: A paradox in noncooperative behavior and escalation, *Journal of conflict Resolution* **15**, 1, pp. 109–111.

Worrell, J. (2000). *On coalgebras and final semantics*, Ph.D. thesis, University of Oxford.