To appear in Math. Struct. in Comp. Science

Selection Functions, Bar Recursion, andBackward Induction
M a r tı́ n E s c a r d ó1 and P a u l o O l i v a2
1
2

University of Birmingham, Birmingham B15 2TT, UK.
Queen Mary University of London, London E1 4NS, UK

Revised version November 11, 2009

Bar recursion arises in constructive mathematics, logic, proof theory and higher-typecomputability theory. We explain bar recursion in terms of sequential games, and show
how it can be naturally understood as a generalisation of the principle of backward
induction that arises in game theory. In summary, bar recursion calculates optimal plays
and optimal strategies, which, for particular games of interest, amount to equilibria. We
consider finite games and continuous countably infinite games, and relate the two. The
above development is followed by a conceptual explanation of how the finite version of
the main form of bar recursion considered here arises from a strong monad of selections
functions that can be defined in any cartesian closed category. Finite bar recursion turns
out to be a well-known morphism available in any strong monad, specialised to theselection monad.

1. Introduction
We define a generalisation of sequential games and investigate constructions of optimal
outcomes and strategies via a form of bar recursion (Berardi et al., 1998; Berger andOliva, 2006; Spector, 1962), which we propose as a formalisation of the principle ofbackward induction from game theory (Nisan et al., 2007). Our sequential games aredefined in terms of rounds, where Xi are the possible moves at round i, leaving open thenumber of players, and who plays at each round. The outcome of a game is specified by
an n-ary predicate p : Πn−1
i=0 Xi → R, and the aim of the game by a quantifier for eachround of the game. For instance, assume that R is the set B = {true, false} of booleans,and consider a game between two players, playing in alternating rounds, with the firstplayer trying to force the outcome to be the value true while the second player tries toobtain the opposite outcome false. The first player has a winning strategy if and only if∃x0 ∀x1 ∃x2 ∀x3 . . . p(x0 , . . . , xn−1 ).
On the other hand, assume the aim at each round is to force the outcome to be the value
true. In this case, the existence of a winning strategy corresponds to the satisfiability ofthe predicate p, i.e.
∃x0 ∃x1 . . . ∃xn−1 p(x0 , . . . , xn−1 ).

M. Escardó and P. Oliva

2

Dually, if the goal of each round is to obtain a final outcome false, the non-existence ofa winning strategy corresponds to the tautology of the predicate p, i.e.
∀x0 ∀x1 . . . ∀xn−1 p(x0 , . . . , xn−1 ).
Now consider games with more than two outcomes, e.g. R = {−1, 0, 1}. Following up
from our first example, suppose the outcome 1 means that the first player wins, −1means that the second player wins, and 0 stands for a draw. In this case, the existenceof a non-losing strategy for the first player is expressed as!
supinf . . .

x0 ∈X0 x1 ∈X1

sup

inf

xn−2 ∈Xn−2 xn−1 ∈Xn−1

p(x0 , . . . , xn−1 )≥ 0.

Similarly, if all inf functionals are replaced by sup, this corresponds to a game where eachround is trying to maximise the final global payoff p(x0 , . . . , xn−1 ). In this last case, if
R = Rn and at each round i we are trying to maximise the i-coordinate of the outcome,the existence of a winning strategy corresponds to the existence of a profile in Nashequilibrium for sequential games (Nisan et al., 2007).
In summary, the goal at each round i, in an n-round game, is defined via an outcome
quantifier,φi : (Xi → R) → R,
which we leave open in the definition of the game. In the case φi are the standard
quantifiers ∃, ∀ : (X → B) → B or the supremum and infimum functionals sup, inf : (X →R) → R, where R is a closed and bounded set of real numbers, we obtain the examples
mentioned above. We then define the product of generalised quantifiers and use it todefine notions such as optimal play, outcome and strategy.
Some generalised quantifiers φ : (X → R) → R have selection functions, i.e. functions
ε : (X → R) → X
satisfying φ(p) = p(ε(p)). For example, a selection function for the supremum functional
sup : (X → R) → R, when it exists, gives a point at which p attains its maximum value
max p. We show that, when outcome quantifiers have selection functions, an optimal
strategy for the game can be computed via a suitably defined product of corresponding selection functions. This product will turn out to appear not only in game theory(corresponding to backward induction (Nisan et al., 2007)), but also in algorithms (corresponding to backtracking (Valiente, 2002)) and proof theory (corresponding to bar
recursion (Berardi et al., 1998; Berger and Oliva, 2006; Spector, 1962)), among others.
We then consider the infinite iteration of the binary product of selection functions,and discuss how this gives optimal strategies in finite games of unbounded length. Boththe finite and infinite products considered here are generalisations of previous work of
the first author (Escardó, 2008). This is explained in Section 5, where we also show how
the infinite product amounts to a form of bar recursion.
The above development is followed by a conceptual explanation of how the finite versionof the main form of bar recursion considered here arises from a strong monad of selections
functions that can be defined in any cartesian closed category (Kock, 1972; Mac Lane,

Selection functions

31971). The finite form of bar recursion turns out to be a well-known morphism available
in any strong monad, specialised to the selection monad.
1.1. Organisation
Section 2. Generalised quantifiers, finite products of quantifiers, and sequential games.
Section 3. Selection functions, finite products of selection functions, calculation of optimal strategies. Section 4. Applications. Section 5. Infinite products of selection functions
and quantifiers, bar recursion. Section 6. The continuation and selection monads. Section 7. Further work.
1.2. Background and pre-requisites
This paper has been deliberately written so that readers who are not familiar with certain
categorical notions should be able to follow Sections 2–4 without the need of familiarisingthemselves with such concepts. These sections are officially developed in the generalityof cartesian closed categories, but linguistically developed as if we were working with sets
and functions as in ordinary mathematics (see below). Sections 5 and 6, on the other
hand, rely on and apply to cartesian closed categories other than that of sets.
Recall that a category is called cartesian closed if it has finite products 1 and X ×Y , andfunction spaces (X → Y ), often written Y X in the literature, characterised by a naturalbijection between maps A × X → Y and A → (X → Y ) (see (Mac Lane, 1971)), given
by currying and uncurrying in lambda-calculus terminology. Recall also that cartesianclosedness is precisely what is needed in a category so that one can interpret the simplytyped lambda-calculus (Lambek and Scott, 1986). In the category of sets, the function
space (X → Y ) is the set of all functions X → Y , and in certain cartesian closed of
topological spaces, (X → Y ) is the set of continuous maps with a suitable topology (seee.g. (Escardó et al., 2004)).
The main cartesian closed categories of interest for this work include (i) that of sets andfunctions, and more generally toposes (Johnstone, 2002), (ii) Howard/Bezem majorizable
functionals (Bezem, 1985), (iii) spaces endowed with extended admissible representationsin the sense of (Schröder, 2002), (iv) several categories of continuous maps of topologicalspaces (Escardó et al., 2004), such as k-spaces, QCB spaces (Battenfeld et al., 2007),
Kleene–Kreisel spaces and continuous functionals (Normann, 1980), various categories ofdomains under the Scott topology (Abramsky and Jung, 1994), and (v) several categories
of effective maps of effectively presented objects, such as Kleene–Kreisel computablemaps (Normann, 1980), effectively given domains (Smyth, 1977), and the effective topos
and realizability toposes, among others.
When working with our underlying cartesian closed category, we reason with generalised elements and the λ-calculus. So, for example, for any given m : X × X → X,
the equation m(x, y) = m(y, x) amounts to the element-free equation m = m ◦ hπ1 , π0 i,where π0 , π1 are the projections. If m is regarded as a variable rather than a constant,this equation is to be understood as λm.m = λm.m ◦ hπ0 , π1 i. A global element of X is a
map 1 → X, and a generalised element of X is a map S → X, where S is called the stage

M. Escardó and P. Oliva

4of definition of x. We write x : X, and occasionally x ∈ X by an abuse of language, tomean that x is a generalised element of X at an unspecified stage S, which never needs
to be mentioned explicitly due to the fact that we are working with the lambda-calculus.
When the underlying category is well pointed, e.g. the category of sets and categories ofcontinuous maps of spaces or domains, working with generalised elements is equivalent
to working with actual elements (or global elements), and most of our examples will fallin this kind of category.
Acknowledgements. We would like to thank Matı́as Menni for discussions about the
subject of Section 6. We thank the anonymous referees for a careful reading of the paperand helpful suggestions. The second author also gratefully acknowledges support of theRoyal Society under grant 516002.K501/RH/kk.

2. Generalised Quantifiers
The main notion discussed in this section is that of a (generalised ) quantifier. Assume afixed cartesian closed category, with a fixed object R, and define
KX := (X → R) → R.
We think of R as an object of generalised truth values, of functions X → R as predicates, of R-valued functions of several variables as relations, and of the elements of KX
as generalised quantification functions, which, by an abuse of language, we refer to as
quantification functions or simply quantifiers. This construction is part of a well-known
monad, which we will develop in Section 6.
Examples 2.0.1.
1

Our underlying category is that of sets. Then the standard universal and existential
quantifiers ∀X , ∃X are elements of KX with R = B = {true, false}.
2 More generally, our underlying category is a topos and R = Ω is the object of truth
values (subobject classifier). Then the standard universal and existential quantifiers∀X , ∃X are elements of KX. Recall that in the topos of sets, Ω = {false, true} = {0, 1}.
We assume classical logic for the topos of sets (principle of excluded middle and axiomof choice).
3 Continuing from above, defineφ(p) := ∀x ∈ X∃y ∈ Y p(x, y),4

for p : X × Y → R. Then φ ∈ K(X × Y ).
Assume R is the real line R in a cartesian closed category of spaces and continuousfunctions (such as k-spaces, QCB spaces, etc.). Define
Z 1p,
I(p) :=
0for p : [0, 1] → R. Then I ∈ K[0, 1].

Selection functions
5

5

Continuing from the previous example, define
Z 1p(x, y)dy,φ(p) := supx∈[0,1]0

for p : [0, 1]2 → R. Then φ ∈ K([0, 1]2 ).
2.1. Finite products of quantifiers
The above Examples 2.0.1(3) and 2.0.1(5) are instances of the following construction.
Definition 2.1.1. Given quantifiers φ ∈ KX and γ ∈ KY , define a new quantifierφ ⊗ γ ∈ K(X × Y )by, for any p : X × Y → R,
(φ ⊗ γ)(p) := φ(λx.γ(λy.p(x, y))).
Examples 2.1.2.
1

If R is the object of truth values in a topos, then ∀X ⊗ ∀Y = ∀X×Y , as this amountsto(∀X ⊗ ∀Y )(p) = ∀x ∈ X(∀y ∈ Y (p(x, y))) = ∀z ∈ X × Y (p(z)) = ∀X×Y (p).

2 Similarly, we have that ∃X ⊗ ∃Y = ∃X×Y .
3 And also (∀X ⊗ ∃Y )(p) = ∀x ∈ X ∃y ∈ Y p(x, y).
4 If R are the real numbers R in a cartesianof spaces and continuous
R
Rclosed categoryRfunctions, by Fubini’s rule, we have [0,1] ⊗ [0,1] = [0,1]×[0,1] , as this amounts to!
ZZZp(x, y)dy dx =
[0,1]

5

[0,1]

p(x, y)d(x, y).
[0,1]×[0,1]Generalising the previous example, let νi be Borel regular measures on locallycompact
R
Hausdorff spaces Xi for i = 0, 1, and define φi ∈ KXi by φi (p) := pdνi . Thenφ ∈ K(X0 × X1 ) defined byZ
φ(p) := pd(ν0 × ν1 )satisfies φ = φ0 ⊗ φ1 , where ν0 × ν1 is the product measure.

We now consider the iteration of the binary product of quantifiers defined above. Let
us writen−1YXi := X0 × · · · × Xn−1
i=0with the conventions that the operation × is right associative, that for n = 0 this is the
one-point set 1 = {()} where () is the empty sequence, and that for n = 1 this is X0 .
Hence for n > 1 this is
n−1
Y
X0 ×
Xi .
i=1

M. Escardó and P. Oliva
Qn−1
Nn−1
Definition 2.1.3. Given quantifiers φ ∈ i=0 KXi , we define i=0 φi ∈ K
asn−1
O
φi := φ0 ⊗ · · · ⊗ φn−1 ,Q

n−1i=0 Xi6

i=0which, expanding the definition amounts to!
n−1Oφi (p) := φ0 (λx0 .φ1 (λx1 . · · · φn−1 (λxn−1 .p(x0 , x1 , . . . , xn−1 )) · · · )).
i=0

Alternatively, we can define this product inductively, since
!
n−1
n−1
O
O
φi = φ0 ⊗φi .
i=0In this case we have!
n−1Oφi (p) = φ0

λx0 .

i=0

i=1

n−1
O

!
φi

!
(λ(x1 , . . . , xn−1 ).p(x0 , x1 , . . . , xn−1 )) ,i=1

which, writing px0 (x1 , . . . , xn ) := p(x0 , x1 , . . . , xn ), can be expressed concisely as
!
!
!
n−1
n−1
O
O
φi (p) = φ0 λx0 .
φi (px0 ) .
i=0

i=1

Nn−1
That is, the value of the quantifier  i=0 φi ona predicate p is given by the value of theNn−1 
quantifier φ0 on the predicate λx0 .
i=1 φi (px0 ). For the base case we can take theunary casen−1O
φi = φn−1
i=n−1

or, alternatively, the nullary case
n−1
O

!
φi

(p) = p(),

i=n

Qn−1
if we instead adopt the convention that i=0 Xi = X0 × · · · × Xn−1 × 1 with theoperation × right associative (cf. Section 3.3 below).
The empty product of quantifiers lives in K1 and is both the universal quantifier ∀1
and the existential quantifier ∃1 , given by λp.p(). With our official convention for finite
products, this is a neutral element for the binary product up to isomorphism, in the sensethat ∀1 ⊗ φ ∈ K(1 × X) and φ × ∀1 ∈ K(X × 1) are isomorphic to φ ∈ KX via theisomorphisms K(1 × X) ∼= KX ∼= K(X × 1).
2.2. Quantifiers in sequential games
We now show how generalised quantifiers and their iterated products can be used toconveniently express some general notions regarding finite sequential games. It should

Selection functions

7

be noted that we use the language of sequential games simply for the sake of intuition,but, as we shall see in Section 4, our notion of game is general enough to capture many
specific constructions in several application areas that are not usually formulated in termsof games.
Example 2.2.1. Consider an alternating, two-person game that finishes after exactly n
moves, with one of the players winning. The i-th move is an element of the set Xi and theQn−1game is defined by a predicate p : i=0 Xi → R, with R = Ω, that tells whether the firstQn−1player, Eloise playing against Abelard, wins a given play ~x = (x0 , . . . , xn−1 ) ∈ i=0 Xi .
Then Eloise has a winning strategy for the game p if and only if∃x0 ∈ X0 ∀x1 ∈ X1 . . . ∃xn−2 ∈ Xn−2 ∀xn−1 ∈ Xn−1 p(x0 , . . . , xn−1 )holds (assuming n even for notational convenience). Let φi := ∃Xi for i even and φi :=∀Xi for i odd. The above sufficient and necessary condition on Eloise having a winning
strategy can be concisely expressed as!
nOφi (p).
i=1

The following definition abstracts from this example in several ways. First we assume
R to be an arbitrary fixed object. Also, we focus on the number of rounds of the game,
ignoring the number of players and who plays in each round, and we take the quantifier tobe applied in each round as part of the definition of the game. We still require, however,that the game has a fixed length n.
Qn−1
Definition 2.2.2. Let (Xi )n−1
i=0 be an n-tuple of objects, let p :i=0 Xi → R be aQn−1
predicate and φ : i=0 KXi be an n-tuple of quantifiers.
1

We think of the triple ((Xi )n−1
i=0 , p, φ) as a game, or, more precisely, as a finite sequential game with n rounds.
(a) Xi is the set of possible moves at round i.
Qn−1(b) A play is a sequence ~x : i=0 Xi .
(c) p is the outcome function, and p(~x) is the outcome of the play ~x.

2(d) φi : (Xi → R) → R is the outcome quantifier for round i.
Qk−1
Given a partial play ~a : i=0 Xi for k ≤ n, define the sub-game outcome function
Qn−1
p~a : i=k Xi → R by
p~a (xk , . . . , xn−1 ) := p(a0 , . . . , ak−1 , xk , . . . , xn−1 ),or, more concisely,
p~a (~x) := p(~a ∗ ~x),where ∗ denotes concatenation of finite sequences. A partial play ~a defines a sub-gamen−1((Xi )n−1
a , (φi )i=k ),i=k , p~which is like the original game but starts at the position determined by the initialM. Escardó and P. Oliva

8

moves ~a. Notice that if k = n then p is constant, and when k = 0 this is the same as
the full game.
N
n−1
3 The optimal outcome of the game is w :=
φ
(p).
i
i=0
Qk−1
Hence, for any ~a : i=0 Xi ,!
n−1
Ow~a :=
φi (p~a )i=kis the optimal outcome of the sub-game determined by ~a, and of course w = w() . Notethat if k = n then w~a = p(~a), whereas, if k < n, then
!
!
n−1
O
w~a = φk λxk .
φi (p~a∗xk ) = φk (λxk .w~a∗xk ) .
i=k+1

Hence, the optimal outcome of round k is determined by the outcome quantifier for
round k together with a mapping λxk .w~a∗xk computing of the optimal outcome atround k + 1 given what is played at round k.
4 An optimal move ak at round k is a move that forces the optimal outcome at roundk + 1 to be the same as the optimal outcome at round k, i.e. w~a = w~a∗ak .
5 A play ~a = a0 , . . . , an−1 is optimal if each ak is an optimal move in the sub-gamedetermined by a0 , . . . , ak−1 . Hence a play ~a is optimal if and only ifw() = w(a0 ) = w(a0 ,a1 ) = · · · = w(a0 ,...,an−1 ) .
6

A strategy is a family of functions,
nextk :

k−1
Y

Xi → Xk ,i=0

7

with k < n, computing which move should be played at each round k, i.e. when thegame is at position ~a = (ai )k−1a).
i=0 the move selected is ak = nextk (~A strategy is optimal if for every k < n, and every partial play (ai )k−1
i=0 , the movenextk (~a) is optimal at round k, i.e.
w~a = φk (λxk .w~a∗xk ) = w~a∗next(~a) .
Given an optimal strategy, the definition by course of values induction
a0 := next0 (),ak+1 := nextk+1 (a0 , . . . , ak )gives an optimal play.
Note that optimal strategies do not exist in general, but they do if the outcome quantifiers have selection functions in the sense of Section 3 below. In fact, we will show thata suitably defined product of selection functions calculates optimal strategies.
Example 2.2.3. In Example 2.2.1 above, the optimal outcome w of the game tells whichof Eloise and Abelard has a winning strategy. Suppose, however, we choose R = {−1, 0, 1}
instead, with the convention that −1 means that Abelard wins, 0 means that the gameSelection functions

9

is a draw, and 1 that Eloise wins. Replace the existential and universal quantifiers by theminimum and maximum value functionals minX , maxX : (X → R) → R as(
maxXi if i is even,φi =minXi if i is odd.
This is because Eloise tries to maximise the outcome of the game while Abelard tries tominimise the same outcome. If the optimal outcome w is 1, then Eloise has a winning
strategy, if w = −1 then Abelard has a winning strategy, and if w = 0 then both Eloise
and Abelard have strategies for not losing. Any optimal strategy nextk gives the best
moves for Eloise when k is even, and for Abelard when k is odd.

3. Selection Functions for Quantifiers
The main notion investigated in this section is that of a selection function for a quantifier.
Before introducing the notion, we discuss several well-known examples that motivate thegeneral definition.
The mean value theorem asserts that for any continuous p : [0, 1] → R there is a ∈ [0, 1]
such thatZp = p(a).
Similarly, the maximum value theorem says that any continuous p : X → R defined on a
non-empty compact Hausdorff space X attains its maximum value: there is a ∈ X suchthat
sup p = p(a).
And of course this holds for minimum values too: there is a ∈ X such thatinf p = p(a).
If R is the object of truth values of the topos of sets, then for any non-empty set X
and any predicate p : X → R there is a ∈ X such that∀p = p(a).
This is popularly known as the drinker paradox: in any pub X there is a person a suchthat everybody drinks if and only if a drinks, where p(x) is interpreted as the fact that x
drinks. A variation of the drinker paradox is that in any pub X there is a person a suchthat somebody drinks if and only if a drinks. That is, for any p : X → R there is a ∈ Xsuch that p(x) holds for some x if and only if p(a) holds:∃p = p(a).
All of these statements hold in classical logic, but generally fail in intuitionistic logic
or a computational setting. But notice that: (1) the drinker paradox, in its two forms,
holds constructively for non-empty finite sets X, when R is the set of booleans (decidable
truth values). Moreover, in this case, there is a stronger statement: (2) there is a function
ε : (X → R) → X that constructs, from p, the point a at which p attains its φ-value, inM. Escardó and P. Oliva

10

the sense thata = ε(p)solves the equation. Of course, in the category of sets, if the desired a can always befound for any p, then there is a function ε as above that finds it from p, by the axiom of
choice (in fact, this amounts to the axiom of choice).
Definition 3.0.4. Given a quantifier φ : (X → R) → R, any function ε : (X → R) → X
such thatφ(p) = p(ε(p)),
for all p : X → R, is called a selection function for φ. A quantifier that has a selection
function is called attainable.
We refer to φ(p) as the φ-value of p, and say that p attains its φ-value at a if φ(p) = p(a).
With this terminology, ε is a selection function for the quantifier φ if and only if every p
attains its φ-value at ε(p). For our purposes, ε will play the role of providing an algorithm
for computing φ(p) as p(ε(p)). Notice that if the quantifier φ : (X → R) → R is attainable,
then the set X is non-empty, and φ(λx.r) = r for any r ∈ R, because (λx.r)(ε(λx.r)) = r
for any choice of ε.
In the context of games, if X is a set of moves for a particular round, then a selection
function ε : (X → R) → X can be thought of as a policy function, i.e. a function thatchooses a particular move x ∈ X given that the effect of each move on the outcome of
the whole game is known (i.e. X → R). For instance, if the policy of the player is tomaximise its payoff, then ε would be the functional computing the point ε(p) where p
attains its maximum value.
Remark 3.0.5. The paper (Escardó, 2008) defined selection functions for subsets S
of X with R the discrete booleans (two-point space) in a cartesian closed category ofcontinuous functions. Using the language of the above definition, we can formulate thisas follows: a selection function for the set S is a selection function for the boundedexistential quantifier ∃S : (X → R) → R.
We will see in Section 6 that, like KX = ((X → R) → R) defined above, J defined
below gives rise to a monad, and this fact will play an illuminating role in our investigationof quantifiers that have selection functions. Before knowing that J and K are monads,
the following defines a map that will turn out to be a monad morphism.
Definition 3.0.6. For R fixed as above, write JX := ((X → R) → X). For any ε ∈ JX
we define a quantifier ε ∈ KX byε(p) := p(ε(p)).
Thus, every ε ∈ JX is a selection function of some quantifier, and hence we refer to theelements of JX as selection functions.
For selection functions of existential quantifiers, this construction occurs in the paper (Escardó, 2008), in particular in the proof of (Escardó, 2008, Lemma 3.4).

Selection functions

11

3.1. Finite products of selection functions
We now show that attainable quantifiers are closed under finite products. We then develop
technical tools to be used in the applications described in Section 4. In order to establish
preservation of attainability, we define a product of selection functions, which we show
to correspond to the product of its associated quantifiers (cf. Definition 2.1.1).
Definition 3.1.1. Given selection functions ε ∈ JX and δ ∈ JY define a new selection
functionε ⊗ δ ∈ J(X × Y )by(ε ⊗ δ)(p) := (a, b(a))
where
b(x)

:= δ(λy.p(x, y)),a:= ε(λx.p(x, b(x))).

That is, from the relation p : X × Y → R, we get the function b : X → Y by choosing
some y for a given x using the selection function δ. In a finite game of length two, thisfunction gives a strategy for the second player. We can measure the success of the strategy
for any move x ∈ X by evaluating p(x, b(x)). It follows from the definition of δ that
δ(λy.p(x, y)) = p(x, b(x)). This says that for any x ∈ X, the predicate λy.p(x, y) attains
its δ-value at b(x). Now, a as defined above is such that ε(λx.p(x, b(x))) = p(a, b(a)).
Again, this says that the predicate λx.p(x, b(x)) attains its ε-value at a. Putting this all
together we have:
Lemma 3.1.2. ε ⊗ δ = ε ⊗ δ.
Proof. We calculate(ε ⊗ δ)(p) = p(a, b(a)) = ε(λx.p(x, b(x))) = ε(λx.δ(λy.p(x, y))) = (ε ⊗ δ)(p),by simply unfolding the definitions.
Remark 3.1.3. The above definition is equivalent to(ε ⊗ δ)(p) := (a, δ(λy.p(a, y))),where a := ε(λx.δ(λy.p(x, y))), which was the construction in (Escardó, 2008, Proposition 4.4) to show that a finite product of searchable sets is searchable.
Example 3.1.4. Recall the drinker paradoxes for the quantifiers ∀ and ∃, defined above.
Combining the two forms of the paradox with the product operator for selection functions
we get: In any group of people, there are a man a and a woman b such that every man
loves some woman if and only if a loves b. More precisely, for any two non-empty sets X
and Y and any predicate p : X × Y → Ω, there is (a, b) ∈ X × Y such that(∀x ∈ X∃y ∈ Y p(x, y)) = p(a, b).

M. Escardó and P. Oliva

12

In fact, by the two versions of the drinker paradox, the universal and existential quantifiers ∀X and ∃Y have selection functions AX and EY respectively, and hence AX ⊗EY is aselection function for the quantifier ∀X ⊗∃Y , and thus we can take (a, b) = (AX ⊗EY )(p).
Notice that J1 has precisely one element, which is a neutral element for the productNn−1
up to isomorphism. We adopt the notation i=0 εi for the iterated product of selection
functions, as we did for quantifiers. By Lemma 3.1.2 and straightforward induction:
Qn−1
Theorem 3.1.5. For any sequence ε ∈ i=0 JXi of selection functions,
n−1
O

εi =

i=0

n−1
O

εi .

i=0

The following expresses this in terms of attained values, which is useful for the formulation and justification of the applications we have in mind:
Corollary 3.1.6. If εi is a selection function for a quantifier φi , and if we define
E=

n−1
O

εi ,

Φ=

i=0

then every p :

n−1
O

φi ,

i=0

Qn−1

a = E(p), in the sense that
i=0 Xi → R attains its Φ-value at ~Φ(p) = p(~a).

Example 3.1.7. We continue from Example 2.2.1 on two-person games. Let Ai , Ei ∈JXi be selection functions for the quantifiers ∀Xi and ∃Xi respectively, and define((∃Xi if i is even,Ei if i is even,
φi =
εi =
Ai if i is odd,
∀Xi if i is odd.
Qn−1
Nn−1
By Corollary 3.1.6, for any game p : i=0 Xi → Ω, the play ~a := ( i=0 εi )(p) is suchthat Eloise has a winning strategy in the game p if and only if she wins the play ~a, as
this amounts to the equation!
n−1O
φi (p) = p(~a).
i=0Section 3.2 below shows, in particular, that ~a above is an optimal play, and that the
product of selection functions can also be used to compute optimal strategies.
Remark 3.1.8. In several kinds of games, the set of allowed moves at round i+1 depends
on the move played at round i. We can account for this with the following generalisationof the binary product:
1

Given a quantifier φ ∈ KX and family of quantifiers γ : X → KY , define theirdependent product φ ⊗ γ ∈ K(X × Y ) as
(φ ⊗ γ)(p) := φ(λx.γ(x)(λy.p(x, y))),for p : X × Y → R.

Selection functions

13

For example, the combination of quantifiers ∀x ∈ A ∃y ∈ B(x) p(x, y) arises as adependent product φ ⊗ γ, where A ⊆ X and B(x) ⊆ Y for each x ∈ A, and whereφ = ∀A and γ(x) = ∃B(x) .
3 Similarly, given a selection function ε ∈ JX and a family of selection functions δ : X →JY , we define their dependent product as2(ε ⊗ δ)(p) := (a, b(a))
for p : X × Y → R, where

4

b(x)

:= δ(x)(λy.p(x, y)),a:= ε(λx.p(x, b(x))).

Then Lemma 3.1.2 holds for this notion of dependent product, with a routine generalisation of its proof.

3.2. Calculating optimal strategies
Let ((Xi )n−1
i=0 , p, φ) be a game in the sense of Definition 2.2.2, and suppose that eachquantifier φi has a selection function εi . By definition of selection function and of optimal
strategy:
Lemma 3.2.1. The construction
nextk (~x) := εk (λxk .w~x∗xk ),where w~x is defined in 2.2.2(3), gives an optimal strategy.
Recall that the optimal outcome w~x of a sub-game is defined in terms of productsof quantifiers. Our next objective is to calculate this optimal strategy as a product of
selection functions instead. In order to do this, we develop the following two recursive
characterisations of finite products of selection functions, which are interesting on theirown right:
Lemma 3.2.2.
n−1
O

!
εi

n−1
O

(p) = ak ∗

i=k

!

!

εi

(pak ) ,

!

!!

i=k+1

where
ak = εkn−1O

λxk .pxk

εi(pxk ),

i=k+1

Proof. This follows directly from Remark 3.1.3, taking X = Xk , Y =Nn−1
ε = εk and δ = i=k+1 εi , a = ak .
Lemma 3.2.3.
n−1
O
i=0

!
εi

(p) = ~aQn−1

i=k+1 Xi ,

M. Escardó and P. Oliva

14

where ~a is given by course of values recursion as
ak

= εk

n−1
O

λxk .pa0 ,...,ak−1 ,xk

!
εi

!!
pa0 ,...,ak−1 ,xk



i=k+1

= εk (λxk .wa0 ,...,ak−1 ,xk ).
Proof. The first equation follows by Lemma 3.2.2 and course of values induction. By
the assumption that εi is a selection function for the quantifier φi and Theorem 3.1.5,
Qk−1
the optimal outcome of the game that starts at position ~x ∈ i=0 Xi can be calculated
as
!
!
n−1
O
w~x = p~x
εi (p~x ) ,i=kwhich gives the second equation.
By Lemmas 3.2.2 and 3.2.3 we get:
Theorem 3.2.4. The optimal-strategy functions nextk constructed in Lemma 3.2.1 canbe calculated as
!
!
n−1
O
nextk (~x) :=εi (p~x ) .
i=k0

Moreover,1

The whole sequence
~a =

n−1
O

!
εi

(p~x )

i=k2

is an optimal play for the game that starts at position ~x.
The predicates pk : Xk → R defined bypk (xk ) = wa0 ,...,ak−i ,xk = pa0 ,...,ak−1 ,xk

n−1
O

!
εi

!
pa0 ,...,ak−1 ,xk



i=k+1

satisfyεk (pk ) = ak ,pk (ak ) = pj (aj ).

for all k, j < n.
Theorem 3.2.4(2) says that the optimal move ak can be computed from the selection
function εk and the mapping λxk .wa0 ,...,ak−1 ,xk of possible moves at round k to optimal
outcomes at round k + 1.

3.3. Implementation of the finite productThe computation of finite products of selection functions can be easily implemented inhigher-type functional programming languages such as Haskell (Hutton, 2007) in the case
all types Xi are the same and equal to X.

Selection functions

15

type J r x = (x -> r) -> xotimes :: J r x -> J r [x] -> J r [x](epsilon ‘otimes‘ delta) p = a : b(a)where b(x) = delta(\xs -> p(x : xs))a = epsilon(\x -> p(x : b(x)))
bigotimes :: [J r x] -> J r [x]bigotimes [] = \p -> []bigotimes (epsilon : epsilons) =epsilon ‘otimes‘ (bigotimes epsilons)
We are using lower case letters r and x for R and X due to Haskell’s syntacticalrequirements. In Haskell, a finite list of length n is written[x0 , x1 , . . . , xn−1 ] = x0 : x1 : · · · : xn−1 : [],where [] is the empty list. The operator otimescomputes thebinary product of a selection
Nn−1 
function ε : JX0 with a selection function δ : J
i=1 Xi , obtaining a selection function
N

n−1
in J
i=0 Xi , and the function bigotimes iterates this finitely often. List types in
Haskell actually include infinite lists, and we will see in Section 5 that this algorithm
in fact works for infinite lists of selection functions as well (and corresponds to a formof bar recursion). Dependently typed languages such as Agda (Bove and Dybjer, 2008)
allow the types Xi to be distinct, with a similar recursive definition.

4. Applications
In this section we show that finite products of selection functions appear in many guises
in different areas, such as game theory, fixed point theory, proof theory and algorithms.

4.1. Game theory
Consider a sequential game with n players (say 0, 1, . . . , n − 1) and n rounds, withplayer i picking his move at round i from a fixed set Xi . In standard game theory, a play(x0 , . . . , xn−1 ) ∈ Πn−1
i=0 Xi (cf. Definition 2.2.2) is also known as a strategy profile, andnoutcome functions p : Πn−1
i=0 Xi → R are called payoff functions, since p(x0 , . . . , xn−1 ) =(v0 , . . . , vn−1 ) gives the payoff each player gets at the end of all rounds. Each player istrying to maximise their payoff, so the outcome selection functions εi : (Xi → Rn ) → Xiare
εi (q) := x ∈ Xi such that (qx)i ≥ (max{(qx)i : x ∈ Xi })where q : Xi → Rn . Finally, an optimal play is a strategy profile where each player has
maximised their possible payoff, relative to the choice of the other players.

M. Escardó and P. Oliva

16

Theorem 4.1.1. The optimal play
~x :=

n−1
O

!
εi

(p)

i=0

is a strategy profile in Nash equilibrium.
By the definition of Nash equilibrium, it is enough to note that the optimal strategyfunction nextk (x0 , . . . , xk−1 ) computes the move for player k (in the sub-game px0 ,...,xk−1 )maximising his payoff, given that all the following players are playing optimally. Hence,
once an optimal play has been obtained, any change of move from either player individually cannot result in a better payoff for that player.
The above construction can be viewed as a formal description of backward induction,a technique used in Game Theory (Nisan et al., 2007) to compute Nash equilibria insequential games. Intuitively, backward induction is explained as follows: An equilibrium
strategy profile is computed by inductively pruning branches of the game tree. Startingfrom the last player, we pick in each sub-tree only the branch which would be selectedby the last player if that sub-game is reached. The same is then done for each player inturn, in reverse order. We end up with just one branch left which by construction is an
optimal play.
4.2. Fixed point theory
A map fix : (R → R) → R is a called a fixed point operator if fix(p) is a fixed point of pfor every p : R → R, i.e.,fix(p) = p(fix(p)).
For non-trivial fixed point operators to exist, we must work in a cartesian closed category
other than that of classical sets, as for every set, except the one-point set, there is an endofunction with no fixed point. Well known examples are various categories of domains.
Now, JR = KR = ((R → R) → R), and hence a fixed point operator can be consideredboth as a selection function and as a quantifier. Moreover, f : (R → R) → R is a fixed
point operator if and only if it is its own selection function, as this amounts tof (p) = f (p) = p(f (p)).
Bekič’s Lemma (Bekič, 1984) says that if X and Y have fixed point operators, then sodoes X × Y , and moreover explicitly constructs a fixed point operator for the productfrom given fixed point operators for the factors. We now show that Bekič’s construction
arises as a product of suitable selection functions:Lemma 4.2.1. If X and Y have fixed point operators fixX and fixY , then X × Y has afixed point operator fixX×Y ∈ J(X × Y ), with R = X × Y , given by
fixX×Y := εX ⊗ δY ,where we define the selection functions ε ∈ JX and δ ∈ JY (also with R = X × Y ) byεX (p) := fixX (πX ◦ p),

δY (q) := fixY (πY ◦ q).

Selection functions

17

Here πX : X × Y → X and πY : X × Y → Y are the projections.
The selection functions ε and δ are not fixed point operators themselves, nor are thederived quantifiers φ = ε ∈ KX and γ = δ ∈ KY . But, by Theorem 3.1.5 that givesε ⊗ δ = φ ⊗ γ, and by the facts that J(X × Y ) = K(X × Y ) for R = X × Y , and that
fixX×Y is a fixed point operator if and only if it is its own selection function, we conclude
from Lemma 4.2.1 that fixX×Y is also given as a product of quantifiers:
fixX×Y = φ ⊗ γ.
For the proof of Lemma 4.2.1, however, again in view of Theorem 3.1.5, it is enoughto conclude thatε ⊗ δ = φ ⊗ γ,
where of course the left product is of selection functions and the right one is of quantifiers,
because then fixX×Y is its own selection function and hence is a fixed point operator.
Indeed, when applied to a function r = (s, t) : X ×Y → X ×Y , both sides of the equation
reduce to the same term, namely (a, b) witha=fixX (λx.s(x, fixY (λy.t(x, y)))),

b=

fixY (λy.t(a, y)).

This is Bekič’s formula for calculating a fixed point (a, b) of the function r. Of course, here
we are using the fact that any r : X × Y → X × Y is of the form (s, t) with s : X × Y → X
and t : X × Y → Y ,r(x, y) = (s(x, y), t(x, y)),by considering s = πX ◦ r and t = πY ◦ r.
Notice that there is an asymmetry in the definitions of a and b. If we switch theroles of a and b (and of s and t), another fixed-point operator is obtained. We have notinvestigated the relationship between these two fixed-point operators, but we suspectthey do not coincide in general. As is well known in domain theory (and first observedby Bekič), however, if X and Y are objects of a category of domains and continuousfunctions, and fixX and fixY are the least fixed-point operators, then either construction
produces the least fixed-point operator of the product domain X × Y , and hence the twoconstructions coincide.
By Lemma 4.2.1 and induction:
Qn−1
Theorem 4.2.2. If Xi for 0 ≤ i < n has a fixed point operator fixi , then i=0 Xi
Qn−1
Qn−1
has a fixed point operator fix ∈ J( i=0 Xi ), with R = i=0 Xi , given as a product of
selection functions,
fix =

n−1
O

(λpi . fixi (πi ◦ pi )),i=0where πi is the projection of the product into Xi .

M. Escardó and P. Oliva

18

4.3. Proof theory
Uses of the product of selection functions in proof theory will be further discussed in Section 5.7, where we explain how this construction is related to the so-called bar recursion.
In this section we look at a simple example, where the computational interpretation ofa non-computational principle can be explained again in terms of products of selection
functions. The principle we consider is the infinite pigeon-hole principle, which says thatfor any finite set n = {0, 1, . . . , n−1} of colours and any colouring of the natural numbers,some colour occurs infinitely often:∀n : N ∀f : N → n ∃k ∈ n ∀i ∃j ≥ i(f j = k).
This is non-computational, in the sense that, given n and f , we cannot effectively produce the colour k which is used infinitely often. We look, therefore, at the dialectica
interpretation (Avigad and Feferman, 1998) of its negative translation, i.e.
∀n : N ∀f : N → n(¬¬∃k ∈ n ∀i ∃j ≥ i(f j = k)).
The dialectica interpretation of this is∀n : N ∀f : N → n ∀ε : n → (NN → N) ∃k ∈ n ∃p : N → Np(εk (p)) ≥ εk (p) ∧ f (p(εk (p))) = k,i.e. given n, f and a sequence εi , we must find k and p such thatp(εk (p)) ≥ εk (p) ∧ f (p(εk (p))) = k.
Intuitively, the function p is trying to compute a value j which makes the statement
true (i.e., selection function for existential quantifier in ∃j ≥ i(f j = k)), whereas thefunctional εk tries to produce a counter-example i given any such p and fixed colour k(i.e., selection function for universal quantifier in ∀i(pi ≥ i ∧ f (pi) = k)). The above
constructive version of the infinite pigeon-hole principle says that given a partition fof the natural numbers into n sets, and given n (counter-example) selection functions
ε0 , . . . , εn−1 , one for each colour, we can always find k < n and pk , such that εk is not
successful in finding a counter-example, i.e. pk (εk (pk )) = k.
But, again, we can also view the above as an instance of our general notion of sequential
game (Definition 2.2.2). Consider the game where Xi = R = N, and max : Nn → N is theoutcome function, and φk (p) = p(εk p) is the outcome quantifier for round k. We show
how the above computational interpretation of the infinite pigeonhole principle can berealized from the optimal play in this sequential game. Note that although this is a finite
game, with n rounds, we have at each round k an infinite number of possible moves as
Xk = N.
Theorem 4.3.1. Let n, f and εi be given. Define
!
n−1
O
~x :=
εi (max).
i=0Selection functions

19

Then, for all k < n we have pk (xk ) ≥ xk , and for some k < n we havef (pk (εk (pk ))) = k,where
pk (y) :=

n−1
O

max

x0 ,...,xk−1 ,y

i=k+1

!
εi

!
max

x0 ,...,xk−1 ,y.

In fact, by Theorem 3.2.4, xk = εk (pk ), for all k < n. Hencepk (xk ) = max{x0 , . . . , xn−1 },and pk (xk ) ≥ xk , for all k < n. It remains to show that f (pk (εk (pk ))) = k for some k,
but this follows from the fact that pk (εk (pk )) = pk (xk ) is the same for all k < n, again
by Theorem 3.2.4.
Remark 4.3.2. A similar calculation was performed in (Oliva, 2006), but using a finite
version of Spector’s bar recursion (cf. Section 5.7) instead of finite products of selection
functions.

4.4. Algorithms
Products of selection functions also correspond to the algorithmic technique of backtracking. For instance, if each εk : (B → B) → B is a selection function for the boolean
existential quantifier, and p(x0 , . . . , xn−1 ) is a decidable predicate on n-boolean variables,
then
!
n−1
O
εi (p)
i=0

computes an assignment which makes p true, if p is satisfiable.
The same construction can also be used to compute a shortest path between two nodes
in a given weighted directed graph, where in this case the quantifiers are the minimum
functionals. Let X be a finite set of vertices, and d : X ×X → R be the weighted incidence
matrix of the directed graph, with d(x, x) = 0, where R = [0, ∞]. If d(x, y) = ∞ thismeans that there is no edge from node x to node y; otherwise this gives the weight ofthe edge from x to y. Let n be the cardinality of X, and let Xi = X for i < n. Define
the quantifiers φi : (Xi → R) → R asφi (p) := min p = min{p(x) : x ∈ Xi },and let εi be a selection function for φi . So we have a constant sequence of quantifiers,and of selection functions. The length of a path x0 , . . . , xk−1 is defined as d(x0 , x1 ) +. . . + d(xk−2 , xk−1 ). If this is different from ∞, and if xi 6= xj for i 6= j, we call this aproper path. Given vertices u and v, define q : X n → R byq(x0 , . . . , xn−1 ) := if there is k < n such that u, x0 , . . . , xk , v is a proper path thenthe length of such path for the smallest k else ∞.

M. Escardó and P. Oliva

20

Theorem 4.4.1. A shortest path, or the non-existence of a path from u to v, can beread off from
!
n−1
O
~a :=
εi (q).
i=0

More precisely, if q(~a) = ∞ then v is not reachable from u; otherwise look for the smallest
k < n such that d(ak , v) 6= ∞, and the shortest path from u to v is u, a0 , . . . , ak , v.
In fact, by simultaneous induction on n − k − 1,!
n−1Oεi (qa0 ,...,ak−1 )i=kcalculates the shortest way to link the path u, a0 , . . . , ak−1 to the node v, and!
n−1O
qa0 ,...,ak−1 ,ak
εi (qa0 ,...,ak−1 ,ak )
i=k+1

calculates the length of any such shortest way.
Note that this solution corresponds to computing a shortest path via backtracking withpruning, which is less efficient than Dijkstra’s algorithm. The tree over which backtracking is performed is based on the order in which the predicate q queries its arguments.
Also, the pruning takes place whenever q finds that the argument x0 , x1 , . . . , xk is not
a proper path by only looking at a few positions, and hence speeding up the backtracking (cf. (Escardó, 2007)). In fact, the product of selection functions behaves as such ingeneral, including all applications mentioned above.
Note also that, alternatively, we could use the dependent version of the product of
selection functions (Remark 3.1.8) to ensure that the next element added to the path isconnected to the previous one, and has not been visited before, meaning that only proper
paths are considered.

5. Infinite Products of Selection Functions
In (Escardó, 2008, Definition 4.5), a functionalΠ : ((D → B) → D)ω → ((Dω → B) → Dω )is constructed, where D is a domain and B is the lifted domain of booleans. Using ournotation and choosing R = B, the type definition of this functional can be written asΠ : (JD)ω → JDω .
It is proved in (Escardó, 2008, Theorem 4.6) that, given ε ∈ (JD)ω such that εi ∈ JD is aselection function for an existential quantifier ∃Si , with Si ⊆ D, it holds that Π(ε) ∈ JDω
Q
is a selection function for the existential quantifier ∃Πi Si of the set i Si ⊆ Dω .

Selection functions

21

5.1. Generalisation of the product functional
We rework the product functional Π in a number of ways. Firstly, we work with an infinite
sequence Xi of spaces rather than a single domain D, and we replace the countableQ
product (JD)ω by the dependent product i JXi . To be consistent with our notation,N
we rename the functional to , and give it the type
!
O Y
Y
:
JXi → J
Xi .
i

i

Secondly, we allow R to be any discrete space, not just the booleans. In the infinite
case, the assumption that R be discrete is essential (Remark 5.5.8). Thirdly, we showQ
that, more generally, given ε ∈ i JXi such that εi ∈ JXi is a selection function for aNQquantifier φi ∈ KXi , it holds that i εi ∈ J ( i Xi ) is a selection function for a suitablyNQ
defined quantifier
i φi ∈ K ( i Xi ). Lastly, we observe that the recursive definitionNof the Π functional given in (Escardó, 2008, Section 8.1, page 30), here written
asexplained above, can be written asOOεi = ε0 ⊗
εi+1 ,ii

and hence the infinite version can be seen as simply the iteration of the binary versionof the product of selection functions. We also show that the analogous equationOO
φi = φ0 ⊗
φi+1
i

i

holds for attainable quantifiers, but unfortunately does not characterise infinite productsof quantifiers in general.
We will see in Section 5.5 that these equations for infinite products can be understoodas definitions by bar recursion, introduced in Section 5.4. We first discuss the spaces towhich the development discussed above applies (Section 5.2), and observe that infinite
sequential games, in the continuous case, amount to finite games of unbounded length(Section 5.3).
5.2. A convenient category of spaces and domains
In order to be able to form the required function spaces for the product functional, we
work in a cartesian closed category of continuous maps of topological spaces closed under countable products. The largest such category for we which are able to prove ourmain results is that of continuous maps of QCB spaces (Battenfeld et al., 2006; Battenfeld et al., 2007). Such spaces are precisely the T0 topological quotients of countably
based spaces, and can be characterised in a number of ways, such as, among others:(i) the sequential T0 spaces with countable pseudo-bases, or (ii) the sequential T0 spaces
with admissible quotient representations, (iii) a certain full subcategory of the category PER(ωAlgLat), whose objects are countably based algebraic lattices with a partial
equivalence relation, and whose morphisms are Scott continuous maps that preserve theequivalence relation (Bauer, 2002). QCB spaces admit a theory of computability, and,

M. Escardó and P. Oliva

22

as shown by (Escardó et al., 2004), have some well-known cartesian closed subcategories
closed under countable products, such as (i) Kleene–Kreisel continuous functionals, and(ii) Ershov–Scott continuous functionals. Hence, in particular, they simultaneously account for total and partial computation. For some lemmas, we allow k-spaces (also known
as compactly generated spaces), which contain QCB as a full subcategory closed underfinite and countable products and function spaces (Escardó et al., 2004), as the restriction
to QCB spaces would be artificial and serve no purpose.
5.3. Finite games of unbounded length
In a topological setting, the move from finite to countable products corresponds to themove from finite games of fixed length to finite games of unbounded length. In order toQ
see this, notice that if a discrete-valued function p : i Xi → R is continuous, then forQ
any sequence α ∈ i Xi , the value p(α) depends only on a finite prefix of the sequence α.
Q
Formally, for α, β ∈ i Xi and n ≥ 0, define
α =n βiff αi = βi for all i < n.
Q
If p is continuous then for every α ∈ i Xi there is some n such thatp(β) = p(α) for all β =n α.
QDenote by nα the smallest such n. If p : i Xi → R is the outcome function of a game,then continuity of p implies that the outcome of every infinite play is determined by afinite prefix of the play. In this case, we may say that the play α terminates in nα rounds.
It is in this sense that, by considering continuous outcome functions, we move from finite
games of fixed length to finite games of unbounded length.
5.4. Bar induction
Q
A continuous discrete-valued continuous function p : i Xi+n → R can be regarded asa well-founded tree as follows. The root of the tree is the only node of level 0. Eachnode of level i is either a leaf labelled by an element of R, or else has one branch foreach point of Xi+n , leading to a node of level i + 1. The well-foundedness condition saysthat each maximal path of the tree starting from the root is finite and hence eventuallyQreaches a leaf. For each α ∈ i Xi+n , the finite prefix of α of length nα (defined in
Section 5.3) gives a maximal path ending at a leaf labelled by the value p(α), and all
maximal paths of the tree are of this form. Hence if p is constant then it is seen as asingleton tree consisting of just a leaf, and otherwise the subtree of p that follows theQ
branch xn ∈ Xn is that corresponding to the predicate pxn : i Xi+n+1 → R. Intuitively,Q
to evaluate p(α) for any given α ∈ i Xi+n , one follows the branches α0 , α1 , . . . until aleaf is reached, whose label gives the value p(α). Notice that different trees can give riseto the same continuous function. The procedure described above builds the optimal tree,corresponding to the optimal modulus of continuity α 7→ nα of the function p.
The following is a counter-part of induction on well-founded trees, and is well knownin various guises and particular situations:Selection functions

23

Lemma 5.4.1 (Bar induction). Let Xi be a sequence of k-spaces and R be discrete,and consider a sequence of sets!
Y
An ⊆ Pn :=Xi+n → R ,iwhere the product and exponential are calculated in the category of k-spaces. If for all n,
12

the constant functions are in An , andfor all p ∈ An , the condition ∀x ∈ Xn (px ∈ An+1 ) implies p ∈ An ,then An = Pn for all n.
Proof. Suppose that for some n, there is p ∈ Pn such that p 6∈ An . Then, by theassumption, there is some αn such that pαn 6∈ An+1 . Proceeding in the same manner,Q
we get an infinite sequence α ∈ i≥n Xi such that pαn ,αn+1 ,...,αk 6∈ An+k+1 for every k.
But, by continuity, pαn ,αn+1 ,...,αk is constant for some k, and hence is in An+k+1 by
assumption, which is a contradiction.
We now consider definitions of continuous functionals hn : Pn → Yn by bar recursion (Normann, 1999, Section 6), where the spaces Pn are as in Lemma 5.4.1 and thespaces Yn are arbitrary. Given Ln : R → Yn and Bn : Pn × (Xn → Yn+1 ) → Yn , weconsider the equations
hn (λα.r)hn (p)= Ln (r),= Bn (p, λx.hn+1 (px )).

The intuitive idea is that the base case Ln accounts for leaves and the recursion step Bn
for branches. By bar induction, one easily sees that there is at most one such function hn .
Of course, one cannot continuously test whether a function is constant or not, and hence
there is no guarantee that there is a continuous solution. Moreover, the second equation
also applies to the case when p is the constant function λα.r, where we get, using both
equations and the fact that (λα.r)x = λβ.r,
Ln (r) = hn (λα.r) = Bn (λα.r, λx.hn+1 (λβ.r)) = Bn (λα.r, λx.Ln+1 (r)).
Now, by bar induction, one easily sees that:
Lemma 5.4.2. Let Bn : Pn × (Xn → Yn+1 ) → Yn be a family of continuous maps. If forevery r ∈ R there is at most one sequence Ln (r) ∈ Yn such thatLn (r) = Bn (λα.r, λx.Ln+1 (r)),
then there is at most one family of continuous functions hn : Pn → Yn such thathn (p) = Bn (p, λx.hn+1 (px )),which automatically satisfy hn (λα.r) = Ln (r).
Definition 5.4.3. We refer to the system of equations hn (p) = Bn (p, λx.hn+1 (px )) as a
specification of hn by bar recursion.

M. Escardó and P. Oliva

24

The advantage of this recursion scheme is that it has only one equation and hence avoids
the non-continuous case distinction discussed above. Notice that we do not require thatthe conditions of Lemma 5.4.2 hold, and hence a specification by bar recursion can havezero, one or more continuous solutions.
5.5. The infinite product as the iteration of the binary product
The functional equation that defines the functional Π : (JD)ω → JDω in (Escardó, 2008,
Section 8.1, page 30) isΠ(ε)(p) = x0 ∗ Π(ε0 )(px0 ) where x0 = ε0 (λx.px (Π(ε0 )(px ))),
and where ε0 is the sequence ε with its first term ε0 removed, i.e. ε0i = εi+1 . This can beequivalently written asΠ(ε)(p) = x0 ∗ b(x0 ),whereδ = Π(ε0 ),b(x) = δ(λα.p(x ∗ α)),x0 = ε0 (λx.p(x ∗ b(x))).

In turn, this can be written asΠ(ε) = ε0 ⊗ Π(ε0 ),if, as in Section 3.3, we consider the variation of the finite product ⊗ that given two
QQ
selections functions ε ∈ JX0 and δ ∈ J ( i Xi+1 ), produces ε ⊗ δ ∈ J ( i Xi ). Thisvariation is given by(ε ⊗ δ)(p) = x0 ∗ b(x0 ),where b and x0 are defined as above.
Remark 5.5.1. Equivalently, to define the variation of the binary product, we canQQconsider the isomorphism X0 × i Xi+1 → i Xi defined by (x, α) 7→ x ∗ α. In fact,
because, as established in Section 6 below, J is a functor, we get an isomorphismQ
Q
Q
J (X0 × i Xi+1 ) → J ( i Xi ). Then the original product ε ⊗ δ ∈ J (X0 × i Xi+1 )gives the above variation after the application of this last isomorphism:
!
!
Y

Y
Y
∼
⊗
=
JX0 × J
Xi+1 −→ J X0 ×
Xi+1 −→ J
Xi .
i

i

N
It is thus natural to attempt to define , in the generality discussed in Section 5.1, asa solution to the functional equation F (ε) = ε0 ⊗ F (ε0 ). The above equations for Π makesense because it was assumed that Xi = D, for every i. But if we assume the type of F
Q
Q
in the left-hand side of the above equation to be i JXi → J ( i Xi ) , then this forcesQQ
the type of F in the right-hand side to be i JXi+1 → J ( i Xi+1 ) . Hence we instead
consider the system of equations
Fn (ε) = ε0 ⊗ Fn+1 (ε0 ),QQwith the continuous unknowns Fn : i JXi+n → J ( i Xi+n ) . We now show that if Xi
and R are QCB spaces with R discrete, there a unique solution, using bar recursion.

Selection functions

25

Lemma 5.5.2. Assume that Xi and R are k-spaces with R discrete, and fix a sequence
εi ∈ JXi of selection functions. The system of equations

with the unknowns δn ∈ Jof the form

δn = εn ⊗ δn+1
i+n Xi is equivalent to a specification of δn by bar recursionQδn (p) = Bn (p, λx.δn+1 (px )).
Moreover, there is at most one solution, and if it exists then it satisfiesδn (λα.r)(i) = εi+n (λx.r).
Construction. Define Bn : Pn × (Xn → Yn+1 ) → Yn by
Bn (p, f ) = xn ∗ f (xn ),where Yn =where xn = εn (λx.p(x ∗ f (x))),Q

i Xi+n and Pn = (Yn → R).

Q
Proof. Because (Pn → Yn ) = J ( i Xi+n ), we have that δn : Pn → Yn , andBn (p, λx.δn+1 (px ))= xn ∗ b(xn ),where b(x) = δn+1 (px ) and xn = εn (λx.p(x ∗ b(x)),=(εn ⊗ δn+1 )(p).

Hence the equations δn (p) = Bn (p, λx.δn+1 (px )) are equivalent to δn = εn ⊗δn+1 . Because
xn = εn (λx.r) if p = λα.r, the equations Ln (r) = Bn (λα.r, λx.Ln+1 (r)) amount to
Ln (r) = εn (λx.r) ∗ Ln+1 (r). But there is a unique sequence Ln (r) ∈ Yn that satisfies
this, namely Ln (r)(i) = εi+n (λx.r), and hence the result follows from Lemma 5.4.2.
We emphasise that the next construction is not a specification by bar recursion, because
a domain cannot be discrete, except in the uninteresting case it is the one-point space,and hence the two equations do not uniquely characterise δn . But if R is e.g. a lifteddiscrete space, this of course comes very close to a specification by bar recursion, which
is what the proof of Theorem 5.5.4 exploits.
Lemma 5.5.3. If Xi and R are domains, then for every sequence of selection functionsQ
εi ∈ JXi , there is a sequence of selection functions δn ∈ J ( i Xi+n ), continuously in ε,such that, for all n,δn (λα.r)=

λi.εi+n (λx.r),

δn (p)=Bn (p, λx.δn+1 (px )),where Bn is defined in the construction of Lemma 5.5.2.
Q
Q
Proof. Let F = n (Pn → Yn ) = n J(Yn ), and define H : F → F by
H(h)(n)(p) = Bn (p, λx.hn+1 (px )).
F
Then H is continuous and hence has a fixed point δ = k H k (⊥) with δn : Pn → Yn , because F is a domain. Then δn (p) = Bn (p, λx.δn+1 (px )) holds by construction. Moreover,M. Escardó and P. Oliva

26

clearly Bn depends continuously on εn , and hence so do H and its least fixed point δ.
By induction on k,(
εi+n (λx.r) if i < k,kH (⊥)(n)(λα.r)(i) =⊥if i ≥ k,F
and hence δn (λα.r)(i) = k H k (⊥)(n)(λα.r)(i) = εi+n (λx.r), as claimed.
We do not know whether the following theorem holds more generally for k-spaces.
Theorem 5.5.4. If Xi and R are QCB spaces with R discrete, then for any sequenceQεi ∈ JXi , there is a unique sequence δn = δn (ε) ∈ J ( i Xi+n ) such that, for all n,
δn = εn ⊗ δn+1 .
Moreover, δn (ε) is continuous in ε.
Proof. We use the fact that QCB is fully and faithfully embedded into PER(ωAlgLat)
as described in (Bauer, 2002). The embedding transforms Xi and R into objects (|Xi |, ∼i )and (|R|, ∼R ). It also gives Scott continuous functions |εi | : (|Xi | → |R|) → |Xi | that preserve ∼, because the embedding preserves function spaces. Then we can apply Lemma 5.5.3
to the domains |Xi | and |R| under the Scott topology, and to the selection functions |εi |,to get selection functions |δn |. Using the two equations of Lemma 5.5.3 as the base caseand induction step of an argument by bar induction on p, one sees that for all n andQp ∈ Pn , if so , s1 : n |Xi+n | → |R| track p, then |δn |(s0 ) ∼ |δn |(s1 ). Hence s0 ∼ s1
implies |δn |(s0 ) ∼ |δn |(s1 ), and so |δn | is a morphism of PER(ωAlgLat), which then gives
a morphism δn of QCB, because the embedding of QCB into PER(ωAlgLat) is full.
Notice that the assumption of discreteness of R is used twice in this proof, so thatbar induction can be applied to (1) establish that there is at most one solution in
Lemma 5.5.2, and (2) prove totality of the functional constructed in Lemma 5.5.3. As
discussed in Remark 5.5.8 below, such an assumption is essential.
Lemma 5.5.5. Under the assumptions and notation of Theorem 5.5.4, and additionally(k)defining εi := εk+i we haveδn ε(k) = δn+k (ε).
Proof. If we apply Theorem
5.5.4 to the sequences ε and ε(k) , we get sequences δn =

(k)
(k)
δn (ε) and ζn = δn εthat satisfy δn = εn ⊗ δn+1 and ζn = εn ⊗ ζn+1 = εn+k ⊗ ζn+1 .
But the sequence δn+k also satisfies the second equation, and hence, by uniqueness,ζn = δn+k , which amounts to the statement of the lemma.
Corollary 5.5.6. The equation Fn (ε) = ε0 ⊗ Fn+1 (ε0 ) has
 a unique continuous solution
Q
Q
Fn : i JXi+n → J ( i Xi+n ), namely Fn (ε) = δ0 ε(n) .
Proof. This equation amounts to δ0 (ε(n) ) = ε0 ⊗ δ0 (ε(n+1) ), which in turn amounts toδn (ε) = ε0 ⊗ δn+1 (ε) by Lemma 5.5.5, and holds uniquely by Theorem 5.5.4.

Selection functions

27

Definition 5.5.7. For any sequence εi ∈ JXi , we write
lary 5.5.6, this is characterised asOOεi = ε0 ⊗
εi+1 .
iNi εi := δ0 (ε). Then, by Corol-iRemark 5.5.8. The assumption that R be discrete is essential. If R = (N → N) and
Xi = N, for instance, we could take p(α)(m) = α(m) + 1 and εn (q) = q(0)(n + 1). In thiscase our equation would imply
δ0 (p)(0) = x0 = ε0 (λx.p(x ∗ b(x))) = p(0 ∗ b(0))(1) = b(0)(0) + 1 = δ1 (p0 )(0) + 1,
and by induction δ0 (p)(0) = δn (p0n )(0) + n, for all n, and hence there is no solution
δn for the equation of Theorem 5.5.4. This is adapted from a similar counter-examplein (Berger and Oliva, 2005). Note, however, that for specific families εn and R nondiscrete, a solution may exist, e.g. if εn are constant functions. But notice that, by virtueof the previous counter-example, the equation of Corollary 5.5.6 cannot have a solution
if R = (N → N).
5.6. Infinite products of quantifiers
We now proceed to the definition of infinite products of quantifiers, which turns out tobe subtler. Any such notion ought to satisfy, in particular,OOOO
inf = Qinf
∃Xi = ∃Qi Xi ,∀Xi = ∀Qi Xi ,sup = Qsup ,
i

i

i

Xi

i Xi

i

Xi

i Xi

when these quantifiers exist for suitable choices of R. We have seen that the selection
NN
function i εi is continuous in the sequence ε. However, such a quantifier i φi cannot
be continuous in φ. In fact, consider the particular case in which φi is the boolean-valued,Qbounded existential quantifier ∃Si for a finite subset Si of Xi . Then i Si is empty if
and only if Si is empty for some i. But an empty set may be present arbitrarily far awayNin the sequence Si , and hence ( i ∃Si ) (p) depends on the whole sequence ∃Si , which
violates continuity. In connection with this, we observe, for future reference, that thebounded existential quantifier of the empty set is not attainable.
It is thus natural to attempt to define infinite products of quantifiers φi ∈ KXi by
mimicking Theorem 5.5.4 but giving up continuity of the formation of the product.
Consider the system of equations
γn = φn ⊗ γn+1
Qwith the unknowns γn ∈ K ( i Xn+i ). This system of equations can be put in bar
recursive form
γn (p) = Bn (p, λx.γn+1 (px )),for a suitable Bn . In fact, because
γn (p)=(φn ⊗ γn+1 )(p) = φn (λx.γn+1 (λα.p(x ∗ α))= φn (λx.γn+1 (px ))M. Escardó and P. Oliva

28

we can (and are forced to) defineBn (p, f ) = φn (f ).
Now the equation Ln (r) = Bn (λα.r, λx.Ln+1 (r)) amounts to
Ln (r) = φn (λx.Ln+1 (r)).
If e.g. Xi = R = N and φi (q) = q(0) + 1, then this equation reduces to Ln (r) =Ln+1 (r) + 1, and, by induction, Ln (r) = Ln+k (r) + k for every k, which is impossible andhence shows that there is no sequence γn such that γn = φn ⊗ γn+1 . Thus, in general,
the infinite iteration of the finite product of quantifiers fails to exist.
Now, by the discussion that follows Definition 3.0.4, if the quantifiers φn are attainable, then φn (λx.r) = r, and hence the above constraint on the sequence Ln amounts
to Ln (r) = Ln+1 (r), i.e. Ln can be any constant sequence. Then Lemma 5.4.2 is notapplicable, and, moreover, even if the equation γn = φn ⊗ γn+1 has a solution, all it says
about γn (λα.r) is that it must be a constant sequence Ln (r). But if γn itself is required
to be attainable, then γn (λα.r) = r. Hence, by bar induction, using this for the base caseand γn (p) = Bn (p, λx.γn+1 (px )) for the inductive step, we see that if the quantifiers φiare attainable, then the system of equations γn = φn ⊗ γn+1 has at most one attainable
solution.
Theorem 5.6.1. For every sequence of attainable quantifiers φi ∈ JXi , there is a uniqueQ
sequence of attainable quantifiers γn ∈ J ( i Xi+n ) such that, for all n,γn = φn ⊗ γn+1 .
Proof. It remains to establish existence. Let εi be a selection function for the quantifier φi . By Theorem 5.5.4, there is a unique sequence δi such that δn = εn ⊗ δn+1 . Taking
γn = δn , Theorem 3.1.5 gives γn = εn ⊗ δn+1 = εn ⊗ δn+1 = φn ⊗ γn+1 , as required.
N
If we define i φi = γ0 , under the assumptions of this theorem, then, by construction,OOOO
φi = φ 0 ⊗φi+1 ,
εi =
εi .
i

i

i

i

In particular, we do have that, as required above, for suitable choices of R discrete,O
O
OO∃Xi = ∃Qi Xi ,∀Xi = ∀Qi Xi ,sup = Qsup ,inf = Qinf ,
i

i

i

Xi

i Xi

i

Xi

i Xi

provided the quantifiers of the left-hand sides of the equations exist and are attainable.
Question 5.6.2. By (Escardó, 2008, Theorem 6.3), if R = B, if X is a space of Kleene–
Kreisel functionals, and if ∅ =6 S ⊆ X has a quantifier ∃S ∈ KX, then ∃S has a selection
function continuously in ∃S . By (Escardó, 2008, Lemma 5.5), such a set S has a quantifier∃S ∈ KX if and only if it is compact. We remark that the universal quantifier ∀S iscontinuously interdefinable with the quantifier ∃S , and that ∃S = supS and ∀S = inf S
for the case R = B with false < true. We highlight the following open question. Under
which constraints on R, X and φ ∈ KX do quantifiers φ have a selection function

Selection functions

29

continuously in φ? Notice that, for such quantifiers, the infinite product functional iscontinuous.
5.7. Relation to traditional instances of bar recursion
Recall that in Lemma 3.2.2 we developed a recursive characterisation of the optimal play!
n−1Oεi (p).
i=0

Before we proceed, let us consider an alternative recursive characterisation in which thesequence of selection functions ε and the outcome predicate p do not change in recursive
calls. For this, we introduce a finite sequence s which is prefixed to the argument of p,
and grows in recursive calls. Intuitively, each recursive call extends a partial play s oflength k in an optimal way from k onwards to get a complete play. In fact, bar recursion
is normally presented in this way, with the sequence s, rather than as in Section 5.4.
Qn−1
Definition 5.7.1. For εi ∈ JXi and p : i=0 Xi → R fixed, and for each k < n, definek−1Ycbrk :

Xi →

n−1
Y

Xi

i=0

i=0

by
(
(cbrk (s))i :=si

if i < k,εi (λxi .p(cbri+1 (s ∗ t ∗ xi )))if n > i ≥ k,where t = (cbrk (s))k ∗ · · · ∗ (cbrk (s))i−1 . Notice that the equation cbrn (s) = s is includedin the above scheme, which gives a base case for the recursion.
Qk−1
Qn−1
Proposition 5.7.2. The family of functions cbrk : i=0 Xi → i=0 Xi is related tothe product of selection functions as!
n−1O
cbrk (s) = s ∗εi (ps ).
i=k

In particular we have
n−1
O

!
εi

(p) = cbr0 ().

i=0The above family of functions cbrk (s) can be viewed as a finite approximation to thefunctional
∞
X k−1
Y
Y
cbr :
Xi →
Xi
k

i=0

i=0

which computes an infinite optimal play, from a partial play s of finite but unbounded
length, as(
si
if i < |s|cbr(s)(i) :=εi (λxi .q(cbr(s ∗ t ∗ xi ))) if i ≥ |s|,

M. Escardó and P. Oliva

30

where t = cbr(s)(|s|) ∗ · · · ∗ cbr(s)(i − 1) and q : Π∞
i=0 Xi → R. Note that we no longer havea fixed stopping point n, but if q is assumed to be a continuous functional, for instance,then we eventually reach a point of continuity of q and the bar recursion stops.
This functional cbr is very similar to (yet different from) the functional used by Berardi,
Q
Bezem and Coquand (Berardi et al., 1998), taking s : i∈N Xi with finite support,(si
if i ∈ dom(s)Xibbc(s)(i) :=Xi
εi (λx .q(bbc(s ∗ (i, x)))) if i 6∈ dom(s).
Other instances of bar recursion include Spector’s bar recursion (Spector, 1962), with
εk : (Xk → Πi Xi ) → Πi Xi ,(sb
if q(bs) < |s|Πi Xi
sbr(s) :=X|s|
ε|s| (λx. sbr(s ∗ x)) if q(bs) ≥ |s|,c is any fixed mapping Σk Πk−1 Xi → Πi Xi , and modified bar recursion (Berger
where (·)
i=0
and Oliva, 2006), with Xi = X, for a fixed X,(
si
if i < |s|X
mbr(s)(i) :=Xεi (λx .q(mbr(s ∗ x))) if i ≥ |s|.
6. The Continuation and Selection Monads
Crucial parts of the above development follow naturally from conceptual reasons expressed in terms of category theory. The above construction K is part of a well-known
monad, known as the continuation monad, which we review here. We show that also J ispart of a monad, which we refer to as the selection monad. The two monads are strong,which explains products of quantifiers and of selection functions in a unified way. Moreover, the procedure ε 7→ ε that transforms selections functions into quantifiers given in
Definition 3.0.6 is a monad morphism J → K. This explains our main Theorem 3.1.5
that shows that attainable quantifiers are closed under finite products.
6.1. Strong monads on cartesian closed categories
Recall that a monad (Mac Lane, 1971) on a category X is a triple (T, η, µ) where T : X →X is a functor, and ηX : X → T X (the unit) and µX : T T X → T X (the multiplication)
are natural transformations, subject to the three equationsµX ◦ ηT XµX ◦ T µX= idT X = µX ◦ T ηX
= µX ◦ µT X

(unit laws),(associativity law).

The associativity law is fairly laborious and space consuming to check directly for thecases T = J and T = K, because it involves three applications of T , which amounts toa nesting of six function spaces. In such situations, as is well known, it is often moreconvenient to derive the monad from a suitable adjunction (Mac Lane, 1971, page 134).
Assuming that the underlying category has finite products, the monad is strong if andSelection functions

31

only if it admits a (necessarily unique) natural transformation
tX,Y : X × T Y → T (X × Y )subject to certain equations, which can be safely omitted because we work with thefollowing characterisation: Further assuming that the category is cartesian closed, themonad is strong if and only if the functor is X -enriched (Kock, 1970a). This means thatits action on morphisms is tracked by a morphism(X → Y ) → (T X → T Y )of X , rather than merely a function from the hom-set X (X, Y ) to the hom-set X (T X, T Y ).
For example, in a cartesian closed category of continuous functions, this means that theassignment f 7→ T f is continuous in f . When T is X -enriched, the strength is given by
the λ-definition
tX×Y (x, v) = T (λy.(x, y))(v),
and automatically satisfies the alluded equations. Notice that λy.(x, y) : Y → X × Y andhence T (λy.(x, y)) : T Y → T (X × Y ).
Definition 6.1.1. Let T be a strong monad on a cartesian closed category X . One
defines a morphism
mX,Y : T X × T Y → T (X × Y )by
mX×Y (u, v) = µX×Y (T (λx.t(x, v)))(u).
That is, given any fixed v : T Y , we have λx.t(x, v) : X → T (X × Y ); applying the functor
T to this we get a map T X → T T (X × Y ), and composing with the multiplicationµX×Y : T T (X × Y ) → T (X × Y ) we get the a map T X → T (X × Y ), which we apply tou : T X to get mX×Y (u, v).
Remarks 6.1.2.
1This standard morphism makes T into a monoidal monad (Kock, 1972). This amounts
to saying that
m1,X (η1 (), u) ∼= mX,1 (u, η1 ())=u∼
andmX,Y ×Z (u, mY,Z (v, w)) ∼= mX×Y,Z (mX,Y (u, v), w)
via the isomorphisms
T (1 × X) ∼= TX ∼= T (X × 1),

2

T (X × (Y × Z)) ∼= T ((X × Y ) × Z).

We have defined m from t. We can recover t from m byt(x, v) = m(η(x), v).

3

Any monad morphism θX : T X → T 0 X commutes with the standard monoidal monadstructure defined in 6.1.1:
θX×Y (m(u, v)) = m(θX (u), θY (v)).

M. Escardó and P. Oliva

32

Recall that a monad morphism T → T 0 is a natural transformation T → T 0 that commutes with the functors, units and multiplications that define the monads.
6.2. The continuation monad
The continuation monad KX = ((X → R) → R) is well known (Kock, 1970b; Moggi,
1990; Moggi, 1991), and hence we provide the constructions but omit a verification of theaxioms. The easiest way to derive the continuation monad is by considering the functor
P : X → X op defined by
P X := (X → R).
This is an X -enriched functor, since its action P f = (q 7→ q ◦ f ) on morphisms,


f
q
f
q
P (X −→ Y ) = (Y −→ R) 7→ (X −→ Y −→ R) ,is tracked by a morphism (X → Y ) → (P Y → P X) of X . This functor is self-adjoint on
the right,
X (A, P X) ∼= X (X, P A),
and the adjunction induces the continuation monad K = P P .
For a morphism f : X → Y , the morphism Kf : KX → KY is given by
Kf (φ)(q) = φ(λx.q(f (x))).
Because f 7→ Kf is λ-definable, it is a morphism of the category and hence the monadis strong, with strength tX,Y : X × KY → K(X × Y ) given by
tX,Y (x, γ)= K(λy.(x, y))(γ)= λp.γ(λy.p(x, y)).

The unit ηX : X → KX is defined by
ηX (x)(p) = p(x).
The multiplication µX : KKX → KX is defined byµ(Φ)(p) = Φ(λφ.φ(p)).
Remark 6.2.1. It is easily verified that the morphism mX,Y : KX × KY → K(X × Y )defined in 6.1.1 satisfies
mX,Y (φ, γ) = φ ⊗ γ,
where ⊗ is defined in Section 2.1, and hence tX,Y (x, γ) = η(x) ⊗ γ. By Remark 6.1.2, weconclude that the product of quantifiers is associative: (φ0 ⊗ φ1 ) ⊗ φ2 ∼= φ0 ⊗ (φ1 ⊗ φ2 ).
We now illustrate the meaning of these constructions in the context of this work.
Examples 6.2.2. Consider R = Ω in the category of sets or any topos.
1

For any A ⊆ X and f : X → Y , the bounded quantifiers ∃A , ∀A ∈ KX and ∃f (A) , ∀f (A) ∈KY satisfy
Kf (∃A ) = ∃f (A) ,Kf (∀A ) = ∀f (A) ,Selection functions

2

33

because ∃y ∈ f (A)(q(y)) = ∃x ∈ A(q(f (x))) and similarly for ∀. In this sense, Kf
behaves like an f -image operator, and functoriality says that the g-image of the f image is the same as the (g ◦ f )-image.
For the strength tX,Y : X × KY → K(X × Y ), we have, for any x ∈ X and any
B ⊆Y,t(x, ∃B ) = ∃{x}×B ,t(x, ∀B ) = ∀{x}×B .

Similarly, by Example 2.1.2, for the operation mX,Y : KX × KY → K(X × Y ), we
have for any A ⊆ X,
m(∃A , ∃B ) = ∃A ⊗ ∃B = ∃A×B ,3

m(∀A , ∀B ) = ∀A ⊗ ∀B = ∀A×B .

The unit produces the bounded existential/universal quantifier for the singleton set:ηX (x) = ∃{x} = ∀{x} ,4because ηX (x)(p) = p(x) = ∃x ∈ {x}(p(x)) = ∀x ∈ {x}(p(x)).
The multiplication µX : KKX → KX involves the perhaps unfamiliar concept ofquantification over quantifiers. Suppose A ⊆ KX is a set such that each φ ∈ A is thebounded existential quantifier of a set Bφ ⊆ X, i.e.
φ = ∃BφThen the bounded universal quantifier ∀A ∈ KKX of the set A ⊆ KX satisfiesµ(∀A )(p) = ∀φ ∈ A ∃x ∈ Bφ (p(x)).

6.3. The selection monad
To prove that J is a monad, we construct a new category, which will turn out to be theKleisli category of J, and show that there is an adjunction with X . In order to define thismanifestation of the Kleisli category of J, we simultaneously work with a manifestationof the Kleisli category of K.
We have used letters X, Y , Z for the objects of our underlying category X . In
order to both avoid confusion and be compatible with the notational conventions of
MacLane (Mac Lane, 1971) for the objects of two different categories related by an adjunction, we will now also adopt the letters A, B, C. These new letters will stand for
objects of a Kleisli category, or equivalently the category of free algebras. Similarly, inan adjoint situation, we will use the letter f for morphisms of X and the letter g formorphisms of free algebras.
A morphism A → B of the Kleisli category of K is a morphism A → KB of theunderlying category X , which, by transposition, amounts to a morphism(B → R) → (A → R).
For the proof that J is a monad that we are about to develop, it is convenient to abstractfrom this situation, by considering an arbitrary functor
P : X → X op

M. Escardó and P. Oliva

34

and hence morphisms of the form
P B → P A.
We will recover the intended results by considering P X = (X → R) as in Section 6.2.
For the remainder of this section, let P : X → X op be an enriched functor that is
self-adjoint on the right, in the sense that there is a natural isomorphism
X (X, P A) ∼= X (A, P X).
We remark that the following definition does not require that the functor P be enrichedor self-adjoint on the right, but everything else does. The enrichment is needed in order
to be able to define new morphisms and enriched functors using the lambda-calculus.
Definition 6.3.1. Define a new category K from our underlying category X and thefunctor P : X → X op as follows:1
2

Objects of K: the same as those of X .
Morphisms of K: A morphism f : A → B of K is a morphism f : P B → P A of X :K(A, B) = X (P B, P A).

3

4

Composition of K: For f : A → B and g : B → C in K, that is, f : P B → P A andg : P C → P B in X , defineg  f = f ◦ g.

Identities of K: Of course, the identity of A in K is the identity of P A in X .

Notice that, in the following lemma, both adjuntions (P, P ) and (F, G) induce the samemonad on X , namely K = P P , and that, by construction, K is isomorphic to the Kleisli
category XK .
Lemma 6.3.2. The functor F = FK : X → K that is the identity on objects and sends
f : X → Y to P f : P Y → P X, regarded as a morphism X → Y of K, has a right adjoint
G = GK : K → X .
Proof. On objects, GA = P P A, and G sends a morphism g : A → B of K, regarded
as a morphism g : P B → P A of X , to P g : P P A → P P A. By construction, a natural
isomorphism K(F X, A) ∼= X (X, GA) amounts to a natural isomorphism X (X, P A) ∼=X (A, P X), which is given by assumption that P is self-adjoint on the right.
A morphism A → B of the Kleisli category of J is a morphism A → JB of theunderlying category, which, by transposition, amounts to a morphism(B → R) → (A → B).
For our proof that J is a monad, we abstract from this situation as above, and consider
morphisms of the form
P B → (A → B).
Definition 6.3.3. Define a new category J from our underlying category X and theenriched functor P : X → X op as follows:Selection functions
1
2

35

Objects of J : the same as those of X .
Morphisms of J : A morphism f : A → B of J is a morphism f : P B → (A → B) ofX:
J (A, B) = X (P B, A → B).
We think of such a morphism as a kind of parametrised morphism of X , and we write
the parameter as a subscript: For f : P B → (A → B) and q : P B and a : A, write
fq (a) = f (q)(a).

3

Auxiliary construction: This parameter q : P B can be “transferred back” to a newparameter p : P A using P fq : P B → P A:
p = Hf (q) := P fq (q)4Composition of J : For
f : P B → (A → B),

g : P C → (B → C)

in X , define the compositeg  f : P C → (A → C)
by, for any r : P C,
(g  f )r = gr ◦ fHg(r) .

5
6That is, we compose functions in the usual way, but transferring back the parameter.
Identities of J : The constantly identities idq = id of X . It is clear that these act asleft and right identities of composition, because H id(p) = p.
Associativity. We first establish:
Claim: H(g  f ) = Hf ◦ Hg.
When we know that J is a category, this, together with the fact that Hid = id, willamount to saying that H is a covariant functor J → K with object part HA = A,
because Hf ◦ Hg = Hg  Hf by definition of composition in K. But we will first use
this claim to prove that J is a category.
Proof of the claim:
H(g  f )(r)=P (g  f (r))(r) = P (gr ◦ fHg(r) )(r) = P fHg(r) ◦ P gr (r)= P fHg(r) (Hg(r)) = Hf (Hg(r)).

Proof of associativity: Let
f : P B → (A → B),

g : P C → (B → C),

h : P D → (B → D),

and s : P D, and calculate:((h  g)  f ))s==(h  g)s ◦ fH(hg)(s) = hs ◦ gHh(s) ◦ fHg(Hh(s))
hs ◦ (g  f )Hh(s) = (h  (g  f ))s .

Hence J is indeed a category and H : J → K is a functor.

M. Escardó and P. Oliva

36

Notational warning. In the following proof, we use the letter epsilon for the counit, as iscustomary, but in its form . Recall that we also use the variant ε of the letter epsilon
for selection functions, which in the following proof correspond to functions P A → A.
Lemma 6.3.4. The functor F = FJ : X → J that is the identity on objects and that
sends a morphism f : X → Y to the constantly f morphism P Y → (X → Y ) of X has aright adjoint G = GJ : J → X .
Proof. We describe G and the required natural isomorphim
J (F X, A) ∼= X (X, GA)
by a universal property, appealing to (Mac Lane, 1971, Theorem IV-2(iv), page 81). It
suffices to show that for every J -object A there is a universal morphism from F to A.
By definition, this amounts to saying that there are an X -object GA and a J -morphism = A : F GA → A such that for every J -morphism f : F X → A, the equation F g = fholds for a unique X -morphism g : X → GA. Considering X = 1 in the desired natural
isomorphism, this suggests to choose GA to be
GA = (P A → A).
We define  : F GA → A in J , or equivalently  : P A → ((P A → A) → A) in X , to be,
for any p : P A and ε : (P A → A),
p (ε) = ε(p).
For any g : X → GA in X , that is, g : X → (P A → A),(  F g)p (x) = (p ◦ (F g)H(p) )(x) = (p ◦ g)(x) = p (g(x)) = g(x)(p).
Hence given any f : F X → A in J , or equivalently, f : P A → (X → A) in X , we areforced to define g : X → GA, byg(x)(p) = fp (x).
With this, not only does the equation   F g = f hold, but also it uniquely determines g,
as required to conclude the existence of a right adjoint.
The above proof does not say explicitly how G acts on morphisms. By the proofof (Mac Lane, 1971, Theorem IV-2(iv), page 81), its action on morphisms is uniquelydetermined by its action on objects and the requirement that  : F GA → A be a naturaltransformation in A, as follows: Given a morphism h : A → B in J , the morphism Gh in
X is the unique g : GA → GB such that   F g = f , where f = h   : F GA → B. Now,
by the construction of g from f in the proof of Lemma 6.3.4, expanding all the definitions,and using the fact that a morphism h : A → B of J is a morphism h : P B → (A → B)
of X , we have that, for all q ∈ P B and ε ∈ GA = (P A → A),
Gh(ε)(q)==g(ε)(q) = fq (ε) = (h  )q (ε) = (hq ◦ Hh(q) )(ε)

hq (ε(Hh(q))) = hq (ε(P hq (q))).

Selection functions

37

The proof of Lemma 6.3.4 does not say explicitly what the unit ηX : X → GF X of
the adjunction is either. By the proof of (Mac Lane, 1971, Theorem IV-2(iv), page 81),
it is the unique morphism such that   F g = ηX for g = idF X : F X → F X. By theconstruction of g from f in the proof of Lemma 6.3.4 and the definition of the identities
of J ,ηX (x)(p) = (idF X )p (x) = x.
Applying the standard construction of a monad from a given adjunction, we get:Lemma 6.3.5. JX = GF X = (P X → X) is a strong monad on X , with action onmorphisms f : X → Y given by, for all ε : JX and q : P Y ,Jf (ε)(q) = f (ε((P f (q)))),
and with units ηX : X → JX and multiplications µX : JJX → JX given by, for all x : X,
p : P X, and E : JJX,ηX (x)(p) = x,

µX (E)(p) = E(P p (p))(p).

Proof. Let f : X → Y in X and h = F f . Then hq = f by the definition of F , andhence we conclude thatGF f (q) = hq (ε(P hq (q))) = f (ε(P f (q))),as claimed. The multiplication is given by, for any E : JJX and p : P X,µ(E)(p) = G(E)(p) = p (E(P p (p))) = E(P p (p))(p),as claimed. The monad is strong because the action of J on morphisms is clearly λdefinable, and hence tracked by a morphism of X .
Lemma 6.3.6. There is a monad morphism θX : JX → KX, given by the adjoint
transposes of the family of maps
λp.P (λε.ε(p))(p) : P X → P JX.
Proof. We apply (Moggi, 1990, Proposition 4.0.10), which shows that monad morphisms θ : J → K are in bijection with functors H : XJ → XK of the Kleisli categories
which are the identity on objects and such that the equation H ◦ FJ = FK holds. The
direction of the bijection that we need constructs the component θX : JX → KX of thenatural transformation as Hh, where the morphism h in XJ is the identity JX → JX
of X in X , regarded as a morphism JX → X of the Kleisli category XJ of J. In the
manifestation J of XJ , this amounts to a morphism h : P X → (JX → X) of X , whichis readily seen to be hp (ε) = ε(p). Notice that Hh : JX → X, because H is the identity
on objects, and hence Hh : JX → KX regarded as a morphism of the Kleisli categoryof K, and hence Hh : P X → P JX regarded as a morphism of X . Now, for H : J → K
constructed in Definition 6.3.3, we have
H(FJ f )(q) = P f (q) = FK f (q),

M. Escardó and P. Oliva

38

and hence the above is applicable. We thus get θ as the adjoint transpose JX → P P X
ofHh = λp.P hp (p) = λp.P (λε.ε(p))(p)which concludes the proof.
Theorem 6.3.7. JX = ((X → R) → X) is a strong monad on X , with action onmorphisms f : X → Y given by
Jf (ε)(q) = f (ε(q ◦ f )),and with units ηX : X → JX and multiplications µX : JJX → JX given by
ηX (x)(p) = x,

µX (E)(p) = E(λε.p(ε(p)))(p).

Moreover, the assignment ε → ε is a monad morphism from J to the continuation monad
KX = ((X → R) → R).
Proof. Take P X = (X → R) and P f (q) = q ◦ f as in Section 6.2. ThenP p (p) = p ◦ p = λε.p(p (ε)) = λε.p(ε(p)),
which gives the above definition of µ. Now
λp.P (λε.ε(p))(p) = λp.λε.p(ε(p)),
whose transpose is λε.λp.p(ε(p)) and hence gives the desired monad morphism.
Remarks 6.3.8.
1Because a monad morphism commutes with the functors that define the monads,
Theorem 6.3.7 gives, for any f : X → Y and ε ∈ JX:
Jf (ε) = Kf (ε).

Hence if ε ∈ JX is a selection function for the quantifier φ ∈ KX then Jf (ε) is aselection function for the image quantifier Kf (φ). In particular, by Example 6.2.2(1),for any A ⊆ X, if ε is a selection function for ∃A , then Jf (ε) is a selection functionfor ∃f (A) , which is the content of the proof of (Escardó, 2008, Proposition 4.3).
2 Theorem 3.1.5 follows directly from Theorem 6.3.7 and Remarks 6.1.2.
3 The construction of the strength and of the monoidal monad structure given in Definition 6.1.1 is characterised as follows, where ⊗ is defined as in Section 3.1:(a) The morphism tX,Y : X × JY → J(X × Y ) satisfiest(x, δ) = λp.(x, δ(λy.p(x, y))) = η(x) ⊗ δ(b) The morphism mX,Y : JX × JY → J(X × Y ) satisfiesm(ε, δ) = ε ⊗ δ.
(c) Hence, by Remark 6.1.2, we conclude that the product of selection functions is
associative: (ε0 ⊗ ε1 ) ⊗ ε2 ∼= ε0 ⊗ (ε1 ⊗ ε2 ).

Selection functions

39

7. Further work
The work presented here sets the ground for applications to proof theory which we are
currently developing. We study the role of the monad J in the translation of proofs in
the context of minimal logic ML, where monad algebras JA → A are objects with arealizer/proof of the instance
PLR A

:

((A → R) → A) → A

of Peirce’s law. Also, in the same way the monad K gives rise to the well-known negativetranslation, the monad J defines a proof translation of ML + PLR into ML. We alsoNknow that the infinite product functional
realizes (in the sense of Kreisel’s modified
realizability) the J-shift∀n(JA(n)) → J (∀nA(n)) .
The J-shift is more general than the double negation shift (K-shift), and gives the K-shift
in the cases it exists, similarly to the relation between countable products of selection
functions and quantifiers discussed in Section 5.6. This leads to a natural construction
based on the product of selection functions which realises the axiom of countable (anddependent) choice.
We are also investigating the inter-definability (over Gödel’s system T ) between the
new instance of bar recursion presented here and traditional instances (cf. Section 5.7).
References
Abramsky, S. and Jung, A. (1994). Domain theory. In Abramsky, S., Gabbay, D., and Maibaum,T., editors, Handbook of Logic in Computer Science, volume 3 of Oxford science publications,pages 1–168. Oxford university press.
Avigad, J. and Feferman, S. (1998). Gödel’s functional (“Dialectica”) interpretation. In Buss,
S. R., editor, Handbook of proof theory, volume 137 of Studies in Logic and the Foundationsof Mathematics, pages 337–405. North Holland, Amsterdam.
Battenfeld, I., Schröder, M., and Simpson, A. (2006). Compactly generated domain theory.
Math. Structures Comput. Sci., 16(2):141–161.
Battenfeld, I., Schröder, M., and Simpson, A. (2007). A convenient category of domains. In Computation, meaning, and logic: articles dedicated to Gordon Plotkin, volume 172 of Electron.
Notes Theor. Comput. Sci., pages 69–99. Elsevier, Amsterdam.
Bauer, A. (2002). A relationship between equilogical spaces and type two effectivity. MLQ
Math. Log. Q., 48(suppl. 1):1–15.
Bekič, H. (1984). Programming languages and their definition, volume 177 of Lecture Notes in
Computer Science. Springer-Verlag, Berlin. Selected papers edited by C. B. Jones.
Berardi, S., Bezem, M., and Coquand, T. (1998). On the computational content of the axiomof choice. The Journal of Symbolic Logic, 63(2):600–622.
Berger, U. and Oliva, P. (2005). Modified bar recursion and classical dependent choice. Lect.
Notes Log., 20:89–107.
Berger, U. and Oliva, P. (2006). Modified bar recursion. Math. Structures Comput. Sci.,
16(2):163–183.
Bezem, M. (1985). Strongly majorizable functionals of finite type: a model for bar recursion
containing discontinuous functionals. The Journal of Symbolic Logic, 50:652–660.

M. Escardó and P. Oliva

40

Bove, A. and Dybjer, P. (2008). Dependent types at work. Lecture notes from the LerNET
Summer School, Piriapolis, available at the authors’ web pages.
Escardó, M. (2007). Infinite sets that admit fast exhaustive search. In Proceedings of the 22nd
Annual IEEE Symposium on Logic In Computer Science, pages 443–452. IEEE Computer
Society.
Escardó, M. (2008). Exhaustible sets in higher-type computation. Log. Methods Comput. Sci.,
4(3):3:3, 37.
Escardó, M., Lawson, J., and Simpson, A. (2004). Comparing Cartesian closed categories of(core) compactly generated spaces. Topology Appl., 143(1-3):105–145.
Hutton, G. (2007). Programming in Haskell. Cambridge University Press.
Johnstone, P. (2002). Sketches of an Elephant: a Topos Theory Compendium. Oxford University
Press.
Kock, A. (1970a). Monads on symmetric monoidal closed categories. Arch. Math. (Basel),
21:1–10.
Kock, A. (1970b). On double dualization monads. Math. Scand., 27:151–165 (1971).
Kock, A. (1972). Strong functors and monoidal monads. Arch. Math. (Basel), 23:113–120.
Lambek, J. and Scott, P. (1986). Introduction to Higher Order Categorical Logic. Cambridge
University Press.
Mac Lane, S. (1971). Categories for the Working Mathematician. Springer.
Moggi, E. (1990). An abstract view of programming languages. Technical Report ECS-LFCS90-113, Laboratory for Foundations of Computer Science, University of Edinburgh.
Moggi, E. (1991). Notions of computation and monads. Information and Computation, 93(1):55–
92.
Nisan, N. et al. (2007). Algorithmic Game Theory. Cambridge University Press.
Normann, D. (1980). Recursion on the countable functionals, volume 811 of Lec. Not. Math.
Springer.
Normann, D. (1999). The continuous functionals. In Griffor, E. R., editor, Handbook of Computability Theory, chapter 8, pages 251–275. North Holland, Amsterdam.
Oliva, P. (2006). Understanding and using Spector’s bar recursive interpretation of classicalanalysis. Beckmann, Arnold (ed.) et al., Logical approaches to computational barriers. Second conference on computability in Europe, CiE 2006, Swansea, UK, June 30–July 5, 2006.
Proceedings. Berlin: Springer. Lecture Notes in Computer Science 3988, 423-434 (2006).
Schröder, M. (2002). Extended admissibility. Theoret. Comput. Sci., 284(2):519–538.
Smyth, M. (1977). Effectively given domains. Theoret. Comput. Sci., 5(1):256–274.
Spector, C. (1962). Provably recursive functionals of analysis: a consistency proof of analysis
by an extension of principles in current intuitionistic mathematics. In Dekker, F. D. E.,
editor, Recursive Function Theory: Proc. Symposia in Pure Mathematics, volume 5, pages
1–27. American Mathematical Society, Providence, Rhode Island.
Valiente, G. (2002). Algorithms on Trees and Graphs. Springer.