# Higher-order Games with Dependent Types

Martín Escardó  Paulo Oliva

###### Abstract

In previous work on higher-order games, we accounted for finite games of
unbounded length by working with continuous outcome functions, which carry
implicit game trees. In this work we make such trees explicit. We use concepts
from dependent type theory to capture history-dependent games, where the set
of available moves at a given position in the game depends on the moves played
up to that point. In particular, games are modelled by a $W$-type, which is
essentially the same type used by Aczel to model constructive Zermelo-Frankel
set theory (CZF). We have also implemented all our definitions, constructions,
results and proofs in the dependently-typed programming language Agda, which,
in particular, allows us to run concrete examples of computations of optimal
strategies, that is, strategies in subgame perfect equillibrium.

###### keywords:

Computational game theory , selection function , optimal strategies , subgame
perfect equilibrium , dependent type theory , Agda.

††journal: Theoretical Computer Science

[inst1]organization=School of Computer Science, University of
Birmingham,addressline=Bristol Road, city=Birmingham, postcode=B15 2TT,
country=UK

[inst2]organization=School of Electronic Engineering and Computer Science,
Queen Mary University of London,addressline=Mile End Road, city=London,
postcode=E1 4NS, country=UK

#### We dedicate this paper to Ulrich Berger on the occasion of his 65th
birthday

Our use of selection functions in this paper, and in our previous work, is
inspired by Ulrich’s PCF definition of the Fan Functional [4]. In particular,
the product of selection functions, which we use to compute optimal
strategies, is a generalisation of his seminal construction of a selection
function for the Cantor space for defining the Fan Functional.

##  1 Introduction

Games of perfect information are normally modelled in economics and game
theory via _maximising_ players. At the end of each play in the game all
players receive a payoff, so that players pick their moves in order to
maximise their final payoff. In zero-sum games, usually one considers two
players and a single outcome, where one player is trying to maximise the
outcome, while the other tries to minimise it.

Higher-order games [10, 12] have been introduced as a generalisation of both
of these frameworks, where the outcome type of the game can have an arbitrary
type $R$, and the goal of each player at a round where $X$ is the set of
available moves is defined via generalised _quantifiers_ , which are higher-
order functions of type $(X\to R)\to R$.

Standard examples of sequential games of perfect information, such as Tic-Tac-
Toe, checkers and chess, can be modelled by taking $R$ to be the linearly
ordered set $\\{-1<0<1\\}$, so that the two players correspond to the
quantifiers $\max,\min\colon(X\to R)\to R$ (see [11]). This setup is rather
general, in particular allowing to treat sequential games of unbounded length
[13].

In this paper we account for history-dependent sequential games of perfect
information of unbounded length, where the set of available moves at a given
position in the game depends on the moves played up to that point. This is
achieved by modelling game trees as a certain type of well-founded _dependent
type trees_. In previous work this was instead done by considering either a
fixed game length, or games of countable length with a continuous outcome
function [10]. In fact, every continuous function carries an implicit well-
founded tree, and this goes back to Brouwer. Here we work with explicitly
given well-founded trees instead.

We make use of concepts from _dependent type theory_ [5] in order to formalise
this, and we have implemented all our definitions, results and proofs in Agda
[3], which is both a programming language and a proof assistant based on
dependent type theory.

#### Related work

Our type of trees is essentially the same as that used by Leversha [20] to
define ordinals, and by Aczel [2] to model constructive Zermelo-Frankel set
theory (CZF). The precise relationship is discussed in Section 5.

As in previous work [10], we think of backward induction in terms of a certain
product of selection functions (Definition 4.13 below). The product of
selection functions is also a manifestation of bar recursion [14], used to
interpret classical proofs in analysis [8, 9], and can be used to give
computational content to the Tychonoff Theorem from topology [7]. See our
survey paper [11] where the versatility of the product of selection functions
is discussed in further detail.

Several other recent papers also explore the connection between selection
functions and computational interpretations of classical analysis, e.g. Powell
[21, 22].

Ghani, Hedges, Winschel, and Zahn [17] introduce a notion of _open game_ ,
which is compositional and hence allows to build larger games from smaller
blocks, where quantifiers are generalised to best-response functions.

Hartmann and Gibbons [18] apply selection functions to algorithm design by
considering modified notions of (history dependent) products of selection
functions, which allows them to design greedy algorithms in a modular way.

Abadi and Plotkin [1] consider programming languages for describing systems in
terms of choices and their resulting costs and rewards, and use the selection
monad to define computationally adequate denotational semantics for them.

#### Organisation

Section 2: Dependent type trees. Section 3: Quantifiers and higher-order games
with dependent types. Section 4: Selection functions and their use for the
computation of optimal strategies, and main theorem. Section 5: Discussion of
the relationship of our type of type trees with the $W$-type of iterative sets
used by Leversha [20] to define ordinals in dependent type theory, and by
Aczel [2] to model CZF. Section 6: Proofs and programs in Agda.

##  2 Dependent type trees

We assume some familiarity with dependent type theory [5]. However, we reason
informally, but rigorously, as in the book [23]. We write the type
$\Pi(x:X),A(x)$ as $(x:X)\to A(x)$. The elements of this types are functions
that map elements $x:X$ to values in $A(x)$. We write the type
$\Sigma(x:X),A(x)$ as $(x:X)\times A(x)$. The elements of this type are
(dependent) pairs $(x,y)$ with $x:X$ and $y:A(x)$. We work with a universe
$\operatorname{Type}$, which is a large type of small types closed under the
type theoretic operations.

We consider sequential game plays of the form $x_{0},\dots,x_{n-1}$ where the
type of the second move $x_{1}$ depends on the first move $x_{0}$, and the
type of the third move $x_{2}$ depends on the first and second moves $x_{0}$
and $x_{1}$, and so on. In order to specify such a dependent sequence of
moves, we first define dependent-type trees.

######  Definition 2.1 ((Dependent) type trees)

We define the type $\operatorname{Tree}$ of _dependent type trees_ , or just
_type trees_ for short, by induction as follows

  1. 1.

There is an empty type tree, denoted by $[]$.

  2. 2.

If $X$ is a type and $X^{\scriptscriptstyle f}\colon X\to\operatorname{Tree}$
is a family of trees indexed by $X$, then there is a type tree with root $X$
and subtrees $X^{\scriptscriptstyle f}(x)$ for each $x:X$, denoted by
$X\operatorname{::}X^{\scriptscriptstyle f}$. We think of
$X^{\scriptscriptstyle f}$ as a _forest_.

So notice that $(-)\operatorname{::}(-)$ is a function of type

$(X:\operatorname{Type})\times(X\to\operatorname{Tree})\to\operatorname{Tree}.$

We adopt the following notational conventions:

  1. 1.

The variable $X$ ranges over types.

  2. 2.

The variable $X^{\scriptscriptstyle t}$ ranges over type trees.

  3. 3.

The variable $X^{\scriptscriptstyle f}$ ranges over type forests.

######  Example 2.2 (Tic-Tac-Toe type tree)

In Tic-Tac-Toe, the types of available moves at each round form a dependent
type tree. The root of the tree is the type of the nine positions on the grid.
Depending on the move of the first player, the second player then chooses from
the type of the eight remaining available positions, and so on. Once one of
the players wins or all the positions are filled then the next player does not
have any further available move, arriving at an empty subtree.

A dependent sequence of moves as discussed above is given by a path in a
dependent type tree.

######  Definition 2.3 (Paths)

We define the type $\operatorname{\mathrm{Path}}X^{\scriptscriptstyle t}$ of
paths on a type tree $X^{\scriptscriptstyle t}$ by induction on
$X^{\scriptscriptstyle t}$ as follows:

  1. 1.

There is one path in the empty tree $[]$, which we denote by
$\operatorname{\langle\rangle}$.

  2. 2.

For every type $X$, every forest $X^{\scriptscriptstyle f}\colon
X\to\operatorname{Tree}$, every $x:X$ and every path $\vec{x}$ in
$X^{\scriptscriptstyle f}(x)$, there is a path $x\operatorname{::}\vec{x}$ in
the tree $X\operatorname{::}X^{\scriptscriptstyle f}$. The elements $x$ and
$\vec{x}$ are called the _head_ and _tail_ of the path
$x\operatorname{::}\vec{x}$.

The above path constructors have the following types:

  1. 1.

$\operatorname{\langle\rangle}:\operatorname{\mathrm{Path}}\,[]$.

  2. 2.

$(-)\operatorname{::}(-):(x:X)\times\operatorname{\mathrm{Path}}(X^{\scriptscriptstyle
f}(x))\to\operatorname{\mathrm{Path}}(X\operatorname{::}X^{\scriptscriptstyle
f})$.

We let the variable $\vec{x}$ range over paths.

######  Example 2.4 (Tic-Tac-Toe paths)

The paths in the Tic-Tac-Toe tree consists of exactly the sequences of legal
moves that end with one of the players winning or a draw.

We will need to add different structures to the nodes of game trees, including
a type of quantifiers (Section 3.1), a type of selection functions (Section
4.1) and move choices (Section 4). We accomplish this with a type of
structured trees defined as follows, with a parameter $\operatorname{S}$ for
the structure, where structure on a type $X$ is taken to be a type
$\operatorname{S}X$

######  Definition 2.5 (Trees with structure)

Given structure $\operatorname{S}:\operatorname{Type}\to\operatorname{Type}$
and a tree $X^{\scriptscriptstyle t}:\operatorname{Tree}$ we define a new type
of structured trees

$\mathrm{structure}(\operatorname{S},X^{\scriptscriptstyle t})$

by induction on $X^{\scriptscriptstyle t}$ as follows:

  1. 1.

There is an empty structured tree

$[]:\mathrm{structure}(\operatorname{S},[]).$

  2. 2.

If $X$ is a type, $X^{\scriptscriptstyle f}\colon X\to\operatorname{Tree}$ is
a forest and

$\displaystyle s$ $\displaystyle:$ $\displaystyle\operatorname{S}X,$
$\displaystyle s^{\scriptscriptstyle f}$ $\displaystyle:$
$\displaystyle(x:X)\to\mathrm{structure}(\operatorname{S},X^{\scriptscriptstyle
f}(x)),$

then there is a structured tree

$s\operatorname{::}s^{\scriptscriptstyle
f}:\mathrm{structure}(\operatorname{S},X\operatorname{::}X^{\scriptscriptstyle
f})$

with root $X$ equipped with $s:\operatorname{S}X$ and subtrees
$s^{\scriptscriptstyle f}(x)$ for $x:X$.

Notice that in the notation $s\operatorname{::}s^{\scriptscriptstyle f}$ we
leave both types $X$ and $X^{\scriptscriptstyle f}$ implicit, and that the
forest $s^{\scriptscriptstyle f}$ is indexed by the type $X$ rather than the
type $\operatorname{S}X$. Although we use the same notation
$(-)\operatorname{::}(-)$, the type of type trees is of course not the same as
that of structured type trees, and the latter depends on the former:

$\mathrm{structure}:(\operatorname{Type}\to\operatorname{Type})\times\operatorname{Tree}\to\operatorname{Type}.$

Hence if $X^{\scriptscriptstyle t}$ is a type tree, then
$\mathrm{structure}(\operatorname{S},X^{\scriptscriptstyle t})$ is the type of
structured type trees over $X^{\scriptscriptstyle t}$. So for _one_ type tree
$X^{\scriptscriptstyle t}:\operatorname{Tree}$ there are, in general, many
structured type trees of type
$\mathrm{structure}(\operatorname{S},X^{\scriptscriptstyle t})$.

##  3 Higher-order games with dependent types

We start by recalling the notion of a _quantifier_ , needed for the definition
of a higher-order game (see [10]). For the remainder of the paper we fix a
type $R$ of game outcomes. For example, for Tic-Tac-Toe, as discussed in the
Introduction, we take $R=\\{-1,0,1\\}$, but for other games we can choose $R$
to be e.g. the type of real numbers or the type of booleans.

###  3.1 Quantifiers

Let $\operatorname{K}X$ be an abbreviation for the type $(X\to R)\to R$, with
$R$ arbitrary but fixed, as described above.

######  Definition 3.1 (Quantifiers)

We call functions of type $\operatorname{K}X$ _quantifiers_.

If $R$ is the type of booleans, the elements of the function type
$\operatorname{K}X$ include the standard existential and universal
quantifiers, but we also allow numerical quantifiers, as in the following
example.

######  Example 3.2 ($\min$ and $\max$)

The simplest non-standard examples of quantifiers are the
$\min,\max\colon(X\to R)\to R$ functions, which we will use in our Tic-Tac-Toe
running example. The idea is that the type of outcomes $R$ will the linearly
ordered type with three values $-1<0<1$, so that given a type of available
moves $X$, the quantifiers select the preferred outcome given a local outcome
function $X\to R$.

######  Definition 3.3 (Quantifier tree)

Given a type tree $X^{\scriptscriptstyle t}$, we define the type of
_quantifier trees over $X^{\scriptscriptstyle t}$_ by

$\operatorname{\mathcal{K}}X^{\scriptscriptstyle
t}=\mathrm{structure}(\operatorname{K},X^{\scriptscriptstyle t}).$

We adopt the following notational conventions:

  1. 1.

The variable $\phi$ ranges over the type $\operatorname{K}X$ of quantifiers.

  2. 2.

The variable $\phi^{\scriptscriptstyle t}$ ranges over the type
$\operatorname{\mathcal{K}}X^{\scriptscriptstyle t}$ of quantifier trees.

  3. 3.

The variable $\phi^{\scriptscriptstyle f}$ ranges over quantifier forests
$(x\colon X)\to\operatorname{\mathcal{K}}(X^{\scriptscriptstyle f}(x))$.

######  Example 3.4 (Tic-Tac-Toe quantifier tree)

We associate a quantifier tree to the Tic-Tac-Toe type tree of Example 2.2 by
alternating the $\min$ and $\max$ quantifiers depending on the level of the
tree. Assuming that player X moves first, and that the outcome $-1$ indicates
that player X has won, the root of the quantifier tree is the $\min$
quantifier.

######  Definition 3.5 (Binary dependent product of quantifiers [10])

Given a quantifier

$\phi:\operatorname{K}X$

on a type $X$ and given a family $Y$ of types indexed by $X$, and a family of
quantifiers

$\gamma\colon(x:X)\to\operatorname{K}(Y(x)),$

we define a quantifier

$\phi\operatorname{\otimes^{\tiny K}}\gamma:\operatorname{K}((x:X)\times
Y(x))$

by

$(\phi\operatorname{\otimes^{\tiny K}}\gamma)(q)=\phi(\lambda
x.\gamma(x)(\lambda y.q(x,y))).$

######  Example 3.6 (Product of $\min$ and $\max$)

For instance, for the quantifiers $\min\colon(X\to R)\to R$ and
$\max\colon(x:X)\to(Y(x)\to R)\to R$, their product corresponds to a
$\min$-$\max$ operation where the range of $y$ depends on $x$:

$(\min\operatorname{\otimes^{\tiny K}}\max)(q)=\min_{x:X}\max_{y:Y(x)}q(x,y).$

We can now adapt the iterated product of quantifiers [10] to quantifier trees.

######  Definition 3.7 (K-sequence)

To each quantifier tree

$\phi^{\scriptscriptstyle t}:\operatorname{\mathcal{K}}X^{\scriptscriptstyle
t}$

we associate a single quantifier

$\operatorname{K{-}sequence}\left(\phi^{\scriptscriptstyle
t}\right):\operatorname{K}(\operatorname{\mathrm{Path}}X^{\scriptscriptstyle
t})$

on the type of paths of the tree $X^{\scriptscriptstyle t}$ by induction as
follows.

  1. 1.

To the empty tree $[]:\operatorname{Tree}$ we associate the quantifier

$\lambda
q.q\operatorname{\langle\rangle}:\operatorname{K}(\operatorname{\mathrm{Path}}[]).$

  2. 2.

To a quantifier tree of the form
$\phi\operatorname{::}\phi^{\scriptscriptstyle f}$ we associate the quantifier

$\phi\operatorname{\otimes^{\tiny K}}(\lambda
x.\operatorname{K{-}sequence}\left(\phi^{\scriptscriptstyle f}(x)\right)).$

This inductive definition can also be written as

$\displaystyle\operatorname{K{-}sequence}([])$ $\displaystyle=$
$\displaystyle\lambda q.\operatorname{\langle\rangle},$
$\displaystyle\operatorname{K{-}sequence}(\phi\operatorname{::}\phi^{\scriptscriptstyle
f})$ $\displaystyle=$ $\displaystyle\phi\operatorname{\otimes^{\tiny
K}}(\lambda x.\operatorname{K{-}sequence}\left(\phi^{\scriptscriptstyle
f}(x)\right))$ $\displaystyle=$ $\displaystyle\lambda q.\phi(\lambda
x.(\operatorname{K{-}sequence}\left(\phi^{\scriptscriptstyle
f}(x)\right))(\lambda\vec{y}.q(x,\vec{y}))),$

by definition 3.5.

###  3.2 Higher-order games

Using the notions of type trees and quantifier trees introduced above, we can
formulate finite higher-order games as follows.

######  Definition 3.8 (Dependent higher-order game)

A finite _higher-order game_ is given by a tuple $(X^{\scriptscriptstyle
t},R,q,\phi^{\scriptscriptstyle t})$ where

  1. 1.

$X^{\scriptscriptstyle t}$ is a _type tree_ of moves available at different
stages of the game,

  2. 2.

$R$ is the type of possible _outcomes_ of the game,

  3. 3.

$q\colon\operatorname{\mathrm{Path}}(X^{\scriptscriptstyle t})\to R$ is the
_outcome function_ ,

  4. 4.

$\phi^{\scriptscriptstyle t}$ is a quantifier tree.

One can think of the type tree $X^{\scriptscriptstyle t}$ as describing the
rules of the game, specifying the available moves at each position or stage of
the game. The function
$q\colon\operatorname{\mathrm{Path}}(X^{\scriptscriptstyle t})\to R$ gives the
outcome at the end of the game, for a given sequence of moves. And the
quantifier tree $\phi^{\scriptscriptstyle t}$ describes the objective of the
game, assigning a quantifier to each position in the game. The following two
examples have the same rules and outcome functions, but different objectives.

######  Example 3.9 (Tic-Tac-Toe)

The game of Tic-Tac-Toe can be modelled as the higher-order game
$(X^{\scriptscriptstyle t},R,q,\phi^{\scriptscriptstyle t})$ where

  1. 1.

$X^{\scriptscriptstyle t}$ is a type tree of moves defined in Example 2.2,

  2. 2.

$R$ is the linearly ordered type $-1<0<1$,

  3. 3.

$q\colon\operatorname{\mathrm{Path}}(X^{\scriptscriptstyle t})\to R$ is the
_outcome function_ that, given a sequence of moves, has values $-1$ or $1$ if
one of the players has won, or $0$ if no more moves are available, and

  4. 4.

$\phi^{\scriptscriptstyle t}$ is a quantifier tree from Example 3.4.

######  Example 3.10 (Anti-Tic-Tac-Toe)

The game of Anti-Tic-Tac-Toe, where players try to avoid making three in a
row, can be modelled exactly as Tic-Tac-Toe (Example 3.9), except that the
quantifiers in the quantifier tree $\phi^{\scriptscriptstyle t}$ from Example
3.4 are swapped. The quantifiers still alternate between $\min$ and $\max$,
but now the root of the quantifier tree is the $\max$ quantifier.

Consider also the following example, where the quantifier tree is not based on
$\min$ and $\max$, but instead on existential quantifiers.

######  Example 3.11 (Eight Queens)

The game of Eight Queens, where a player attempts to place eight queens on a
chess board in such way that no queen can capture the other ones, can be
modelled as the higher-order game $(X^{\scriptscriptstyle
t},R,q,\phi^{\scriptscriptstyle t})$ as follows:

  1. 1.

$X^{\scriptscriptstyle t}$ is a type tree of moves with depth 8, describing
the positions on the chess board that have not been used yet.

  2. 2.

$R$ is the type of Booleans
$\mathbb{B}=\\{\operatorname{true},\operatorname{false}\\}$.

  3. 3.

$q\colon\operatorname{\mathrm{Path}}(X^{\scriptscriptstyle t})\to R$ is the
_outcome function_ that, given the position of the eight queens on the board,
has values $\operatorname{false}$ or $\operatorname{true}$ depending on
whether some queen can capture another or not.

  4. 4.

$\phi^{\scriptscriptstyle t}$ is the quantifier tree of existential
quantifiers $\exists\colon(X\to\mathbb{B})\to\mathbb{B}$ at each node, where
$X$ is the type of available moves at the node, defined by
$\exists(p)=\operatorname{true}$ if and only if there is $x:X$ such that
$p(x)=\operatorname{true}$.

Notice that, in the above example, in some sense there is only one player,
although the concept of player is not incorporated explicitly in our notion of
game.

######  Definition 3.12 (Optimal outcome)

Given a game $(X^{\scriptscriptstyle t},R,q,\phi^{\scriptscriptstyle t})$ we
call $\operatorname{K{-}sequence}\left(\phi^{\scriptscriptstyle
t}\right)(q):R$ the _optimal outcome_ of the game.

###### Example 3.13

In the case of Tic-Tac-Toe, it is well-known that the optimal outcome of the
game is a draw. Perhaps less well-known is that in the case of Anti-Tic-Tac-
Toc the optimal outcome is also a draw. It is too laborious to calculate these
by hand using our definitions, but the definitions can be directly translated
to e.g. Haskell or Agda programs so that optimal outcomes of games can be
automatically calculated [11, 16].

##  4 Optimal strategies

A strategy for a given type tree selects an element of each node of the tree.
Using Definition 2.5, this corresponds to the identity structure $SX=X$. That
is, for each type $X$ of moves in the game tree, the structure is an element
of $SX$, which amounts to saying that we pick an element of $X$.

######  Definition 4.1 (Type of strategies)

Given a type tree $X^{\scriptscriptstyle t}$, we define the type of
_strategies over $X^{\scriptscriptstyle t}$_ by

$\operatorname{Strategy}X^{\scriptscriptstyle t}=\mathrm{structure}((\lambda
X.X),X^{\scriptscriptstyle t}).$

The type $\operatorname{Strategy}[]$ has exactly one element
$\operatorname{\langle\rangle}$, which we think of as the empty strategy.
Given a type tree of the form $X\operatorname{::}X^{\scriptscriptstyle f}$, an
element of the type of strategies

$\operatorname{Strategy}(X\operatorname{::}X^{\scriptscriptstyle
f})=X\times((x:X)\to\operatorname{Strategy}(X^{\scriptscriptstyle f}(x))),$

is a pair consisting of a move in $X$ together with a function that maps each
such move $x:X$ to a strategy in the subtree $X^{\scriptscriptstyle f}(x)$.

######  Definition 4.2 (Strategic path)

Each $\sigma\colon\operatorname{Strategy}X^{\scriptscriptstyle t}$ determines
a single path

$\operatorname{spath}(\sigma):\operatorname{\mathrm{Path}}X^{\scriptscriptstyle
t},$

which we call the _strategic path of $\sigma$_, as follows:

  1. 1.

If $\sigma:\operatorname{Strategy}\,[]$ then its strategic path is the empty
path $\operatorname{\langle\rangle}$.

  2. 2.

If $\sigma:\operatorname{Strategy}(X\operatorname{::}X^{\scriptscriptstyle
f})$ then $\sigma$ is of the form
$x\operatorname{::}\sigma^{\scriptscriptstyle f}$ and its strategic path is
defined as $x\operatorname{::}\operatorname{spath}(\sigma^{\scriptscriptstyle
f}(x))$.

######  Definition 4.3 (Optimal strategies)

Given a game $(X^{\scriptscriptstyle t},R,q,\phi^{\scriptscriptstyle t})$, we
define the notion of optimal strategy by induction on $X^{\scriptscriptstyle
t}$ as follows.

  1. 1.

If $X^{\scriptscriptstyle t}$ is the empty tree $[]$ then any
$\sigma:\operatorname{strategy}(X^{\scriptscriptstyle t})$ is empty, which is
considered optimal,

  2. 2.

When the game has a type tree of the form
$X\operatorname{::}X^{\scriptscriptstyle f}$ with a quantifier tree for the
form $\phi\operatorname{::}\phi^{\scriptscriptstyle f}$, then a strategy
$x_{0}\operatorname{::}\sigma^{\scriptscriptstyle f}$ is optimal if the
following two conditions hold, where
$q_{x}=\lambda\vec{y}.q(x\operatorname{::}\vec{y})$:

    1. (a)

$q_{x_{0}}(\operatorname{spath}(\sigma^{\scriptscriptstyle
f}(x_{0})))=\phi(\lambda
x.q_{x}(\operatorname{spath}(\sigma^{\scriptscriptstyle f}(x))))$.

    2. (b)

For each $x:X$, the strategy $\sigma^{\scriptscriptstyle
f}(x)\colon\operatorname{strategy}(X^{\scriptscriptstyle f}(x))$ is optimal at
the subgame $(X^{\scriptscriptstyle f}(x),R,q_{x},\phi^{\scriptscriptstyle
f}(x))$.

This is a generalisation of the notion of subgame perfect equilibrium, where
quantifiers other than $\min$ and $\max$ are allowed.

######  Theorem 4.4 (Optimality theorem)

Given a game $(X^{\scriptscriptstyle t},R,q,\phi^{\scriptscriptstyle t})$ and
an optimal strategy $\sigma$ for it, we have that the outcome on the strategic
path of $\sigma$ is indeed the optimal outcome of the game, that is,

$q(\operatorname{spath}\sigma)=\operatorname{K{-}sequence}(\phi^{\scriptscriptstyle
t})(q).$

###### Proof 1

By a induction on the type tree $X^{\scriptscriptstyle t}$. The base case when
$X^{\scriptscriptstyle t}$ is the empty tree is immediate. When the game is
defined over a type tree $X\operatorname{::}X^{\scriptscriptstyle f}$, let
$\phi\operatorname{::}\phi^{\scriptscriptstyle f}$ be the associated
quantifier tree, and $x_{0}\operatorname{::}\sigma^{\scriptscriptstyle f}$ the
given strategy. Then, by the induction hypothesis, we have that for every
$x:X$

$q_{x}(\operatorname{spath}(\sigma^{\scriptscriptstyle
f}(x)))=\operatorname{K{-}sequence}(\phi^{\scriptscriptstyle f}(x))(q_{x})$

and hence

$\begin{array}[]{rcl}q(\operatorname{spath}(x_{0}\operatorname{::}\sigma^{\scriptscriptstyle
f}))&=&q_{x_{0}}(\operatorname{spath}(\sigma^{\scriptscriptstyle
f}(x_{0})))\\\\[5.69054pt] &=&\phi(\lambda
x.q_{x}(\operatorname{spath}(\sigma^{\scriptscriptstyle
f}(x))))\\\\[2.84526pt] &\stackrel{{\scriptstyle({\rm IH})}}{{=}}&\phi(\lambda
x.(\operatorname{K{-}sequence}\left(\phi^{\scriptscriptstyle
f}(x)\right))(q_{x}))\\\\[5.69054pt]
&=&\operatorname{K{-}sequence}(\phi\operatorname{::}\phi^{\scriptscriptstyle
f})(q)\end{array}$

using in the first step that $x_{0}\operatorname{::}\sigma^{\scriptscriptstyle
f}$ is an optimal strategy. $\Box$

###  4.1 Selection functions

Let $\operatorname{J}X$ be an abbreviation for the type $(X\to R)\to X$.
Recall the following definitions from [10].

######  Definition 4.5 (Selection functions)

  1. 1.

We call functions of type $\operatorname{J}X$ _selection functions_.

  2. 2.

We say that a selection function $\varepsilon:\operatorname{J}X$ attains a
quantifier $\phi:\operatorname{K}X$ if for all $p\colon X\to R$.

$p(\varepsilon(p))=\phi(p).$

  3. 3.

For each selection function $\varepsilon:\operatorname{J}X$ we can associate a
quantifier $\overline{\varepsilon}:\operatorname{K}X$ defined by

$\overline{\varepsilon}(p)=p(\varepsilon(p))$

so that by definition the selection function $\varepsilon$ attains the
quantifier $\overline{\varepsilon}$.

######  Example 4.6 ($\operatorname{argmin}$ and $\operatorname{argmax}$)

Let $X$ be a finite non-empty type and $R$ a linearly ordered type. Standard
examples of selection functions are

$\operatorname{argmin},\operatorname{argmax}\colon(X\to R)\to X,$

which select an arbitrary point at which the outcome function $q\colon X\to R$
attains its minimum or maximum. We will use them in our Tic-Tac-Toe running
example. It is easy to see that $\operatorname{argmin}$ and
$\operatorname{argmax}$ attain the $\min$ and $\max$ quantifiers,
respectively.

######  Definition 4.7 (Selection function tree)

Given a type tree $X^{\scriptscriptstyle t}$, we define the type of _selection
function trees over $X^{\scriptscriptstyle t}$_ by

$\operatorname{\mathcal{J}}X^{\scriptscriptstyle
t}=\mathrm{structure}(\operatorname{J},X^{\scriptscriptstyle t}).$

We adopt the following conventions:

  1. 1.

The variable $\varepsilon$ ranges over the type $\operatorname{J}X$ of
selection functions.

  2. 2.

The variable $\varepsilon^{\scriptscriptstyle t}$ ranges over the type
$\operatorname{\mathcal{J}}X^{\scriptscriptstyle t}$ of selection function
trees.

  3. 3.

The variable $\varepsilon^{\scriptscriptstyle f}$ ranges over selection
function forests $(x\colon
X)\to\operatorname{\mathcal{J}}(X^{\scriptscriptstyle f}(x))$.

######  Example 4.8 (Tic-Tac-Toe selection function tree)

We associate a selection function tree to the Tic-Tac-Toe type tree of Example
2.2 by alternating the $\operatorname{argmin}$ and $\operatorname{argmax}$
selection functions depending on the level of the tree. Assuming that player X
moves first, the root of the selection function tree is the
$\operatorname{argmin}$ selection function.

######  Definition 4.9 (Attainability on trees)

Given a tree $X^{\scriptscriptstyle t}$, a quantifier tree
$\phi^{\scriptscriptstyle t}:\operatorname{\mathcal{K}}X^{\scriptscriptstyle
t}$ and a selection function tree $\varepsilon^{\scriptscriptstyle
t}:\operatorname{\mathcal{J}}X^{\scriptscriptstyle t}$, we define the relation

> _$\varepsilon^{\scriptscriptstyle t}$ attains $\phi^{\scriptscriptstyle t}$_

by induction on $X^{\scriptscriptstyle t}$ as follows:

  1. 1.

If $X^{\scriptscriptstyle t}$ is the empty tree $[]$ then
$\varepsilon^{\scriptscriptstyle t}$ attains $\phi^{\scriptscriptstyle t}$.

  2. 2.

If the tree $X^{\scriptscriptstyle t}$ is of the form
$X\operatorname{::}X^{\scriptscriptstyle f}$ then
$\varepsilon\operatorname{::}\varepsilon^{\scriptscriptstyle f}$ attains
$\phi\operatorname{::}\phi^{\scriptscriptstyle f}$ if $\varepsilon$ attains
$\phi$ and for each $x:X$ we have that $\varepsilon^{\scriptscriptstyle f}(x)$
attains $\phi^{\scriptscriptstyle f}(x)$.

###### Example 4.10

The selection function tree for Tic-Tac-Toe given in Example 4.8 has been
defined so that it attains the Tic-Tac-Toe quantifier tree of Example 3.4.

######  Definition 4.11 (From selection trees to quantifier trees)

Given any tree $X^{\scriptscriptstyle t}$ and selection function tree
$\varepsilon^{\scriptscriptstyle
t}:\operatorname{\mathcal{J}}X^{\scriptscriptstyle t}$, we define a quantifier
tree

$\overline{\varepsilon^{\scriptscriptstyle
t}}:\operatorname{\mathcal{K}}X^{\scriptscriptstyle t}$

by induction on $X^{\scriptscriptstyle t}$ as follows:

  1. 1.

If $X^{\scriptscriptstyle t}$ is the empty tree $[]$ then
$\varepsilon^{\scriptscriptstyle t}$ is the empty tree and so is
$\overline{\varepsilon^{\scriptscriptstyle t}}$.

  2. 2.

If the tree $X^{\scriptscriptstyle t}$ is of the form
$X\operatorname{::}X^{\scriptscriptstyle f}$ then the selection function tree
$\varepsilon^{\scriptscriptstyle t}$ is of the form
$\varepsilon\operatorname{::}\varepsilon^{\scriptscriptstyle f}$ and
$\overline{\varepsilon^{\scriptscriptstyle t}}$ is the quantifier tree
$\overline{\varepsilon}\operatorname{::}(\lambda
x.\overline{\varepsilon^{\scriptscriptstyle f}(x)})$.

A simple proof by induction shows that $\varepsilon^{\scriptscriptstyle t}$
attains $\phi^{\scriptscriptstyle t}$ if and only if
$\overline{\varepsilon^{\scriptscriptstyle t}}=\phi^{\scriptscriptstyle t}$.

###### Example 4.12

It is easy to see that if $\varepsilon^{\scriptscriptstyle t}$ is the argmin-
argmax selection function tree for Tic-Tac-Toe given in Example 4.8 then
$\overline{\varepsilon^{\scriptscriptstyle t}}$ is the min-max quantifier tree
of Example 3.4.

######  Definition 4.13 (Dependent product of selection functions [10])

For any selection function

$\varepsilon:\operatorname{J}X$

on a type $X$, any a family $Y$ of types indexed by $X$, and any family

$\delta\colon(x:X)\to\operatorname{J}(Y(x))$

of selection functions, we define a selection function

$\varepsilon\operatorname{\otimes^{\tiny
J}}\delta:\operatorname{J}((x:X)\times Y(x))$

by

$(\varepsilon\operatorname{\otimes^{\tiny J}}\delta)(q)=(x_{0},\nu(x_{0}))$

where

$\displaystyle\nu(x)$ $\displaystyle=$ $\displaystyle\delta(x)(q_{x})$
$\displaystyle x_{0}$ $\displaystyle=$ $\displaystyle\varepsilon(\lambda
x.q_{x}(\nu(x)).$

We can also adapt the iterated product of selection functions [10] to
selection function trees as follows.

######  Definition 4.14 (J-sequence)

To each selection function tree $\varepsilon^{\scriptscriptstyle
t}:\operatorname{\mathcal{J}}X^{\scriptscriptstyle t}$ we associate a single
selection function

$\operatorname{J{-}sequence}(\varepsilon^{\scriptscriptstyle
t}):\operatorname{J}(\operatorname{\mathrm{Path}}X^{\scriptscriptstyle t})$

on the type of paths of the tree $X^{\scriptscriptstyle t}$ by induction as
follows.

  1. 1.

To the empty tree $[]:\operatorname{Tree}$ we associate the selection function
$\lambda q.\operatorname{\langle\rangle}$ of type
$\operatorname{J}(\operatorname{\mathrm{Path}}\,[])$.

  2. 2.

To a selection function tree of the form
$\varepsilon\operatorname{::}\varepsilon^{\scriptscriptstyle f}$ we associate
the selection function $\varepsilon\operatorname{\otimes^{\tiny J}}(\lambda
x.\operatorname{J{-}sequence}\varepsilon^{\scriptscriptstyle f}(x))$.

Note that, by Definition 4.13, we have

$(\varepsilon\operatorname{\otimes^{\tiny J}}(\lambda
x.\operatorname{J{-}sequence}\varepsilon^{\scriptscriptstyle
f}(x)))(q)=x_{0}\operatorname{::}\nu(x_{0})$

where

$\displaystyle\nu(x)$ $\displaystyle=$
$\displaystyle(\operatorname{J{-}sequence}\varepsilon^{\scriptscriptstyle
f}(x))(q_{x})$ $\displaystyle x_{0}$ $\displaystyle=$
$\displaystyle\varepsilon(\lambda x.q_{x}(\nu(x)).$

###### Remark 4.15

Notice the similarity of Definitions 3.7 and 4.14. They can be unified in a
single definition that assumes that the structure is the functor of a strong
monad, which $\operatorname{K}$ and $\operatorname{J}$ are. Moreover, this is
also the case for Definitions 3.5 and 4.13. Although they look very different,
they are both instances of a general definition for strong monads. For any
strong monad $T$ we can define

$t\otimes^{T}f=(\lambda x.T(\lambda y.(x,y))^{\dagger}(f(x)))(t)$

for any $t:TX$ and $f:(x:X)\to T(Yx)$, where $(-)^{\dagger}$ is the Kleisli
extension operator. The definition of the strong monads $K$ and $J$ can be
found in [10], [9] or [11] (and also in our Agda formalisation discussed in
Section 6).

###  4.2 Calculating optimal strategies

Finally, let us now show how the $\operatorname{J}$-sequence construction can
be used to calculate optimal strategies in games based on dependent type
trees.

######  Definition 4.16 (Strategy of selection tree)

Given tree $X^{\scriptscriptstyle t}$, a selection function tree
$\varepsilon^{\scriptscriptstyle
t}:\operatorname{\mathcal{J}}X^{\scriptscriptstyle t}$ and an outcome function
$q\colon\operatorname{\mathrm{Path}}X^{\scriptscriptstyle t}\to R$, we define
a strategy

$\operatorname{strategy}(\varepsilon^{\scriptscriptstyle
t},q):\operatorname{Strategy}X^{\scriptscriptstyle t}$

by induction as follows:

  1. 1.

When $X^{\scriptscriptstyle t}$ is the empty tree then
$\operatorname{strategy}(\varepsilon^{\scriptscriptstyle t},q)$ is the empty
strategy.

  2. 2.

When $X^{\scriptscriptstyle t}$ is of the form
$X\operatorname{::}X^{\scriptscriptstyle f}$ and
$\varepsilon^{\scriptscriptstyle
t}=\varepsilon\operatorname{::}\varepsilon^{\scriptscriptstyle f}$ then we
define

$\operatorname{strategy}(\varepsilon^{\scriptscriptstyle
t},q)=(x_{0},\sigma^{\scriptscriptstyle f})$

where

$\displaystyle x_{0}$ $\displaystyle=$
$\displaystyle\operatorname{head}(\operatorname{J{-}sequence}(\varepsilon^{\scriptscriptstyle
t})(q)),$ $\displaystyle\sigma^{\scriptscriptstyle f}(x)$ $\displaystyle=$
$\displaystyle\operatorname{strategy}(\varepsilon^{\scriptscriptstyle
f}(x),q_{x}).$

######  Lemma 4.17 (Main lemma)

Given a tree $X^{\scriptscriptstyle t}$, a selection function tree
$\varepsilon^{\scriptscriptstyle
t}:\operatorname{\mathcal{J}}X^{\scriptscriptstyle t}$ and an outcome function
$q\colon\operatorname{\mathrm{Path}}X^{\scriptscriptstyle t}\to R$, we have

$\operatorname{spath}(\operatorname{strategy}(\varepsilon^{\scriptscriptstyle
t},q))=\operatorname{J{-}sequence}(\varepsilon^{\scriptscriptstyle t})(q).$

###### Proof 2

By induction on $X^{\scriptscriptstyle t}$. When $X^{\scriptscriptstyle t}$ is
the empty tree, the result is immediate. Let $X^{\scriptscriptstyle
t}=X\operatorname{::}X^{\scriptscriptstyle f}$ and
$\varepsilon^{\scriptscriptstyle
t}=\varepsilon\operatorname{::}\varepsilon^{\scriptscriptstyle f}$ and assume,
for each $x:X$, the induction hypothesis holds

$\operatorname{spath}(\operatorname{strategy}(\varepsilon^{\scriptscriptstyle
f}(x),q_{x}))=\operatorname{J{-}sequence}(\varepsilon^{\scriptscriptstyle
f}(x))(q_{x})$

Then

$\begin{array}[]{rcl}\operatorname{spath}(\operatorname{strategy}(\varepsilon^{\scriptscriptstyle
t},q))&=&\operatorname{spath}(x_{0}\operatorname{::}\sigma^{\scriptscriptstyle
f})\\\\[5.69054pt]
&=&x_{0}\operatorname{::}\operatorname{spath}(\sigma^{\scriptscriptstyle
f}(x_{0}))\\\\[2.84526pt]
&\stackrel{{\scriptstyle(\text{IH})}}{{=}}&x_{0}\operatorname{::}\nu(x_{0})\\\\[5.69054pt]
&=&\operatorname{J{-}sequence}(\varepsilon^{\scriptscriptstyle
t})(q)\end{array}$

where

$\displaystyle\nu(x)$ $\displaystyle=$
$\displaystyle\operatorname{J{-}sequence}(\varepsilon^{\scriptscriptstyle
f}(x))(q_{x})$ $\displaystyle x_{0}$ $\displaystyle=$
$\displaystyle\varepsilon(\lambda x.q_{x}(\nu(x)))$
$\displaystyle\sigma^{\scriptscriptstyle f}(x)$ $\displaystyle=$
$\displaystyle\operatorname{strategy}(\varepsilon^{\scriptscriptstyle
f}(x),q_{x}),$

which concludes the proof. $\Box$

######  Lemma 4.18 (Selection strategy lemma)

Given a type tree $X^{\scriptscriptstyle t}$, an outcome function
$q\colon\operatorname{\mathrm{Path}}X^{\scriptscriptstyle t}\to R$, and a
selection function tree $\varepsilon^{\scriptscriptstyle
t}:\operatorname{\mathcal{J}}X^{\scriptscriptstyle t}$,

$\operatorname{strategy}(\varepsilon^{\scriptscriptstyle
t},q):\operatorname{Strategy}X^{\scriptscriptstyle t}$

is optimal for the game $(X^{\scriptscriptstyle
t},R,q,\overline{\varepsilon^{\scriptscriptstyle t}})$.

###### Proof 3

By induction on the tree $X^{\scriptscriptstyle t}$. When
$X^{\scriptscriptstyle t}$ is the empty tree, the result is again immediate.
If $X^{\scriptscriptstyle t}=X\operatorname{::}X^{\scriptscriptstyle f}$ and
$\varepsilon^{\scriptscriptstyle
t}=\varepsilon\operatorname{::}\varepsilon^{\scriptscriptstyle f}$, recall
that $\operatorname{strategy}(\varepsilon^{\scriptscriptstyle
t},q)=x_{0}\operatorname{::}\sigma^{\scriptscriptstyle f}$ where

$\displaystyle x_{0}$ $\displaystyle=$ $\displaystyle\varepsilon(\lambda
x.q_{x}(\operatorname{J{-}sequence}(\varepsilon^{\scriptscriptstyle
f}(x))(q_{x}))),$ $\displaystyle\sigma^{\scriptscriptstyle f}(x)$
$\displaystyle=$
$\displaystyle\operatorname{strategy}(\varepsilon^{\scriptscriptstyle
f}(x),q_{x}).$

By induction hypothesis we have that, for all $x:X$, the strategy
$\sigma^{\scriptscriptstyle f}(x)$ is optimal for the subgame

$(X^{\scriptscriptstyle
f}(x),R,q_{x},\overline{\varepsilon^{\scriptscriptstyle f}(x)})$

and since

$x_{0}=\varepsilon(\lambda
x.q_{x}(\operatorname{spath}(\operatorname{strategy}(\varepsilon^{\scriptscriptstyle
f}(x),q_{x})))),$

by the Main lemma 4.17, we indeed have

$q(x_{0}\operatorname{::}\operatorname{spath}(\sigma^{\scriptscriptstyle
f}(x_{0})))=\overline{\varepsilon}(\lambda
x.q(x\operatorname{::}\operatorname{spath}(\sigma^{\scriptscriptstyle
f}(x)))),$

which concludes the proof. $\Box$

######  Theorem 4.19 (Selection strategy theorem)

If a selection function tree $\varepsilon^{\scriptscriptstyle
t}\colon\operatorname{\mathcal{J}}X^{\scriptscriptstyle t}$ attains a
quantifier-free $\phi^{\scriptscriptstyle
t}\colon\operatorname{\mathcal{K}}X^{\scriptscriptstyle t}$ then, for any
outcome function $q\colon\operatorname{\mathrm{Path}}X^{\scriptscriptstyle
t}\to R$,

$\operatorname{strategy}(\varepsilon^{\scriptscriptstyle t},q)$

is optimal for the game $(X^{\scriptscriptstyle
t},R,q,\phi^{\scriptscriptstyle t})$.

###### Proof 4

Since $\overline{\varepsilon^{\scriptscriptstyle t}}=\phi^{\scriptscriptstyle
t}$ when $\varepsilon^{\scriptscriptstyle t}$ attains
$\phi^{\scriptscriptstyle t}$, the theorem is an immediate consequence of the
Selection strategy lemma 4.18.

######  Example 4.20 (Tic-Tac-Toe optimal strategy)

Since the quantifier tree $\phi^{\scriptscriptstyle t}$ in the Tic-Tac-Toe
game $(X^{\scriptscriptstyle t},R,q,\phi^{\scriptscriptstyle t})$ (Example
3.9) is attained by a selection function tree $\varepsilon^{\scriptscriptstyle
t}$ (Definition 4.8), the theorem above shows that
$\operatorname{strategy}(\varepsilon^{\scriptscriptstyle t},q)$ is optimal.

##  5 Discussion of dependent type trees

Aczel [2] considers a type $\operatorname{Tree}_{A}$ similar to our type
$\operatorname{Tree}$, but without our leaf constructor $[]$, for the purpose
of modelling CZF. The type $\operatorname{Tree}_{A}$ consists of well-founded
type trees where leaves are of the form
$X\operatorname{::}X^{\scriptscriptstyle f}$ with $X$ empty and
$X^{\scriptscriptstyle f}$ the unique function on $X$. In our definition,
nodes $X$ with $X$ empty are allowed in principle. However, as soon as there
is a strategy for a type tree $X^{\scriptscriptstyle t}:\operatorname{Tree}$,
the internal nodes of $X^{\scriptscriptstyle t}$ must all be inhabited.

It is not hard to see that the subtype of $\operatorname{Tree}$ consisting of
the trees whose internal nodes are all inhabited is in bijection with the
subtype of $\operatorname{Tree}_{A}$ consisting of trees whose internal nodes
are all decidable (that is, either empty or inhabited). So we can work with
the type $\operatorname{Tree}_{A}$ instead. But, in this case, we need to
slightly modify all our constructions on trees. For example, with our
definition of path, the type of paths over a tree $X^{\scriptscriptstyle
t}:\operatorname{Tree}$ is empty if $X^{\scriptscriptstyle t}$ has no leaves
of the form $[]$. However, we can define a correct notion of path for Aczel
trees by

$\operatorname{\mathrm{Path}}(X\operatorname{::}X^{\scriptscriptstyle f})={\rm
is{-}empty}(X)+((x:X)\times\operatorname{\mathrm{Path}}(X^{\scriptscriptstyle
f}(x)).$

This definition is correct in that paths in our original sense correspond to
paths in this modified sense along the bijection discussed above. All other
definitions have to be modified in a similar way, by treating the base case
differently.

Another observation is that empty internal nodes can be pruned away with an
idempotent map
$\operatorname{prune}:\operatorname{Tree}\to\operatorname{Tree}$ such that any
tree $X^{\scriptscriptstyle t}$ has the same paths as the tree
$\operatorname{prune}(X^{\scriptscriptstyle t})$, and this can be done without
assuming that the internal nodes of $X^{\scriptscriptstyle t}$ are decidable.
Moreover, as soon as there is at least one path in the tree
$X^{\scriptscriptstyle t}$, all internal nodes of tree
$\operatorname{prune}(X^{\scriptscriptstyle t})$ are inhabited.

An extended version of this discussion, with full technical details, is
formalised in Agda (see the next section).

##  6 Proofs and Programs in Agda

A second contribution of the present work is that all the definitions,
constructions, theorems, lemmas, proofs and examples presented above have been
implemented and computer-verified in Agda [16].

As Agda adopts a constructive foundation, the function
$\operatorname{strategy}(\varepsilon^{\scriptscriptstyle t},q)$, which defines
strategies from selection trees $\varepsilon^{\scriptscriptstyle t}$ and
outcome functions $q$, is automatically a computer program that can be used to
calculate optimal strategies in concrete games. In particular, we also
implemented Tic-Tac-Toe as outlined in the above examples.

The Agda development discussed above [16] is organised in the following files:

  1. 1.

_TypeTrees._ This defines dependent type trees and basic concepts for them,
including the general definition of adding “structure” to a type tree.

  2. 2.

_FiniteHistoryDependent_. This implements this paper, excluding the examples.
We took care of presenting the material in the same order as in this paper,
and of using the same labels for theorems, definitions, etc.

  3. 3.

There are three _TicTacToe_ files, which implement our running example in
different ways. The first one is the shortest and most transparent, but also
the most inefficient, while the other two try to sacrifice clarity for
efficiency.

  4. 4.

_Constructor_. This gives an alternative construction of games, not discussed
in this paper, and is used in the more efficient versions of Tic-Tac-Toe.

  5. 5.

_Discussion_. This formalises an extended version of the discussion of Section
5.

##  7 Further work

The work presented here is part of a project to extend the theory of higher-
order games so as to model different types of players and strategies. Our aim
is to make use of the combination of the selection monad with other monads, as
in [15], leading to games and strategies parametrised by a monadic structure.
In particular, by making use of a probability monad, we intend to model
suboptimal or “irrational” players in future work.

## Acknowledgements

We thank the anonymous referee for a number of helpful comments and questions.
We would also like to thank Ohad Kammar for discussions. He also implemented
[19] part of the above in the dependently typed programming language Idris
[6].

## References

  * [1] Martín Abadi and Gordon Plotkin.  Smart choices and the selection monad.  Log. Methods Comput. Sci., 19(2):Paper No. 3, 63, 2023.
  * [2] P. Aczel.  The type theoretic interpretation of constructive set theory.  In Angus Macintyre, Leszek Pacholski, and Jeff Paris, editors, Logic Colloquium ’77, volume 96 of Studies in Logic and the Foundations of Mathematics, pages 55–66. Elsevier, 1978.
  * [3] Agda community.  Agda wiki.  https://wiki.portal.chalmers.se/agda/pmwiki.php.
  * [4] U. Berger.  Totale Objekte und Mengen in der Bereichstheorie.  PhD thesis, Mathematisches Institut der Universität München, 1990.
  * [5] Ana Bove and Peter Dybjer.  Dependent types at work.  Lecture Notes in Computer Science, 5520:57–99, 2009.
  * [6] Edwin Brady.  Idris, a general-purpose dependently typed programming language: Design and implementation.  Journal of Functional Programming, 23:552–593, 9 2013.
  * [7] M.H. Escardó.  Exhaustible sets in higher-type computation.  Logical Methods in Computer Science, 4(3):paper 4, 2008.
  * [8] M.H. Escardó and P. Oliva.  Computational interpretations of analysis via products of selection functions.  In Programs, proofs, processes, volume 6158 of Lecture Notes in Comput. Sci., pages 141–150. Springer, Berlin, 2010.
  * [9] M.H. Escardó and P. Oliva.  The Peirce translation and the double negation shift.  In Programs, proofs, processes, volume 6158 of Lecture Notes in Comput. Sci., pages 151–161. Springer, Berlin, 2010.
  * [10] M.H. Escardó and P. Oliva.  Selection functions, bar recursion and backward induction.  Math. Structures Comput. Sci., 20(2):127–168, 2010.
  * [11] M.H. Escardó and P. Oliva.  What sequential games, the tychonoff theorem and the double-negation shift have in common.  In Proceedings of the Third ACM SIGPLAN Workshop on Mathematically Structured Functional Programming, MSFP ’10, page 21–32, New York, NY, USA, 2010. Association for Computing Machinery.
  * [12] M.H. Escardó and P. Oliva.  Sequential games and optimal strategies.  Royal Society Proceedings A, 467:1519–1545, 2011.
  * [13] M.H. Escardó and P. Oliva.  Computing Nash equilibria of unbounded games.  In Proceedings of The Turing Centenary Conference, volume 10, pages 53–65. EPiC Series, Manchester, 2012.
  * [14] M.H. Escardó and P. Oliva.  Bar recursion and products of selection functions.  The Journal of Symbolic Logic, 80(1):1–28, 2015.
  * [15] M.H. Escardó and P. Oliva.  The Herbrand functional interpretation of the double negation shift.  The Journal of Symbolic Logic, 82(2):590 – 607, 2017.
  * [16] M.H. Escardó and P. Oliva.  TypeTopology - Games.  https://www.cs.bham.ac.uk/~mhe/TypeTopology/Games.index.html, 2021\.  Agda development at https://github.com/martinescardo/TypeTopology/tree/9eb7ad5322d/source/Games.
  * [17] Neil Ghani, Jules Hedges, Viktor Winschel, and Philipp Zahn.  Compositional game theory.  In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’18, page 472–481, New York, NY, USA, 2018. Association for Computing Machinery.
  * [18] Johannes Hartmann and Jeremy Gibbons.  Algorithm design with the selection monad.  In Wouter Swierstra and Nicolas Wu, editors, Trends in Functional Programming, volume 13401 of LNCS, pages 126–143, 2022.
  * [19] O. Kammar.  Games, 2022.  Idris development at https://github.com/ohad/games.
  * [20] G. Leversha.  Formal Systems for Constructive Mathematics.  PhD thesis, University of Manchester, Department of Pure and Applied Mathematics, 1976.
  * [21] Thomas Powell.  The equivalence of bar recursion and open recursion.  Ann. Pure Appl. Logic, 165(11):1727–1754, 2014.
  * [22] Thomas Powell.  Parametrized bar recursion: a unifying framework for realizability interpretations of classical dependent choice.  J. Logic Comput., 29(4):519–554, 2019.
  * [23] The Univalent Foundations Program.  Homotopy Type Theory: Univalent Foundations of Mathematics.  https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.


We recall universal approximation of graph-level functions in probability
(Definition 3.1):

######  Definition 3.1.

We say $X_{\theta}(\cdot)$ is a universal approximator of graph-level
functions in probability if, for all invariant functions
$\phi:\mathbb{G}_{n}\to\mathbb{R}$ for a given $n\geq 1$, and
$\forall\epsilon,\delta>0$, there exist choices of length $l$ of the random
walk and network parameters $\theta$ such that the following holds:

$\displaystyle\mathrm{Prob}[|\phi(G)-X_{\theta}(G)|<\epsilon]>1-\delta,\quad\forall
G\in\mathbb{G}_{n}.$ (83)

We remark that a random walk neural network $X_{\theta}(\cdot)$ is composed of
a random walk algorithm, a recording function $q:(v_{0}\to\cdots\to
v_{l},G)\mapsto\mathbf{z}$, and a reader neural network
$f_{\theta}:\mathbf{z}\mapsto\hat{\mathbf{y}}\in\mathbb{R}$.

Intuitively, if the record $\mathbf{z}$ of the random walk always provides
complete information of the input graph $G$, we may invoke universal
approximation of $f_{\theta}$ to always obtain
$|\phi(G)-f_{\theta}(\mathbf{z})|<\epsilon$, and thus
$|\phi(G)-X_{\theta}(G)|<\epsilon$. However, this is not always true as the
random walk may e.g. fail to visit some vertices of $G$, in which case the
record $\mathbf{z}$ would be incomplete. As we show below, this uncertainty
leads to the probabilistic bound $>1-\delta$ of the approximation.

Let us denote the collection of all possible random walk records as
$\\{\mathbf{z}\\}\coloneq\mathrm{Range}(q)$, and consider a decoding function
$\psi:\\{\mathbf{z}\\}\to\mathbb{G}_{n}$ that takes the record
$\mathbf{z}\coloneq q(v_{0}\to\cdots\to v_{l},G)$ of a given random walk
$v_{[\cdot]}$ and outputs the graph $\psi(\mathbf{z})\in\mathbb{G}_{n}$
composed of all recorded vertices
$V(H)\coloneq\\{\mathrm{id}(v_{t}):v_{t}\in\\{v_{0},...,v_{l}\\}\\}$ and all
recorded edges $E(H)\subset V(H)\times V(H)$. We show the following lemma:

######  Lemma A.6.

Let $G_{\mathbf{z}}$ be the subgraph of $G$ whose vertices and edges are
recorded by $\mathbf{z}$. Then the graph $\psi(\mathbf{z})$ decoded from the
record $\mathbf{z}$ is isomorphic to $G_{\mathbf{z}}$ through the namespace
$\mathrm{id}(\cdot)$:

$\displaystyle G_{\mathbf{z}}\overset{\mathrm{id}}{\simeq}\psi(\mathbf{z}).$
(84)

Furthermore, the decoded graph $\psi(\mathbf{z})$ reconstructs $G$ up to
isomorphism, that is,

$\displaystyle G\overset{\mathrm{id}}{\simeq}\psi(\mathbf{z}),$ (85)

if the recording function $q(\cdot)$ and the random walk $v_{[\cdot]}$
satisfies either of the following:

  * •

$q(\cdot)$ uses anonymization, and $v_{[\cdot]}$ has traversed all edges of
$G$.

  * •

$q(\cdot)$ uses anonymization and named neighborhoods, and $v_{[\cdot]}$ has
visited all vertices of $G$.

###### Proof.

Equation (84) is straightforward from the fact that the namespace
$\mathrm{id}(\cdot)$ defines a bijection from $V(G_{\mathbf{z}})$ to
$[|V(G_{\mathbf{z}})|]$, and the recording function uses names
$\mathrm{id}(v_{t})$ to record vertices and edges. Equation (85) is satisfied
when all vertices and edges of $G$ have been recorded, i.e.
$G_{\mathbf{z}}=G$, which is possible either when the random walk has
traversed all edges of $G$, or when it has traversed all vertices of $G$ and
named neighborhoods are used to record the induced subgraph $G[V(G)]=G$. ∎

We further remark Markov’s inequality for any nonnegative random variable $T$
and $a>0$:

$\displaystyle\mathrm{Prob}[T\geq a]\leq\frac{\mathbb{E}[T]}{a}.$ (86)

We are now ready to prove Theorem 3.2.

######  Theorem 3.2.

A random walk neural network $X_{\theta}(\cdot)$ with a sufficiently powerful
$f_{\theta}$ is a universal approximator of graph-level functions in
probability (Definition 3.1) if it satisfies either of the below:

  * •

It uses anonymization to record random walks of lengths $l>C_{E}(G)/\delta$.

  * •

It uses anonymization and named neighborhoods to record walks of lengths
$l>C_{V}(G)/\delta$.

###### Proof.

Instead of directly approximating the target function
$\phi:\mathbb{G}_{n}\to\mathbb{R}$, it is convenient to define a proxy target
function on random walk records $\phi^{\prime}:\\{\mathbf{z}\\}\to\mathbb{R}$
where $\\{\mathbf{z}\\}\coloneq\mathrm{Range}(q)$ as follows:

$\displaystyle\phi^{\prime}\coloneq\phi\circ\psi,$ (87)

where $\psi:\\{\mathbf{z}\\}\to\mathbb{G}_{n}$ is the decoding function of
walk records. Then, for a given $\mathbf{z}$, we have:

$\displaystyle
G\simeq\psi(\mathbf{z})\quad\Longrightarrow\quad\phi(G)=\phi^{\prime}(\mathbf{z}),$
(88)

which is because $\phi$ is an invariant function, so
$\phi(G)=\phi(\psi(\mathbf{z}))=\phi\circ\psi(\mathbf{z})=\phi^{\prime}(\mathbf{z})$.
Then we have:

$\displaystyle\mathrm{Prob}[G\simeq\psi(\mathbf{z})]\leq\mathrm{Prob}[|\phi(G)-\phi^{\prime}(\mathbf{z})|=0].$
(89)

We now invoke universality of $f_{\theta}$ to approximate $\phi^{\prime}$. If
$f_{\theta}$ is a universal approximator of functions on its domain
$\\{\mathbf{z}\\}\coloneq\mathrm{Range}(q)$, for any $\epsilon>0$ there exists
a choice of $\theta$ such that the below holds:

$\displaystyle|\phi^{\prime}(\mathbf{z})-f_{\theta}(\mathbf{z})|<\epsilon,\quad\forall\mathbf{z}\in\mathrm{Range}(q).$
(90)

Combining Equations (89) and (90), we have:

$\displaystyle\mathrm{Prob}[G\simeq\psi(\mathbf{z})]\leq\mathrm{Prob}[|\phi(G)-\phi^{\prime}(\mathbf{z})|+|\phi^{\prime}(\mathbf{z})-f_{\theta}(\mathbf{z})|<\epsilon].$
(91)

We remark triangle inequality of distances on $\mathbb{R}$, for a given
$\mathbf{z}$:

$\displaystyle|\phi(G)-f_{\theta}(\mathbf{z})|\leq|\phi(G)-\phi^{\prime}(\mathbf{z})|+|\phi^{\prime}(\mathbf{z})-f_{\theta}(\mathbf{z})|,$
(92)

which implies, for a given $\mathbf{z}$:

$\displaystyle|\phi(G)-\phi^{\prime}(\mathbf{z})|+|\phi^{\prime}(\mathbf{z})-f_{\theta}(\mathbf{z})|<\epsilon\quad\Longrightarrow\quad|\phi(G)-f_{\theta}(\mathbf{z})|<\epsilon,$
(93)

and hence:

$\displaystyle\mathrm{Prob}[|\phi(G)-\phi^{\prime}(\mathbf{z})|+|\phi^{\prime}(\mathbf{z})-f_{\theta}(\mathbf{z})|<\epsilon]\leq\mathrm{Prob}[|\phi(G)-f_{\theta}(\mathbf{z})|<\epsilon].$
(94)

Combining Equations (91) and (94), we have:

$\displaystyle\mathrm{Prob}[|\phi(G)-f_{\theta}(\mathbf{z})|<\epsilon]\geq\mathrm{Prob}[G\simeq\psi(\mathbf{z})],$
(95)

which can be written as follows:

$\displaystyle\mathrm{Prob}[|\phi(G)-X_{\theta}(G)|<\epsilon]\geq\mathrm{Prob}[G\simeq\psi(\mathbf{z})].$
(96)

We now consider the probability of the event $G\simeq\psi(\mathbf{z})$ based
on Lemma A.6. We first consider the case where the recording function
$q(\cdot)$ uses anonymization. In this case, $G\simeq\psi(\mathbf{z})$ is
achieved if the random walk of length $l$ has traversed all edges of $G$. Let
$T_{E}(G,v_{0})$ be the number of steps that a random walk starting at $v_{0}$
takes until traversing all edges of $G$. Since the edge cover time $C_{E}(G)$
is its expectation taken at the worst possible starting vertex (Equation
(17)), we have the following:

$\displaystyle\mathbb{E}[T_{E}(G,v_{0})]\leq C_{E}(G),\quad\forall v_{0}\in
V(G),$ (97)

which leads to the following from Markov’s inequality (Equation (86)):

$\displaystyle\mathrm{Prob}[T_{E}(G,v_{0})<l]\geq
1-\frac{\mathbb{E}[T_{E}(G)]}{l}\geq 1-\frac{C_{E}(G)}{l}.$ (98)

For a given random walk $v_{0}\to\cdots\to v_{l}$ and its record $\mathbf{z}$,
the following holds:

$\displaystyle T_{E}(G,v_{0})<l\quad\Longrightarrow\quad
G\simeq\psi(\mathbf{z}),$ (99)

which implies the following:

$\displaystyle\mathrm{Prob}[T_{E}(G,v_{0})<l]\leq\mathrm{Prob}[G\simeq\psi(\mathbf{z})].$
(100)

Combining Equations (96), (98), and (100), we have:

$\displaystyle\mathrm{Prob}[|\phi(G)-X_{\theta}(G)|<\epsilon]\geq
1-\frac{C_{E}(G)}{l}.$ (101)

Therefore, for any $\delta>0$, if we choose $l>C_{E}(G)/\delta$ we would have
the following:

$\displaystyle\mathrm{Prob}[|\phi(G)-X_{\theta}(G)|<\epsilon]>1-\delta.$ (102)

This completes the proof for anonymization. The proof is identical for the
recording function that uses anonymization and named neighborhoods, except
that the edge cover time is changed to the cover time $C_{V}(G)$ (Equation
(16)). This is because neighborhood recording automatically records the
induced subgraph of visited vertices, thus visiting all vertices implies
recording all edges, $G[V(G)]=G$. ∎

####  A.4.8 Proof of Theorem 3.4 (Section 3.1)

######  Theorem 3.4.

A random walk neural network $X_{\theta}(\cdot)$ with a sufficiently powerful
$f_{\theta}$ and any nonzero restart probability $\alpha$ or restart period
$k\geq r+1$ is a universal approximator of vertex-level functions in
probability (Definition 3.3) if it satisfies either of the below for all
$B_{r}(v)\in\mathbb{B}_{r}$:

  * •

It uses anonymization to record random walks of lengths
$l>C_{E}(B_{r}(v))/\delta$.

  * •

It uses anonymization and named neighborhoods to record walks of lengths
$l>C_{V}(B_{r}(v))/\delta$.

###### Proof.

The proof is almost identical to Theorem 3.2, except $G\in\mathbb{G}_{n}$ are
substituted by $B_{r}(v)\in\mathbb{B}_{r}$, and the decoding function
$\psi:\\{\mathbf{z}\\}\to\mathbb{B}_{r}$ is defined to ignore all recorded
vertices $\mathrm{id}(x)$ whose shortest path distance from the starting
vertex $\mathrm{id}(v)=\mathrm{id}(v_{0})=1$ exceeds $r$. The latter is
necessary to restrict the range of the decoding function $\psi$ to
$\mathbb{B}_{r}$. In addition, any nonzero restart probability $\alpha$ or
restart period $k\geq r+1$ is sufficient to make the cover times
$C_{E}(B_{r}(v))$ and $C_{V}(B_{r}(v))$ finite (Theorem 2.5), thereby
guaranteeing the existence of a finite choice of $l$. ∎

####  A.4.9 Proof of Theorem 3.5 (Section 3.2)

######  Theorem 3.5.

The simple random walk neural network outputs
$\mathbf{h}^{(l)}\to\mathbf{x}^{\top}\boldsymbol{\pi}$ as $l\to\infty$.

###### Proof.

Since $G$ is connected and non-bipartite, the uniform random walk on it
defines an ergodic Markov chain with a unique stationary distribution
$\boldsymbol{\pi}$. The limiting frequency of visits on each vertex $v$ is
precisely the stationary probability $\boldsymbol{\pi}_{v}$. Since the model
reads $\mathbf{x}_{v_{0}}\to\cdots\to\mathbf{x}_{v_{l}}$ by average pooling,
the output is given by weighted mean
$\sum_{v}\boldsymbol{\pi}_{v}\mathbf{x}_{v}$ which is
$\mathbf{x}^{\top}\boldsymbol{\pi}$. ∎

####  A.4.10 Proof of Theorem 3.6 (Section 3.2)

######  Theorem 3.6.

Let $\mathbf{h}_{u}^{(l)}$ be output of the simple random walk neural network
queried with $u$. Then:

$\displaystyle\mathbb{E}\left[\left|\frac{\partial\mathbf{h}_{u}^{(l)}}{\partial\mathbf{x}_{v}}\right|\right]=\frac{1}{l+1}\left[\sum_{t=0}^{l}P^{t}\right]_{uv}\to\boldsymbol{\pi}_{v}\quad\text{as}\quad
l\to\infty.$ (103)

###### Proof.

Since the model reads $\mathbf{x}_{v_{0}}\to\cdots\to\mathbf{x}_{v_{l}}$ by
average pooling, the feature Jacobian
$|\partial\mathbf{h}_{u}^{(l)}/\partial\mathbf{x}_{v}|$ is given as number of
visits to the vertex $v$ in the random walk $v_{0}\to\cdots\to v_{l}$ starting
at $v_{0}=u$, divided by length $l+1$. Let us denote the expected number of
these visits by $J(u,v,l)$. Let $\mathbbm{1}_{v_{t}=v}$ be the indicator
function that equals $1$ if $v_{t}=v$ and $0$ otherwise. Then we can write
$J(u,v,l)$ as:

$\displaystyle J(u,v,l)$
$\displaystyle=\mathbb{E}\left[\sum_{t=0}^{l}\mathbbm{1}_{v_{t}=v}|v_{0}=u\right],$
$\displaystyle=\sum_{t=0}^{l}\mathbb{E}[\mathbbm{1}_{v_{t}=v}|v_{0}=u].$ (104)

We have used linearity of expectations for the second equality.
$\mathbb{E}[\mathbbm{1}_{v_{t}=v}|v_{0}=u]$ is the probability of being at $v$
at step $t$ given that the walk started at $u$. This probability is precisely
$[P^{t}]_{uv}$. Therefore:

$\displaystyle
J(u,v,l)=\sum_{t=0}^{l}\left[P^{t}\right]_{uv}=\left[\sum_{t=0}^{l}P^{t}\right]_{uv},$
(105)

which gives the equality in Equation (103). Furthermore, since $G$ is
connected and non-bipartite, the uniform random walk on it defines an ergodic
Markov chain with a unique stationary distribution $\boldsymbol{\pi}$. The
limiting frequency of visits on vertex $v$ is precisely the stationary
probability $\boldsymbol{\pi}_{v}$, which gives the convergence in Equation
(103). This completes the proof. ∎


# Encoding time and energy model for SVT-AV1 based on video complexity

###### Abstract

The share of online video traffic in global carbon dioxide emissions is
growing steadily. To comply with the demand for video media, dedicated
compression techniques are continuously optimized, but at the expense of
increasingly higher computational demands and thus rising energy consumption
at the video encoder side. In order to find the best trade-off between
compression and energy consumption, modeling encoding energy for a wide range
of encoding parameters is crucial. We propose an encoding time and energy
model for SVT-AV1 based on empirical relations between the encoding time and
video parameters as well as encoder configurations. Furthermore, we model the
influence of video content by established content descriptors such as spatial
and temporal information. We then use the predicted encoding time to estimate
the required energy demand and achieve a prediction error of 19.6% for
encoding time and 20.9% for encoding energy.

Index Terms— SVT-AV1, encoding energy, encoding time, video complexity

##  1 Introduction

Research activities in video compression have witnessed remarkable growth in
response to the rising demand for high-quality video content across diverse
digital platforms such as Netflix and TikTok. As video-on-demand services,
social media networks, and video-conferencing applications continue to shape
our digital interactions, the optimization of video encoding has become
important not only in terms of compression efficiency but also regarding their
energy consumption [1]. In 2015, the global greenhouse gas emissions caused by
video streaming were $1.3\%$ [2] and are expected to increase further due to
increased video traffic [3]. To comply with the growing demand for high-
resolution content, advances in video codecs focus on optimizing compression
performance, i.e. reducing the size of the encoded bitstream while maintaining
visual quality of the reconstructed video at the end-user’s device. The
emerging video coding standard AOMedia Video 1 (AV1), released in 2018 by the
Alliance of Open Media [4], achieves higher bitrate savings compared to its
predecessor VP9 [5], however, at the cost of an increased encoding complexity
[6]. Some actions have been made in minimizing encoding complexity by SVT-AV1
that mitigates some of the complexity overhead such as maximizing CPU
utilization for multicore processing [7, 8, 9].

Before any actions towards minimizing the carbon dioxide emission of video
encoding can be made, influences of encoding configuration as well as video
parameters on energy consumption during encoding have to be studied first.
Work on estimating encoding energy for AV1 or SVT-AV1 has not been done yet,
only for other video encoders. Rodríguez-Sánchez et al. [10] proposed an
encoding time prediction for intra-only coding for high-efficiency video
coding (HEVC). The energy estimate $\hat{E}_{\mathrm{enc}}$ is given by

$\hat{E}_{\mathrm{enc}}=P_{\mathrm{avg}}\cdot t_{\mathrm{enc}}$ (1)

and depends on the average power $P_{\mathrm{avg}}$ and the processing time
$t_{\mathrm{enc}}$, that was estimated using the quantization parameter (QP).
Mid-range QPs lead to larger prediction error, which Ramasubbu et al. [11]
minmized by introducing a constant offset energy $E_{0}$:

$\hat{E}_{\mathrm{enc}}=E_{0}+P\cdot t_{\mathrm{enc}}.$ (2)

Here, $P$ corresponds to the mean processing power, with $t_{\mathrm{enc}}$
and $\hat{E}_{\mathrm{enc}}$ again corresponding to the encoding time and
estimated energy for HEVC, respectively. Furthermore, Ramasubbu et al.
estimated HEVC encoding energy by exploiting bit stream features [12].

An encoding time model for HTTPS Adaptive Streaming (HAS) using HEVC was
proposed by Amirpour et al. using spatiotemporal features from the video
complexity analyzer (VCA) [13]. Until now, only transcoding time estimators
for AV1 exist, i.e. Liapin et al. propose an H.264/H.256 to AV1 transcoding
using object tracking [14]. Those two models have one thing in common: they
obtain at one point information about the content of the video scene. Because
of this observation, we also adopt content information for our proposed model.

This paper contributes the following: First, we verify the energy-time
correlation for SVT-AV1 and observe that we can model encoding energy from
processing time. We then propose a single-core encoding time model based on
video parameter and encoder configurations such as the preset. We study the
influence of the video content by testing common content descriptors from the
literature. We then use the linear model to obtain the expected energy
consumption to verify that we can use any time model to estimate encoding
energy.

In Sec. 2, we define an encoding energy model for SVT-AV1 that depends on the
processing time required for encoding a video sequence. Details about tested
content descriptors are explained in Sec. 3. In Sec. 4, we first verify the
linear relationship between processor time and energy demand for the SVT-AV1
encoder. Then, we evaluate the encoding time model without content information
and with the tested content descriptors. Finally, we give the estimation
errors for combining time and energy model.

##  2 High-Level Encoding Energy Model for SVT-AV1

Using the energy-time correlation from [11], we develop an encoding time model
depending on the following parameters: preset, constant rate factor (CRF), and
number of intra frames. We define the complexity $\hat{E}_{\mathrm{enc,kpix}}$
as the energy demand needed for the encoding of $1000$ pixels in 8-bit by

$\hat{E}_{\mathrm{enc,kpix}}=E_{0}+P\cdot
t_{\mathrm{enc,kpix}}\cdot\frac{W\cdot H}{1000}\cdot n_{\mathrm{frames}},$ (3)

with $t_{\mathrm{enc,kpix}}$ being the encoding time per kilopixel, and $W$
and $H$ denoting the width and height of the video sequence. The number of
frames in the video is denoted as $n_{\mathrm{frames}}$. Furthermore, $E_{0}$
is the idle energy and $P$ the slope. They depend on the CPU used for
encoding, whereas the encoding time is influenced by the encoder
configurations and the video content. We will estimate $E_{0}$ and $P$ for
this energy model and propose an encoding time model to estimate the required
processing time.

We assume an exponential relationship between preset $p$ and encoding time, as
well as a linear relationship between the number of intra frames
$n_{\mathrm{intra}}$ and the constant rate factor $CRF$. We estimate the
encoding time per kilopixel $\hat{t}_{\mathrm{enc,kpix}}$ as

$\hat{t}_{\mathrm{enc,kpix}}=\mathcal{C}^{\xi}\cdot
n_{\mathrm{intra}}^{\delta}\cdot\frac{1}{\mathrm{CRF}}\cdot p^{\alpha}\cdot
e^{\beta\cdot p+\gamma}+t_{0},$ (4)

with $t_{0}$ being the offset time, $\mathcal{C}$ an initially unknown content
dependency, as well as parameters to be fitted: the preset dependencies
$\alpha$, $\beta$, $\gamma$, the influence of the number of intra-coded frames
$\delta$, and the video content influence $\xi$. Apart from the exponential
term, we additionally introduce a polynomial dependency for the preset:
$p^{\alpha}$. This leads to a more accurate model.

##  3 Content Dependency

We assume that the content influence on expected time or energy demand is
constant for one video sequence and call this the content complexity factor
$\mathcal{C}$. Increased encoding effort first comes from spatial complexity
$\mathcal{C}_{\mathrm{S}}$, that corresponds to higher structured areas in
single frames as well as temporal complexity $\mathcal{C}_{\mathrm{T}}$, which
stems from moving objects. To quantify the content effect on the encoding
time, we combine both texture and temporal complexity of the sequence and
obtain the content complexity factor, which is an adaption of criticality from
Fenimore et al. [15]:

$\mathcal{C}=f_{n,s}\left(\mathcal{C}_{\mathrm{S}}\right)\cdot
f_{n,t}\left(\mathcal{C}_{\mathrm{T}}\right)$ (5)

Here $\mathcal{C}_{\mathrm{S}}$ denotes the influence of spatial and
$\mathcal{C}_{\mathrm{T}}$ the influence of temporal changes, accompanied by
normalizing functions $f_{n,s}(\cdot)$ and $f_{n,s}(\cdot)$ for both spatial
and temporal content complexity, accordingly. Both temporal and spatial
complexity may not be equally important for encoding complexity. By
introducing normalizing function, we can study the effect on prediction
accuracy by diminishing either of them.

###  3.1 Spatial Complexity

Encoding time increases if the spatial structure is highly varying compared to
flat areas. In the following, various methods to quantify this spatial
complexity are introduced. Spatial information (SI) is defined as

$\mathcal{C}_{s;\mathrm{SI}}=\mathrm{rms}_{\mathrm{space}}\left(\mathrm{Sobel}(X(t_{n}))\right),$
(6)

where $X(t_{n})$ is the frame at index $t_{n}$, $\mathrm{Sobel}(\cdot)$
denotes the Sobel filter, and
$\mathrm{rms}_{\mathrm{space}}\left(\cdot\right)$ corresponds to the root mean
square value over all frames [16]. Spatial complexity from spatial information
is then given by $\mathcal{C}_{s;\mathrm{SI}}$. Furthermore, we use spatial
complexity calculated by the video complexity analyzer (VCA) from Vignesh et
al. [17]. Here, the spatial complexity $\mathcal{C}_{s;\mathrm{VCA}}$ can be
obtained by the discrete cosine transform $\mathrm{DCT}(\cdot)$, i.e.,

$\mathcal{C}_{s;\mathrm{VCA}}=\sum_{k=0}^{C-1}\frac{H_{p,k}}{C\cdot w^{2}},$
(7)

with the block-wise texture for each frame given as

$H_{p,k}=\sum_{i=0}^{w-1}\sum_{j=0}^{w-1}e^{|\left(\frac{ij}{w^{2}}\right)^{2}-1|}|\mathrm{DCT}(i,j)|.$
(8)

The number of blocks per frame is denoted as $C$, $k$ is the block-address in
frame $p$, with block sizes of $w\times w$. Pixel addresses inside a block are
indicated by $i$ and $j$. Spatial complexity from variance
$\mathcal{C}_{s;\mathrm{var}}$ can also be estimated by the variance, where we
will use the average block-based variance with 64x64 dimensional blocks:

$\mathcal{C}_{s;\mathrm{var}}=\sum_{k=0}^{C-1}\frac{H_{p,k}^{\mathrm{var}}}{C\cdot
64^{2}}.$ (9)

$H_{p,k}^{\mathrm{var}}$ is the variance from block $k$ in frame $p$, and $C$
the number of blocks per frame.

###  3.2 Temporal Complexity

Movements from objects in the video scene and from the camera lead to temporal
complexity of a video sequence. The metrics used in order to quantify the
amount of temporal changes are introduced in the following.

First, we use $\mathcal{C}_{t;\mathrm{TI}}$, the complexity from temporal
information (TI):

$\mathcal{C}_{t;\mathrm{TI}}=\mathrm{rms}_{\mathrm{space}}\left(X(t_{n})-X(t_{n-1})\right).$
(10)

Again, $\mathrm{rms}_{\mathrm{space}}\left(\cdot\right)$ corresponds to the
root mean square value over all frames and $X(t_{n})$ is the frame at index
$t_{n}$ [16]. Temporal complexity from VCA $\mathcal{C}_{t;\mathrm{VCA}}$ is
tested, as well, that is

$\mathcal{C}_{t;\mathrm{VCA}}=\sum_{k=0}^{C-1}\frac{\mathrm{SAD}(H_{p,k}-H_{p-1,k})}{C\cdot
w^{2}},$ (11)

with $\mathrm{SAD}(\cdot)$ being the sum of absolute differences and $H_{p,k}$
the block-wise texture from (8). The number of frames per block is $C$ and $k$
is the block-address in frame $p$ with block sizes $w\times w$ [17]. Last, we
use optical flow $\mathcal{C}_{t;\mathrm{optical\leavevmode\nobreak\ flow}}$,
where the mean spatial displacement over the sequence is used, that is

$\mathcal{C}_{t;\mathrm{optical\leavevmode\nobreak\
flow}}=\frac{1}{n_{\mathrm{frames}}}\sum_{t}^{n_{\mathrm{frames}}}\sqrt{(u_{t}+v_{t})^{2}}.$
(12)

The number of frames is $n_{\mathrm{frames}}$. $u_{t}$ and $v_{t}$ correspond
to the horizontal and vertical displacement at time $t$, respectively, that is
calculated by the optical flow equation, which is solved using the dense flow
algorithm from Farnebäck et al. [18].

###  3.3 Ultrafast Encoding

Another complexity indicator is the time of ultrafast encoding [11], i.e.,
encoding with preset 13 for SVT-AV1. By encoding with the fastest preset, the
ratio of intra- and inter-coded frames is the same as for slower presets. We
assume slower presets leading to a scaling of inter- (or temporal) as well as
inter-coded (or spatial) frame complexity and thus a linear scaling of
encoding time. To comply with our model, we convert this time to seconds per
kilopixel:

$\mathcal{C}_{s,t;\mathrm{ultrafast}}=t_{\mathrm{preset13}}\cdot\frac{1000}{W\cdot
H\cdot n_{\mathrm{frames}}}.$ (13)

$\mathcal{C}_{s,t;\mathrm{ultrafast}}$ denotes the ultrafast complexity and
$t_{\mathrm{preset13}}$ the time for encoding with the fastest preset.

##  4 Evaluation

We evaluate the proposed model by estimating and measuring the energy
consumption and processing time when encoding with SVT-AV1 on an AMD 7452
processor @2.35 GHz uing single-core processing. We study the content of $18$
sequences from the AOM Common Test Conditions [19] – all sequences from
classes A3 and A4 and the following six sequences from class A2: MountainBike,
OldTownCross, PedestrianArea, RushFieldCuts, WalkingInStreet, and Riverbed. We
encode with CRF $\in\left\\{32,43,55,63\right\\}$, presets
$\in\left\\{1,2,...,13\right\\}$, random access configuration, and the default
GOP size of $\sim 5s$. The mean average precision error metric (MAPE) is used
for comparing estimated $\hat{y}$ and measured values $y$:

$\mathrm{MAPE}(y,\hat{y})=\frac{1}{n}\cdot\sum_{i=1}^{n}\frac{|y_{i}-\hat{y}_{i}|}{y_{i}}.$
(14)

The total number of encodings is $n$ with $i$ denoting their index. To comply
with the small number of sequences, 3-fold cross-validation is used for the
time model. Each fold consists of 2 sequences from each class and two folds
are used for fitting and one for validation. The reported errors are the mean
for each fold.

###  4.1 Energy Measurement Setup

The energy model (3) is evaluated by measuring the power consumption with an
external power meter. In order to eliminate the energy overhead from
background processes, subtracting the idle energy is necessary to obtain the
actual energy demand as described in [20]. Therefore, we first measure the
power consumption $P_{\mathrm{total}}(t)$ during encoding over a time period
$T$ and subtract the integrated idle power $\int
P_{\mathrm{idle}}(t)\mathrm{d}t$ within the same interval and get the encoding
energy $E_{\mathrm{enc}}$:

$E_{\mathrm{enc}}=\int_{t=0}^{T}P_{\mathrm{total}}(t)\quad\mathrm{d}t-\int_{t=0}^{T}P_{\mathrm{idle}}(t)\quad\mathrm{d}t.$
(15)

Here, $t$ corresponds to the time. In order to remove noise, we repeat each
energy measurement $m$ times until the following condition is satisfied:

$2\cdot\frac{\sigma}{\sqrt{m}}\cdot
t_{\alpha_{m}}\left(m-1\right)<\beta_{m}\cdot E_{\mathrm{enc}}.$ (16)

The maximum deviation from the actual energy is then given by $\beta$, with a
probability of $\alpha$. Furthermore, $t_{\alpha}$ is the critical value of
Student’s t-distribution and $\sigma$ the standard deviation. We chose
$\alpha_{m}=0.99$ and $\beta_{m}=0.02$, according to [20].

| SI | VCA E | Variance | Ultrafast
---|---|---|---|---
TI | 25.64 | 23.23 | 25.90 | -
VCA h | 20.76 | 19.64 | 20.78 | -
Optical flow | 25.29 | 23.84 | 25.71 | -
Ultrafast | - | - | - | 25.59
Table 1: Errors in $\%$ between estimated and measured encoding time. Best complexity estimators for both spatial and temporal complexity is from VCA which is denoted in bold numbers. | SI | VCA E | Variance | Ultrafast
---|---|---|---|---
TI | 26.77 | 24.48 | 26.94 | -
VCA h | 22.16 | 20.94 | 22.14 | -
Optical flow | 26.44 | 28.94 | 26.81 | -
Ultrafast | - | - | - | 26.24
Table 2: Errors in $\%$ between estimated and measured encoding energy. Again,
the best complexity estimators for both spatial and temporal complexity is
from VCA (indicated in bold).

###  4.2 Evaluation of Energy Model Using Measured Encoding Time for SVT-AV1

Encoding time measurements are obtained during energy measurements by using
the CPU utilization time. The measured data is fitted on the model from (3)
using least-squares fitting on all data points. The fitted parameter values
are $E_{0}=1.68\cdot 10^{-19}$ and $P=1.77\cdot 10^{-2}$ with a MAPE of
$2.93\%$. Therefore, we can conclude that instead of estimating encoding
energy, it is sufficient to estimate encoding CPU time instead.

###  4.3 Encoding Time Model Using Content Information

First, we study the influence of the video content by comparing the errors for
time prediction without content information and time prediction with an oracle
test by assuming that the content factor $\mathcal{C}$ is known for each
sequence. The estimated encoding time without any prior knowledge is obtained
by setting the content complexity measure $\mathcal{C}=1$ for each sequence.
This results in an estimation error of $38.44\%$. For the optimal content
complexity w.r.t. (4), we use the fraction between real and estimated time for
each sequence, averaging over all CRF–preset combinations. These are shown in
Fig. 1. The higher the content complexity factor, the higher the time or
energy required for encoding, i.e. encoding the sequence RedKayak is more
complex than ControlledBurn in terms of time and also in terms of energy.
Furthermore, we observe larger deviations for higher-complexity sequences,
hence describing the content influence as a constant factor for those will
lead to larger prediction errors. Assuming these theoretical optimal values
for content complexity to be known and evaluating the proposed time model
results in an estimation error of $17.44\%$, which is the lower bound when
approximating constant content influence on encoding time.

Fig. 1: Optimal content factors for evaluated sequences and their standard
deviations indicated by black error bars. The higher the value, the more time
is required for encoding the associated sequence. Larger deviations in content
complexity factors are observed for high-complexity sequences.

For evaluation, each spatial complexity factor $\mathcal{C}_{s}$ is combined
with each temporal factor $\mathcal{C}_{t}$, as described in (5). Normalizing
functions are used for spatial complexity values, i.e., $f_{n,s}=\ln(\cdot)$
for $\mathcal{C}_{s;\mathrm{SI}}$, $\mathcal{C}_{s;\mathrm{VCA}}$, and
$\mathcal{C}_{s;\mathrm{var}}$. Spatial complexity estimates have shown a
lower correlation to encoding time and thus applying the logarithm diminishes
their influence on content complexity. The results are listed in Tab. 1.
Looking at the average deviations, VCA performs best when used as spatial as
well as temporal complexity with an estimation error of $19.64\%$ , which is
close to the best reachable error of $17.44\%$. Nevertheless, using any of the
tested content descriptor without content copmlexity measure significantly
decreases the estimation error of $38\%$ by almost a factor of 2. Using
criticality from [15] as a content estimator, which is a frame-wise
combination of SI and TI, leads to a MAPE of $25.64\%$. VCA outperforms
criticality here. Looking at the average errors over single presets and CRFs,
the highest MAPE occurs for preset 1 ($28.36\%$) and the lowest for preset 5
($13.47\%$). For CRF, the highest error is at $CRF=63$ ($31.29\%$) and lowest
at $CRF=43$ ($16.7\%$).

###  4.4 Energy Model Using Estimated Encoding Time

The encoding energy is estimated from (3) with the time being approximated by
(4) and the errors are shown in Tab. 2. On average, the error increases by
$1.3$ percentage points and again, the smallest prediction error is observed
for combining spatial and temporal complexity from VCA resulting in an MAPE of
$20.94\%$. The prediction error without including any content descriptors is
$39.23\%$.

##  5 Conclusion

We observe that the encoding complexity of AV1 highly depends on the displayed
content of the video. Using a parametric model, we can predict the encoding
energy with a mean average precision error of $39\%$ without any prior
information on the content and $21\%$ by incorporating content information.
Furthermore, we have verified the correlation between processing time and
encoding energy for SVT-AV1 with $3\%$ mean relative estimation error and thus
we can model the consumed energy during the encoding process by its processing
time. In future work, we will extend the model for multicore processing and
study energy consumption for transmission and decoding to model the total
energy consumption of video communication.

## References

  * [1] C. Herglotz, A. Heindel, and A. Kaup, “Decoding-energy-rate-distortion optimization for video coding,” IEEE Transactions on Circuits and Systems for Video Technology, vol. 29, no. 1, pp. 171–182, 2019.
  * [2] A. Stephens, C. Tremlett-Williams, L. Fitzpatrick, L. Acerini, M. Anderson, and N. Crabbendam, “Carbon impact of video streaming,” 2021.
  * [3] U. Cisco, “Cisco annual internet report (2018–2023) white paper,” Cisco: San Jose, CA, USA, vol. 10, no. 1, pp. 1–35, 2020.
  * [4] Y. Chen, D. Murherjee, J. Han, A. Grange, Y. Xu, Z. Liu, S. Parker, C. Chen, H. Su, U. Joshi, C.-H. Chiang, Y. Wang, P. Wilkins, J. Bankoski, L. Trudeau, N. Egge, J.-M. Valin, T. Davies, S. Midtskogen, A. Norkin, and P. de Rivaz, “An overview of core coding tools in the AV1 video codec,” in Proc. Picture Coding Symposium (PCS), pp. 41–45, 2018.
  * [5] D. Mukherjee, J. Bankoski, A. Grange, J. Han, J. Koleszar, P. Wilkins, Y. Xu, and R. Bultje, “The latest open-source video codec VP9-an overview and preliminary results,” in Proc. Picture Coding Symposium (PCS), pp. 390–393, 2013.
  * [6] D. Grois, T. Nguyen, and D. Marpe, “Performance comparison of AV1, JEM, VP9, and HEVC encoders,” in Applications of Digital Image Processing XL, vol. 10396, pp. 68–79, SPIE, 2018.
  * [7] F. Kossentini, H. Guermazi, N. Mahdi, C. Nouira, A. Naghdinezhad, H. Tmar, O. Khlif, P. Worth, and F. B. Amara, “The SVT-AV1 encoder: overview, features and speed-quality tradeoffs,” Applications of Digital Image Processing XLIII, vol. 11510, pp. 469–490, 2020.
  * [8] P.-H. Wu, I. Katsavounidis, Z. Lei, D. Ronca, H. Tmar, O. Abdelkafi, C. Cheung, F. B. Amara, and F. Kossentini, “Towards much better SVT-AV1 quality-cycles tradeoffs for VOD applications,” in Applications of Digital Image Processing XLIV (A. G. Tescher and T. Ebrahimi, eds.), vol. 11842, p. 118420T, International Society for Optics and Photonics, SPIE, 2021\.
  * [9] G. Cobianchi, G. Meardi, S. Poularakis, A. Walisiewicz, O. Abdelkafi, F. B. Amara, F. Kossentini, C. Stejerean, and H. Tmar, “Enhancing SVT-AV1 with LCEVC to improve quality-cycles trade-offs and enhance sustainability of VOD transcoding,” in Applications of Digital Image Processing XLV (A. G. Tescher and T. Ebrahimi, eds.), vol. 12226, p. 122260S, International Society for Optics and Photonics, SPIE, 2022.
  * [10] R. Rodríguez-Sánchez, M. T. Alonso, J. L. Martínez, R. Mayo, and E. S. Quintana-Ortí, “Time and energy modeling of an intra-only HEVC encoder,” in 2015 Visual Communications and Image Processing (VCIP), pp. 1–4, 2015.
  * [11] G. Ramasubbu, A. Kaup, and C. Herglotz, “Modeling the HEVC encoding energy using the encoder processing time,” in 2022 IEEE International Conference on Image Processing (ICIP), pp. 3241–3245, 2022.
  * [12] G. Ramasubbu, A. Kaup, and C. Herglotz, “A bit stream feature-based energy estimator for HEVC software encoding,” in 2022 Picture Coding Symposium (PCS), pp. 19–23, 2022.
  * [13] H. Amirpour, P. T. Rajendran, V. V. Menon, M. Ghanbari, and C. Timmerer, “Light-weight video encoding complexity prediction using spatio temporal features,” in 2022 IEEE 24th International Workshop on Multimedia Signal Processing (MMSP), pp. 1–6, 2022.
  * [14] I. Liapin, “Fast H.264/H.265 to AV1 stream transcoding using a moving object tracker,” in 2018 International Symposium on Consumer Technologies (ISCT), pp. 9–13, 2018.
  * [15] C. Fenimore, J. Libert, and S. Wolf, “Perceptual effects of noise in digital video compression,” in 140th SMPTE Technical Conference and Exhibit, pp. 1–17, 1998.
  * [16] P. ITU-T RECOMMENDATION, “Subjective video quality assessment methods for multimedia applications,” 1999.
  * [17] V. V. Menon, C. Feldmann, K. Schoeffmann, M. Ghanbari, and C. Timmerer, “Green video complexity analysis for efficient encoding in adaptive video streaming,” in Proceedings of the First International Workshop on Green Multimedia Systems, GMSys ’23, (New York, NY, USA), p. 16–18, Association for Computing Machinery, 2023.
  * [18] G. Farnebäck, “Two-frame motion estimation based on polynomial expansion,” in Image Analysis: 13th Scandinavian Conference, SCIA 2003 Halmstad, Sweden, June 29–July 2, 2003 Proceedings 13, pp. 363–370, Springer, 2003.
  * [19] X. Zhao, Z. R. Lei, A. Norkin, T. Daede, and A. Tourapis, “AOM common test conditions v2. 0,” Alliance for Open Media, Codec Working Group Output Document, 2021.
  * [20] C. Herglotz, D. Springer, M. Reichenbach, B. Stabernack, and A. Kaup, “Modeling the energy consumption of the HEVC decoding process,” IEEE Transactions on Circuits and Systems for Video Technology, vol. 28, no. 1, pp. 217–229, 2016.