Sequential games and optimal strategies

Martín Escardó, Paulo Oliva

Abstract

This article gives an overview of recent work on the theory of selection functions. We explain the intuition behind these higher type objects, and define a general notion of sequential game whose optimal strategies can be computed via a certain product of selection functions. Several instances of this game are considered in a variety of areas such as fixed point theory, topology, game theory, higher type computability and proof theory. These examples are intended to illustrate how the fundamental construction of optimal strategies based on products of selection functions permeates several research areas.

1. Introduction

Life is the sum of all your choices, so said Albert Camus. But what does ‘choice’ mean? One could say that to choose is to select one element x out of a set X of possible candidates. The set X could be the collection of all the petrol stations on the way to work, or the different types of fuel available at a particular station. Our choice x is which petrol station to use when the fuel tank empties or which types of fuel we prefer.

So, how do we make choices? What leads us to pick one particular x over all others? If we ignore the fact that in some cases we do like to pick things at random, it is fair to say that we normally decide on a few criteria before making a choice. For instance, quite often we implicitly assign a value (say, a real number Embedded Image) to each element of the set, representing the cost of making that particular choice. If X is the set of fuel types at a particular petrol station, then our mapping Embedded Image could be the cost of a litre of petrol of each particular type x. We then select an xX that has minimal cost or the best cost-benefit. In fact, we are only using the real numbers as an ordered set. Any ordered set (R,≤) would be sufficient. The order does not even need to be total, meaning that for some two candidates x and x′ we might not be able to tell which one is better.

Anyway, once we have fixed a more structured set R, our ‘criteria’ mapping p: XR propagates the structure of R to the elements of X. For instance, if R is an ordered set, we immediately get an order on X by saying that a petrol station x is better than another petrol station y, if p(x)≥p(y). Thus, we might be interested in picking an xX, which either maximizes or minimizes the value of p(x), depending on whether p: XR represents the quality of fuel or the cost of a litre of that particular fuel type, respectively.

Although the mapping p: XR depends on the criteria used by a particular individual, the fact that we pick an x, which minimizes the cost is much more universal. We use the same minimization function when choosing the cheapest hotel or the cheapest pair of trousers. Any function, such as the minimization or maximization functions, that in a uniform way picks an xX when given a mapping p: XR we shall call a selection function. These are functions of type Embedded Image The ‘minimization’ selection function, which we use when p describes the cost associated with each particular choice, is Embedded Image whereas the ‘maximization’ selection functions, which we use when p represents the payoff obtained by making a particular choice, is Embedded Image Both ε and δ have type (XR)→X.

Note that selection functions decide which element to choose for each given ‘criteria’ mapping p: XR. If the cost of the different fuel types change, we might be led to make a different choice, although we are still using the same selection function ε. Only the criteria mapping p will have changed.

Once we have the chosen element x=ε(p), we can in particular calculate the optimal cost (or payoff) we have achieved as Embedded Image For a given p: XR, we say that x=ε(p) is an optimal choice, whereas r=p(ε(p)) is the optimal outcome. We can also define the optimal outcome directly. For instance, in the case of the petrol station, the optimal outcome is the minimum value of the mapping p: XR. As ε picks an x where p has least value, we have that Embedded Image for all p: XR.

A similar equation to the above also holds for the relation between Embedded Image and the selection function δ, i.e. Embedded Image In general, we call a function Embedded Image a quantifier. When for a given quantifier ϕ a selection function ε always picks x=ε(p), such that ϕ(p)=p(x) we say that ε is a selection function for ϕ. In this case ϕ can be defined from epsilon by the equation Embedded Image Intuitively, both selection functions and quantifiers operate on the criteria mapping p: XR. A quantifier ϕ says what is the desired outcome for a given p: XR, whereas a selection function ε for ϕ calculates an xX, which achieves that outcome. Note that our concept of ‘quantifier’ is more general than Mostowski’s notion of a generalized quantifier (Mostowski 1957), which is the case when R is the set of truth-values or Booleans.

For the rest of this review, we shall explore the connection between quantifiers and selection functions, and define algebraic operations on them. We will then define a notion of sequential game, and show that the product of selection functions allows us to compute optimal strategies in such games. In §8, we show, by picking particular instantiations from different areas, that this notion of game is very general. This review mostly covers recent work of the authors, which has appeared in Escardó & Oliva (2010a,b,c), although some concepts have been simplified and generalized.

λ-notation. In the following sections, we rely heavily on the use of λ-notation to describe functions. For instance, the function ‘two to the power of n’ can be described as λn⋅2n. When this is applied to 3, for instance, it gives (λn⋅2n)(3)=23=8. The λ-notation is particularly useful when working with higher type objects such as functions ε from XR to X, since its argument is itself a function.

Models of higher type functions. For the first part of the paper (§§2–5), which concerns finite games of fixed length, the reader can safely think of X and Y as ordinary finite or infinite sets, and the mappings XY as the set of all functions from X to Y . In §6, however, which concerns games of unbounded length, one has to be careful and work with (non-standard) models of functionals, so as to ensure that the infinitely iterated product is well-defined. The model we should bear in mind in this case is that of the continuous functionals (Normann 1999), and in some cases also the model of majorizable functionals (Bezem 1985).

2. The product of quantifiers

Continuing from the examples given in §1, suppose now that we could only choose which petrol station to stop at, and the owner of the petrol stations then chooses the type of fuel we must use at that particular station we have picked. As we know that the owner will try to maximize his profit and will offer us the most expensive fuel, we have to choose the petrol station with the cheapest most expensive fuel. In other words, if X is the set of petrol stations, Y is the set of different fuel types, and Embedded Image gives the cost of fuel y at station x, then the best outcome for us is to pay Embedded Image Interestingly, this is also the optimal outcome for the owner of the petrol stations, as he has no control over which station we choose.

Let us use the abbreviations KRX=(XR)→R and JRX=(XR)→X for the types of quantifiers and selection functions, respectively.

Definition 2.1 (Binary product of quantifiers)

Given quantifiers ϕ: KRX and ψ: KRY , we define their product (ϕψ): KR(X×Y) as Embedded Image

For instance, given the quantifiers Embedded Image and Embedded Image discussed above we have that their product is Embedded Image where, for clarity, we indicate above the equality sign the type of the two objects. Also, given the quantifiers Embedded Image and Embedded Image, corresponding to the existential and universal quantifiers, we have that their product concisely describes the nesting of quantifiers, i.e. Embedded Image

We can iterate this binary product of quantifiers and obtain an n-ary product a follows:

Definition 2.2 (n-ary product of quantifier)

Given a sequence of quantifiers ϕi: KRXi, 0≤in, define their product inductively by iterating the binary product as Embedded Image where Embedded Image.

Let us show how the concept of quantifiers allows us to define a very general notion of sequential games. We will also show that the product of quantifiers described above computes the optimal outcome of such games.

3. Finite games of fixed length

Games often simulate life. In particular, a play in a game can be viewed as a sequence of choices that lead to some outcome. Hence, we can think of a sequence of choices as a sequence of moves in some sequential game. In the case of choosing which petrol station to use, this is a simple game with one player and one round. In the case, we must also choose which fuel type to use, this is a one-player two-round game. If the owner of the station chooses the type of fuel we must use, then this is a two-player two-round game. In all cases, the aim of the game for us (the first player in the last example) is to minimize the cost (or maximize the payoff) obtained from a particular choice, and the actual move in the game is the particular choice we commit ourselves to.

In the following, we explore the concept of a quantifier introduced above and generalize these scenarios to games with a finite number of rounds.

Definition 3.1 (Finite game)

Any tuple Embedded Image defines an n-round sequential game, where

  • — R is the set of possible outcomes of the game,

  • — Xi is the set of possible moves at round i,

  • — ϕi: KRXi is the quantifier for round i, and

  • — Embedded Image is the outcome function.

A sequence Embedded Image is called a play of the game.

Note that, we have said nothing about the number of players in the game. Instead, the definition of the game includes a quantifier ϕi for each round. This function ϕi picks a particular outcome ϕi(p)=rR when given a mapping p: XiR. Intuitively, once we know how each choice of move in Xi will impact the outcome of the game, then ϕi tells us what outcome would be desirable.

For instance, if R={−1,0,1} and ϕi are the minimum-value function for odd rounds and the maximum-value function for even rounds, then we have a two player game where one player is aiming for the outcome −1, whereas the other is aiming for the outcome 1. Thus, the three possible outcomes correspond to one of the players winning, or the game ending in a draw.

The example in §2 corresponds to the case when n=2, i.e. a game with two rounds. X is the set of petrol stations and Y is the collection of different fuel types. The outcome function Embedded Image gives the cost of a particular fuel at a particular station. As we are choosing which station to use, and the owner of the stations chooses the fuel to be used, we have that Embedded Image, whereas Embedded Image.

Definition 3.2 (Strategy)

A strategy for the game Embedded Image is a family of mappings Embedded Image, for each 0≤k<n. Given a partial play a=a0,…,ak−1, any strategy defines a strategic extension of a as Embedded Image for kj<n.

Given a strategy (nextk)i<n, the functions nextk compute which move should be played at each round k, i.e. when the game is at position a=a0,…,ak−1 the next move selected is given by ak=nextk(a). The strategic extension of a partial play is simply the play obtained by following the strategy at each round.

Definition 3.3 (Optimal strategy)

A strategy (nextk)k<n is said to be optimal if for every partial play a=a0,…,ak−1, we have Embedded Image

Intuitively, a strategy is optimal if the outcome obtained by following the strategy Embedded Image is the best possible outcome as described by the quantifier ϕk, for each round k. For instance, considering again the example from §2, the optimal strategy would consist of the functions Embedded Image and Embedded Image where Embedded Image abbreviates Embedded Image. In general, we will write qx for the function λyq(x,y).

Theorem 3.4 (Optimal outcome)

For any optimal strategy (nextk)k<n let b be its strategic play. We have that Embedded Image We call w the optimal outcome of the game. Note that, this is unique and independent of the optimal strategy.

Proof.

Let an optimal strategy (nextk)k<n be fixed. By the definition of optimal strategy (definition 3.3), we have Embedded Image  ■

As discussed in §2, the optimal outcome of the game between us and the owner of the petrol station is for us to choose the station with cheapest most expensive fuel, whereas the owner then picks the most expensive fuel at the station we have chosen. So the optimal outcome of the game is Embedded Image If, on the other hand, we could choose not only which station to use, but also which fuel type to use (and if we were interested in minimizing our cost) that is a different game where Embedded Image and the optimal outcome of the game is Embedded Image where we pick the station which has the cheapest fuel, and then pick the cheapest fuel at that chosen station.

Definition 3.5 (Subgames)

A partial play Embedded Image, for kn defines the subgame Embedded Image, where Embedded Image is the partial outcome function defined as Embedded Image or, more concisely qa(x):=q(a*x), where * denotes concatenation of finite sequences.

The subgame Embedded Image is like the original game except that we are starting at the position determined by the initial moves a. Notice that if k=n then q is constant, and when k=0 this is the same as the full game. The optimal outcome of the subgame defined by a can similarly be computed as Embedded Image If k=n this corresponds to the subgame where there are no more moves to be made—the end of the game. Therefore, the outcome can be computed directly from the moves already made a, i.e. wa=q(a). If k<n then we have a proper subgame, and the optimal outcome of this proper subgame is Embedded Image Hence, the optimal outcome of round k is determined by the quantifier for round k together with the mapping λxkwa*xk computing the optimal outcome at round k+1 given what is played at round k. Considering again the example from §2, when choosing which petrol station x to stop at, it is enough to look at the most expensive fuel type wx at each station, because we know that this is the fuel type the owner of the stations will offer us. Therefore, the optimal outcome for us is Embedded Image. The notion of optimal outcome for subgames leads to the notion of optimal move.

Definition 3.6 (Optimal move and optimal play)

For a partial play a=a0,…,ak−1 a move xk at round k is said to be an optimal move if it preserves the optimal outcome, i.e. if the optimal outcome wa of the subgame determined by a is the same as the optimal outcome wa*xk of the new subgame determined by a*xk. A whole play x=x0,…,xn−1 is called an optimal play if each xk is an optimal move given the partial play x0,…,xk−1.

In other words, a move at round k is optimal if it leads to a subgame where the optimal outcome of the game is still achievable. As one would expect, if we play optimally at each round we will end-up with the optimal outcome of the game.

Lemma 3.7

If x=x0,…,xn−1 is an optimal play then Embedded Image i.e. the outcome of an optimal play is the optimal outcome.

Proof.

Since x is an optimal play we have that (for all 0≤i<n) xi is an optimal move in the subgame x0,…,xi−1, i.e. Embedded Image The result follows since wx0,…,xn−1=q(x), whereas Embedded Image. ■

Moreover, the next lemma shows that plays obtained by following optimal strategies are indeed optimal.

Lemma 3.8 (Optimal strategies and optimal plays)

For any optimal strategy its strategic play is an optimal play.

Proof.

Assume (nextk)k<n is an optimal strategy, and let b=b0,…,bn−1 be the strategic play. We must show, for 0≤k<n−1, that wa=wa*bk, where a=b0,…,bk−1. By (i) the definition of optimal outcome and (ii) the fact that (nextk)k<n is an optimal strategy we have Embedded Image  ■

Note that optimal strategies do not exist in general, since optimal outcomes are not necessarily achievable. For instance, consider the game with a single round having quantifier ϕ0: K{0,1}{0,1} Embedded Image and assume the outcome function is q(x)=1. The optimal outcome defined by ϕ0 is 0, whereas the only achievable outcome is 1. Nevertheless, in §5, we will show that optimal strategies always exist when the quantifiers that define the game are attainable, i.e. have corresponding selection functions. Moreover, a suitably defined product of selection functions calculates optimal strategies.

4. Games with multiple optimal outcomes

Before we proceed to show how a product of selection functions computes optimal strategies, let us first generalize the notion of game introduced in §3. For that, let us consider the space Embedded Image of multi-valued quantifiers. Similarly to before, we say that a multi-valued quantifier ϕ: SRX is attainable if there exists a selection function ε: JRX, such that Embedded Image for all p: XR. Intuitively, ϕ describes a set of optimal outcomes for any given criteria mapping, and the selection function ε for ϕ picks an xX, which achieves one of the optimal outcomes.

Definition 4.1 (Finite games with multiple optimal outcomes)

An n-round sequential game with multiple optimal outcomes is a tuple Embedded Image where

  • — R is the set of possible outcomes of the game,

  • — Xi is the set of possible moves at round i,

  • — ϕi: SRXi is the multi-valued quantifier for round i, and

  • — Embedded Image is the outcome function.

A sequence Embedded Image is called a play of the game.

Just as in §3, every partial play Embedded Image defines a subgame. In games with multiple optimal outcomes, however, we cannot define ‘the’ optimal outcome as we did in §3, simply because there might not be a single optimal outcome for the whole game. Moreover, there seems to be no way of defining a product of multi-valued quantifiers, as we did for the single-valued quantifiers. Nevertheless, we can still define a notion of an optimal strategy, slightly generalizing definition 3.3.

Definition 4.2 (Optimal strategy)

Recall that a partial play a=a0,…,ak−1 and a strategy Embedded Image defines a strategic extension of a as Embedded Image for kj<n. A strategy (nextk)k<n is said to be optimal if for every partial play a=a0,…,ak−1, we have Embedded Image Compare this with definition 3.3, where we have equality (=) instead of ∈.

In §3, we said that a strategy was optimal if the outcome of an strategic play Embedded Image was precisely the optimal outcome according to the quantifier ϕk. By moving to multi-valued quantifiers, what we must say instead is that a strategy is optimal if the outcome of a strategic play is among the possible optimal outcomes for each of the multi-valued quantifier ϕk. It is clear that when multi-valued quantifiers are in fact single-valued the two notions of optimal strategy (definitions 3.3 and 4.2) coincide.

5. Calculating optimal strategies

We have explained at the end of §3, why optimal outcomes are not always achievable. Note also that even when an optimal outcome is achievable, optimal strategies are not necessarily unique. There might be several choices which are all equally optimal, if all lead to an optimal outcome of the game. Nevertheless, what we show next is that if the (multi-valued) quantifiers ϕk for each round k have associated selection functions εk, then we can always compute optimal strategies (in the more general sense of definition 4.2) in the game defined by such ϕk’s. Intuitively, having a selection function ε is a stronger requirement than simply having a quantifier ϕ, because every selection function ε defines a (single-valued) quantifier as Embedded Image Recall that JRX abbreviates (XR)→X.

Definition 5.1 (From JRX to KRX)

Denote by Embedded Image the following mapping from selection functions to quantifiers Embedded Image 5.1

Going back to the example from §2, we are in a good position because the quantifiers Embedded Image and Embedded Image in this case have selection functions ε and δ, respectively (as defined in §1). It is for that reason that we can find a play which is optimal and hence leads to the optimal outcome Embedded Image But how do we compute the optimal play x,y that leads to this optimal outcome? The solution is to turn the game upside down. Instead of trying to find the correct x first, we instead look for the best choice of yY for any given xX. That can be done very easily using the selection function δ for the quantifier Embedded Image, i.e. Embedded Image Hence, for each of our choices of petrol station xX, we know what the optimal move yxY of the second player is. Once we have this mapping xyx from our choice of station x to the fuel type yxY the owner of the petrol station will offer us, we can choose the petrol station with cheapest most expensive fuel. For that we use the selection function for the minimization quantifier, i.e. Embedded Image Finally, once we have computed our best choice of petrol station a as above, we can then go back to yx and compute the optimal move for the second player as y=ya (where a is now the optimal move for player one). Such construction works in general, as we have only used the fact that ε and δ are selection functions for the quantifiers Embedded Image and Embedded Image, respectively.

Definition 5.2 (Binary product of selection functions)

Given selection functions ε: JRX and δ: JRY define their product (εδ): JR(X×Y) using λ-notation as Embedded Image where a=ε(λxq(x,yx)) and yx=δ(λyq(x,y)). We can then equivalently define the product above using function composition as Embedded Image where Embedded Image and Embedded Image is the curried form of q: X×YR. This is illustrated diagrammatically as

Embedded Image

First let us show that the product of selection functions corresponds to the product of single-valued quantifiers defined in §2.

Lemma 5.3

For any given ε: JRX and δ: JRY we have Embedded Image.

Proof.

Simply unfolding definitions we have Embedded Image  ■

From this we can conclude that, just like the product of quantifiers (definition 2.1) computes the optimal outcome of a single-optimal-outcome game, the product of selection functions (definition 5.2) computes an optimal play in such games.

Theorem 5.4 (Optimal plays for two-round games)

Let a two-round sequential game Embedded Image be given. If the quantifiers ϕ01 have selection functions ε01 then an optimal play in the game can be computed as Embedded Image

Proof.

We must show that x and y are optimal moves, i.e. that wx,y=q(x,y) equals wx=ϕ1(λyq(x,y)), which in turn must equal the optimal outcome w=(ϕ0ϕ1)(q). First note that x=ε0(λx′⋅ϕ1(λy′⋅q(x′,y′))) and y=ε1(λy′⋅q(x,y′)). The result then follows as: Embedded Image since ϕ0(p)=p(ε0(p)) and ϕ1(p)=p(ε1(p)). ■

In the general case of multi-valued outcome functions, we have:

Theorem 5.5 (Optimal strategies for two-round games—multi-valued ’s)

Let a two-round sequential game Embedded Image be given, where ϕ0: SRX0 and ϕ1: SRX1 are multi-valued quantifiers. If ϕ01 have selection functions ε01 then an optimal strategy in the game can be computed as Embedded Image and Embedded Image where π0 denotes the first projection, i.e. π0(x,y)=x.

Just as we did with the binary product of quantifiers (definition 2.2) we can iterate the binary product of selection function to obtain an n-ary product as follows:

Definition 5.6 (n-ary product of selection functions)

Given a sequence of selection functions εi: JRXi define their product by simply iterating the binary product as Embedded Image where Embedded Image.

The following theorem describes how this product of selection functions can be used to compute optimal strategies.

Theorem 5.7 (Main theorem for finite games of fixed length)

Let an n-round sequential game Embedded Image be given (in the more general sense of definition 4.1). If the multi-valued quantifiers ϕi: SRX are attainable, i.e. have associated selection functions εi, then an optimal strategy for the game can be computed as Embedded Image where π0 denotes the first projection, i.e. π0(x*α)=x.

Proof.

This is a particular case of the more general theorem 6.5, which we prove in §6. ■

We call the optimal strategy computed from ε the ε-strategy, and its strategic play we call the ε-play. As a consequence of the above theorem we obtain a general way of finding a solution a and p to the following simple system of equations and membership. We will discuss in §7 a few examples of how such a system of equations appears in practice.

Corollary 5.8

Let an n-round sequential game Embedded Image be given. If the multi-valued quantifiers ϕi: SRX are attainable then there are functions pk: XkR, such that Embedded Image and Embedded Image for 0≤k<n, where a is the ε-play.

Proof.

This is a particular case of the more general corollary 6.6 which we prove in §6. ■

In particular, note that if ϕk are all single-valued then pj(aj)=pk(ak), for all 0≤j,k<n, as Embedded Image The intuitive reading of corollary 5.8 is that in any sequential game (with multi-valued outcome functions) it is always possible to turn the global outcome function Embedded Image into a family of local outcome functions pk: XkR, so that

  • — the ε-play a can be computed locally from the selection functions εk, and

  • — the outcome of the ε-play is in the intersection of ‘desired’ outcomes for all rounds k.

6. Finite games of unbounded length

The sort of games considered so far terminate after a fixed number of rounds n. We will show next that it is also possible to compute optimal strategies in games with an unbounded (but finite) number of rounds. These are games where the number of rounds until the outcome is reached depends on how the game develops. Because the number of rounds in the game can be arbitrarily large, we must include in the definition of the game a set of possible moves Xi and an outcome quantifier ϕi for all natural numbers Embedded Image. However, we do not want to consider games that go on indefinitely. One way to ensure that every play in the game is finite is to assume that the value of the outcome function q is determined after a finite (but unbounded) number of rounds, i.e. Embedded Image 6.1 For any ‘infinite’ play α there exists a point n where the value of the outcome q(α) is fixed, so that any other extension β of the play would lead to the same outcome. This holds, for instance, when the set of outcomes R is discrete1 and the outcome function q is continuous.

Definition 6.1 (Finite but unbounded game)

A finite but unbounded sequential game is a tuple Embedded Image where

  • — R is the discrete set of possible outcomes of the game,

  • — Xi is the set of possible moves at round Embedded Image,

  • — ϕi: SRXi is the multi-valued quantifier for round Embedded Image, and

  • — Embedded Image is the continuous outcome function.

A sequence Embedded Image is called a play of the game. The relevant part of a play α is the finite initial segment Embedded Image which determines the value of q(α).

As in §3, a strategy for an unbounded game Embedded Image is a family of mappings Embedded Image, for each Embedded Image. Given a partial play a=a0,…,ak−1, any strategy defines a strategic extension of a as Embedded Image for jk.

Definition 6.2 (Optimal strategy)

A strategy Embedded Image is said to be optimal if for all Embedded Image and for every partial play a=a0,…,ak−1, we have Embedded Image

Having defined the unbounded game and its generalized notion of optimal strategy, we now show how the infinite iteration of the binary product of selection functions computes optimal strategies in games where the quantifiers ϕi are attainable.

Definition 6.3 (Unbounded product of selection functions)

Given an infinite sequence of selection functions εi: JRXi define their unbounded product by simply iterating the binary product as Embedded Image where, for clarity, the type of the final product is shown above the equality sign.

It is perhaps surprising that such product functional is in fact not only well-defined in the model of continuous functionals (Scarpellini 1971) but also computable and part of the standard installation of Haskell (see §7g for more details). This is in stark contrast with the iterated product of quantifiers which is not well-defined even in the model of continuous functionals.

We will show next that the above product of selection functions permits us to compute optimal strategies for finite but unbounded games with attainable quantifiers. First, let us prove the following useful lemma.

Lemma 6.4

Let x=x0,…,xk−1 and Embedded Image For all Embedded Image the following holds: Embedded Image where (α)[j] is the initial segment of α of length j, i.e. α(0),…,α(j−1).

Proof.

If j=0 this follows by definition. Assuming this holds for j we wish to show it for j+1. We have Embedded Image where Embedded Image. Therefore, we have that Embedded Image. ■

As with the finite games of fixed length (theorem 5.7) we now show how the unbounded product of selection functions (definition 6.3) computes optimal strategies in games of unbounded length.

Theorem 6.5 (Main theorem for finite but unbounded games)

Let a finite but unbounded sequential game Embedded Image be given. If the quantifiers ϕi have selection functions εi then an optimal strategy in the game can be computed as Embedded Image where x=x0,…,xk−1.

Proof.

Fix an arbitrary partial play x=x0,…,xk−1. Let Embedded Image We have that Embedded Image By lemma 6.4 we also have that Embedded Image This implies that Embedded Image By the fact that εk is a selection function for ϕk we get Embedded Image The result follows since q(x,βx(k)*βx,βx(k))=q(x*βx), i.e. starting a strategic play from x or an extension of that with the next strategic play x,βx(k) leads to the same final play. ■

As a corollary, we obtain that the following system of equations and membership can be solved via the product of selection functions. This generalizes corollary 5.8.

Corollary 6.6

Let a finite but unbounded sequential game Embedded Image be given. If the quantifiers ϕk have associated selection functions εk then there are functions pk: XkR, such that Embedded Image and Embedded Image for Embedded Image, where α is the ε-strategic play from the proof of theorem 6.5, i.e. Embedded Image

Proof.

Let Embedded Image By definition α(k)=nextk(α(0),…,α(k−1)), i.e. Embedded Image Moreover, since nextk is an optimal strategy we have, for all Embedded Image that Embedded Image  ■

(a) Variant of finite games of unbounded length

The generalization of finite games to unbounded games considered above relies on the set of outcomes R being discrete (and q being continuous). What if R is not discrete, e.g. Embedded Image? Another way to ensure that every play in the game is finite is to assume that each outcome rR determines the length of the play to be considered, via a fixed mapping Embedded Image, which we will call the ‘clock function’.

Definition 6.7 (Unbounded game with explicit control)

A finite but unbounded sequential game with explicit control is a tuple Embedded Image where

  • — R is the set of possible outcomes of the game,

  • — Xi is the set of possible moves at round i,

  • — ϕi: SRXi is the multi-valued quantifier for round i,

  • — Embedded Image is the outcome function, and

  • — Embedded Image is the clock function.2

A sequence Embedded Image is called a play of the game. The relevant part of a play α is the finite initial segment Embedded Image of length n=l(q(α)).

Therefore, only finite initial segments of infinite plays are to be considered, although the non-relevant extension may be crucial to deciding the outcome of the game (a different non-relevant extension might lead to a different outcome). In fact, the length of the relevant part of the infinite play is only determined once we have fixed the infinite play α. As we are only interested in finite games, we assume that for each set of moves Xi there exists a canonical element ciXi, and that Embedded Image is the infinite sequence of canonical elements from Xk onwards. In this way, after each finite play x we check whether the canonical extension of x is such that its relevant part is an initial segment of x. If so, we have already played past the relevant part of the game and we can stop, since we only require that the first n=l(q(α)) moves be optimal. All other (non-relevant) moves might not necessarily be optimal.

Although this sort of unbounded finite game seems less natural than the one introduced in definition 6.1, we show in §7 that it does appear naturally in proof theory, from computational interpretations of ineffective principles (see §7f).

We now show how to compute plays which have an optimal relevant part. First, we must adapt the notion of optimal strategy to take into account the explicit control function Embedded Image.

Definition 6.8 (Optimal strategy for variant of unbounded game)

A strategy Embedded Image is said to be optimal if for every partial play a=a0,…,ak−1, such that kl(q(a*βa)) we have Embedded Image

In particular, notice that if nextk is an optimal strategy in the above sense, then for every partial play a=a0,…,ak−1 we have Embedded Image for all kjl(q(a*βa)), where b is the strategic play of length jk, starting from a. This is obtained by a simple iteration, always taking a to be longer and longer along the strategic play, until the condition kl(q(a*βa)) no longer holds. As in §§5 and 6, we now define a slightly different iterated product of selection functions that computes such optimal strategies for unbounded games with explicit control.

Definition 6.9 (Unbounded product of selection functions with explicit control)

Let Embedded Image be fixed. Given an infinite sequence of selection functions εi: JRXi and an outcome function Embedded Image, we define the unbounded product of Embedded Image by simply iterating the binary product of selection functions as Embedded Image

The following theorem shows how (as in theorems 5.7 and 6.5) the product of selection functions defined above computes optimal strategies for unbounded games with explicit control.

Theorem 6.10 (Main theorem for unbounded games with explicit control)

Let an unbounded sequential game with explicit control Embedded Image be given. If the quantifiers ϕi have associated selection functions εi then an optimal strategy in the game can be computed as Embedded Image where x=x0,…,xk−1.

Proof.

Let x=x0,…,xk−1 and assume l(q(x*βx))≥k. First, note that this implies l(q(x*c))≥k, as otherwise, by the definition of the strategy nextk we would have that βx=c, and get a contradiction. Hence, by the definition of the strategic move at round k we have Embedded Image By a variant of lemma 6.4 to the explicitly controlled product, each component of the product of selection functions above corresponds to a strategic move from the initial partial play x,xk, i.e. Embedded Image By the fact that εk is a selection function for ϕk we get Embedded Image The result follows since q(x,βx(k)*βx,βx(k))=q(x*βx). ■

As a corollary, we obtain that the following set of equations can be solved via the product of selection functions. The following is another possible generalization of corollary 5.8. Since we no longer require R to be discrete, but assume a clock function instead, corollary 6.11 seems to be orthogonal to corollary 6.6.

Corollary 6.11

Let an unbounded game Embedded Image with explicit control be given. If the quantifiers ϕi have associated selection functions εi then there are functions pi: Xi→R, such that Embedded Image for 0 ≤ i ≤ l(q(α)), where α is the ε-strategic play arising from the optimal strategy described in theorem 6.10.

Proof.

Let Embedded Image By definition α(k)=nextk(α(0),…,α(k−1)), i.e. Embedded Image Moreover, since nextk is an optimal strategy we have Embedded Image for all kl(q(α)). ■

7. Selection functions everywhere

In this section, we show how these natural notions of finite (definitions 3.1 and 4.1) and unbounded (definitions 6.1 and 6.7) sequential games, and the corresponding computation of optimal strategies, has appeared in several different areas. We start each subsection by defining a particular instance of the game, fixing the the set of outcomes R, the sets of moves Xi, the (multi-valued) quantifiers ϕi and the outcome function Embedded Image. After each instantiation a discussion will follow showing how the derived optimal strategy, in case ϕi are attainable, corresponds to a known concept in a particular field of research. In some cases we will assume the reader is familiar with particular notions of each field, as it would be difficult to give all background necessary for each particular application discussed.

(a) Algorithms: backtracking

Consider first the following simple instance of the finite game with single-valued quantifiers (definition 3.1).

  • — Outcomes and moves. Let the set of outcomes and the set of moves at each round be the Booleans Embedded Image, i.e. Embedded Image for all 0≤i<n.

  • — Quantifiers. The quantifiers Embedded Image are given by the existential quantifier Embedded Image

  • — Outcome function. For the outcome function take a Boolean formula on n variables, i.e. Embedded Image.

First, note that the optimal outcome Embedded Image calculates whether the formula q is satisfiable or not, whereas an optimal play a returns a satisfying assignment which makes q true in case the formula is satisfiable. Note also that Embedded Image are selection functions for Embedded Image, i.e. given any Embedded Image we have Embedded Image By theorem 5.7 the product of selection functions computes an optimal play, i.e. a satisfying assignment in case the formula is satisfiable. Observing how the product of selection functions operates in this particular case, we note that the computation of the satisfying assignment is done backtracking. Each individual selection function εi performs an exhaustive search on the space Embedded Image in order to find a witness for Embedded Image, when put together, the product of selection function is then able to perform an exhaustive search on the product space Embedded Image.

We note, however, that a search only happens when the formula q queries a particular variable xi. Therefore, if the value of q is already decided given a few particular values the backtracking terminates that search branch and tries a different branch. In other words, in this particular case the products of selection functions perform backtracking with ‘automatic’ pruning.

(b) Fixed point theory: Bekič’s lemma

Consider the following instance of the finite game with multi-valued quantifiers (definition 4.1).

  • — Outcomes and moves. The sets of moves Xi are fixed sets each endowed with a fixed point operator Embedded Image We are assuming now to be working in some particular model or ‘domain’ where such fixed point operators exist. The set of outcomes will be the product space Embedded Image.

  • — Quantifiers. The multi-valued quantifiers ϕi: (XiR)→2R are given as Embedded Image where πi: RXi is the standard ith projection mapping.

  • — Outcome function. The outcome function Embedded Image is a given fixed self-map on the product space.

First we note that εi(pXiR)=fixi(πi°p) are selection functions for the multi-valued quantifiers ϕi: (XiR)→2R, i.e. given any p: XiR, we have Embedded Image

By theorem 5.7 we can compute an optimal strategy in this game as Embedded Image This optimal strategy induces an strategic play a which, by corollary 5.8, satisfies Embedded Image and Embedded Image for the given family of functions Embedded Image

Unwinding the definitions of ϕi and εi we, in fact, have Embedded Image and Embedded Image

Hence, ak=(q(a))k, for all 0≤k<n, which is equivalent to saying that q(a)=a. That is, the tuple a is a fixed point for the mapping Embedded Image.

What we have shown is that in this particular instance of the game, the optimal strategy induces a strategic play which computes a fixed point for a mapping on the product space given a family of fixed point operators for each of the individual spaces Xi. Moreover, the whole construction shows that if each space Xi has a fixed point operator, then the product space Embedded Image must also have a fixed point operator. That is the essential content of Bekič’s lemma (Bekič 1984), a celebrated result in fixed point theory, and frequently used in domain theory.

(c) Game theory: Nash equilibrium

Consider now another instance of the finite game with multi-valued quantifiers (definition 4.1) as follows:

  • — Outcomes and moves. Fix sets Xi as the sets of moves, which for simplicity we assume are finite. For the set of outcomes take n-tuples of reals, i.e. Embedded Image.

  • — Quantifiers. The multi-valued quantifiers ϕi: (XiR)→2R are given as Embedded Image where πi: RXi is the standard ith projection mapping. That is, ϕi returns all the elements in the co-domain of p which have maximal value at coordinate i.

  • — Outcome function. The outcome function Embedded Image is a given mapping from plays to n-tuples of real numbers.

First, since all quantifiers are different, we can think of this as an n-player game. Moreover, the outcome function can be thought of as calculating the payoff each of the n players gets at the end of the game. The quantifiers say that all players are trying to maximize their own payoffs, without paying attention to what impact this might have on other players. Note also that Embedded Image are selection functions for the multi-valued quantifiers Embedded Image, i.e. given any Embedded Image we have Embedded Image By theorem 5.7, we can compute an optimal strategy in this game as Embedded Image A strategy being optimal means Embedded Image which, unwinding the definition of ϕk gives Embedded Image This is saying that the move bak suggested by the strategy leads to an outcome with maximal payoff for player k. It follows that the strategy nextk is in Nash equilibrium, as no player has any incentive to unilaterally change their strategy for round k. In this example, the construction of optimal strategies via products of selection functions corresponds to backward induction, a technique used in Game Theory (Nisan et al. 2007) to compute Nash equilibria in sequential games.

(d) Higher type computability: searchable sets

Consider now the following instance of the unbounded game (definition 6.1), which generalizes the finite game of §7a.

  • — Outcomes and moves. Let R be the domain of Boolean values Embedded Image and each Xi be subsets Si of a fixed domain A.

  • — Quantifiers. Let the quantifiers Embedded Image be the existential quantifiers over the subsets SiA.

  • — Outcome function. For the outcome function we will take an arbitrary predicate on the product space of the Si’s, i.e. Embedded Image.

First, we note that the assumption that ϕi are attainable correspond in this case to the sets Si being searchable, as defined in Escardó (2008).

It turns out that any searchable set (of total elements) is topologically compact, and, mimicking the Tychonoff theorem from topology, it was shown in Escardó (2008) that searchable sets are closed under countable products. For that one must essentially show that the game above defined has an optimal strategy, and that the optimal play witnesses q whenever q is a non-empty predicate.

In fact, the construction used in Escardó (2008) is a particular case of the iterated product of selection function (definition 6.3), and it was precisely this observation that led us to look at this construction in more details.

(e) Proof theory: arithmetic

In the next examples we show how the finite product of selection functions gives a computational interpretation to arithmetic, whereas the unbounded product interprets full classical analysis. Consider the principle of bounded collection for existential formulas, i.e. Embedded Image where A(n,m) is a Embedded Image-formula. It is well-known that such principle lies in between Embedded Image-induction and Embedded Image-induction, see Parsons (1970) and Kohlenbach (2008). For simplicity, let us consider the case when A(n,m)=∃kA0(n,m,k) where A0(n,m,k) is quantifier free, i.e. Embedded Image The negative translation (assuming Markov principle) of this principle is equivalent to Embedded Image Its dialectica interpretation, see Avigad & Feferman (1998), is Embedded Image In other words, given f,g and ε we must produce n,b and p, such that Embedded Image This boils down to producing n,b,p given f,g,εn such that for some mb we have Embedded Image 7.1 assuming f is bounded by t. We show that this can be solved using the optimal strategy of the following finite game. Let f,g and (εn)nt be given.

  • — Outcomes and moves. The sets of moves Xi and the set of outcomes R is taken to be the natural numbers Embedded Image.

  • — Quantifiers. The quantifiers Embedded Image are defined from the given selection functions Embedded Image so that ϕi is attainable by definition.

  • — Outcome function. The outcome function Embedded Image is taken to be Embedded Image

Given that the quantifiers are attainable, we can compute the optimal strategy of this game, and its respective strategic play Embedded Image By corollary 5.8 we have that there are functions Embedded Image such that Embedded Image and Embedded Image for 0≤nt. Take Embedded Image and n=fb (because f is bounded by t we have nt) and p=pn and m=an. We show that this solves the set of equations (7.1). By definition n=fb and m=an=εnpn=εnp. By the definition of q we also have Embedded Image This is essentially the solution given in Oliva (2006) for the dialectica interpretation of the infinite pigeon-hole principle, but here it is given an intuitive game-theoretic explanation.

(f) Proof theory: analysis

The product of selection functions also appears in proof theory, in the form of bar recursion (Spector 1962). More precisely, in order to extend Gödel’s consistency proof (Gödel 1958) from arithmetic to analysis, Spector arrived at the following system of equations: Given a family of (selection) functions εi: JYX and functions r: XωY and Embedded Image find p: XY and α: Xω, such that Embedded Image and Embedded Image We show now that this system of equations can be solved from the optimal strategy of the following unbounded game with explicit control (definition 6.7):

  • — Outcomes and moves. Let Embedded Image and Xi=X.

  • — Quantifiers. The quantifiers ϕi: (XR)→2R are defined from the εi’s as Embedded Image

  • — Outcome function. The outcome function Embedded Image is Embedded Image where r: XωY and Embedded Image are as given in Spector’s equations.

  • — Clock function. Let Embedded Image be the second projection, i.e. l(α,n)=n.

By corollary 6.11, we have that for the strategic play α: Xω there are Embedded Image, such that Embedded Image and Embedded Image for 0≤il(q(α)), where α is the ε-strategic play. Unwinding the definitions of ϕ,q and l, and taking Embedded Image we have Embedded Image and Embedded Image for 0≤iω(α), which solves Spector’s equations taking i=ω(α) and Embedded Image. In other words, the notion required to extend Gödel’s consistency proof from arithmetic to analysis was the computation of optimal strategies for unbounded games with explicit control.

We have shown that in fact Spector’s bar recursion is primitive recursive equivalent to the product of selection functions from definition 6.9, and that a different form of bar recursion (Berardi et al. 1998; Berger & Oliva 2005, 2006) is primitive recursive equivalent to the product of selection functions from definition 6.3. The second form of bar recursion arose from a game computational interpretation of classical logic (Coquand 1995), and it would be interesting to investigate in further detail how our notion of games corresponds to the one used to interpret classical logic. See also Aczel (2001) for more connections between strong monads and classical logic.

(g) Functional programming

We have also shown in Escardó & Oliva (2010c) that the construction JR over any cartesian closed category gives rise to a strong monad, with the monad morphism Embedded Image into the well-known continuation monad KR (Griffin 1990). This monad morphism assigns the quantifier Embedded Image defined by equation (5.1) to a given selection function εJRA. Moreover, the case n=2 of the product of selection functions turns out to be simply the canonical map that makes any strong monad into a monoidal monad.

Monads are widely used in programming language semantics as a way to interpret side-effects (Moggi 1991) and in functional programming, particularly in the language Haskell, more generally as a way of structuring programs. As it turns out—see Escardó & Oliva (2010d)—the ability to iterate this binary product into an infinite product is already built into the Haskell language, once the selection monad is defined. All constructions described here can be easily implemented in functional programming, as done in Escardó & Oliva (2010d). In fact, experimental results show that the calculation of optimal strategies using the iterated product of selection functions is computationally very efficient with respect to both time and space.

8. Games in normal and extensive form

The games discussed in this paper are presented in what is known as normal form in the literature (von Neumann & Morgenstern 1944). This means that one is given an outcome function q that associates outcomes to plays (sequences of moves). For games presented in extensive form one organizes the set of all possible plays as a decision tree, as also discussed by von Neumann & Morgenstern (1944), who show that the two presentations are mathematically equivalent. For each node of the tree there is a set of edges labelled by the moves that can follow that node, leading to subtrees. Each leaf of the tree is labelled by an outcome. Given a sequence of moves, one follows the tree starting from the root until a leaf is obtained, from which one reads off the outcome of the play. The presentation of games in extensive form allows one to see that the n-ary product of selection functions (definition 5.6) corresponds to backward induction, as discussed in §7c.

For games of fixed, finite length n, all leafs are at level n of the tree. For a game of unbounded, finite length, leafs can occur at any level of the tree, but it is required that all paths eventually lead to a leaf. Trees which enjoy this property are called well founded. The well-foundedness condition for games in extensive form is equivalent to our continuity condition (6.1) for games in normal form.

Note that in the finite case, the optimal play (⊗i<nεi)(q) of the game q can be seen as defined by induction on n, but this does not make sense for the infinite product of selection functions. In both the finite and infinite case, for q continuous, the outcome (⊗iεi)(q) can be seen as defined by structural induction on the well-founded tree that defines q in extensive form (see Escardó & Oliva 2010c for details). Thus, curiously, in the finite case, the same construction of (⊗i<nεi)(q) can be seen at the same time as a definition by induction on n and as a definition by induction on the extensive form of q.

The above discussion shows that bar recursion, mentioned in §7f, amounts to recursion on well-founded trees, where the trees are indirectly presented as continuous functions Embedded Image.

Acknowledgements

The authors would like to thank the two anonymous referees for their detailed comments and suggestions which greatly improved the presentation of the paper. The second author (P.O.) also gratefully acknowledges the support of The Royal Society under grant 516002.K501/RH/kk.

Footnotes

  • 1 For example, the natural numbers or more generally the types defined in Escardó (2008, definition 4.12).

  • 2 For instance, if Embedded Image we could take l(⋅) to be the second projection.

  • Received September 8, 2010.
  • Accepted November 3, 2010.

This is an open-access article distributed under the terms of the Creative Commons Attribution License, which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited.

References

View Abstract