Selection Functions, Bar Recursion and Backward Induction

Research output: Contribution to journalArticle

Standard

Selection Functions, Bar Recursion and Backward Induction. / Escardo, Martin; Oliva, P.

In: Mathematical Structures in Computer Science, Vol. 20, No. 2, 01.04.2010, p. 127-168.

Research output: Contribution to journalArticle

Harvard

APA

Vancouver

Author

Bibtex

@article{6cf9143f4cf64bf89167afb74e6c37cb,
title = "Selection Functions, Bar Recursion and Backward Induction",
abstract = "Bar recursion arises in constructive mathematics, logic, proof theory and higher-type computability 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 the selection monad.",
keywords = "Higher-type computability, exhaustible set, Kleene-Kreisel spaces of continuous functionals",
author = "Martin Escardo and P Oliva",
year = "2010",
month = apr,
day = "1",
doi = "10.1017/S0960129509990351",
language = "English",
volume = "20",
pages = "127--168",
journal = "Mathematical Structures in Computer Science",
issn = "0960-1295",
publisher = "Cambridge University Press",
number = "2",

}

RIS

TY - JOUR

T1 - Selection Functions, Bar Recursion and Backward Induction

AU - Escardo, Martin

AU - Oliva, P

PY - 2010/4/1

Y1 - 2010/4/1

N2 - Bar recursion arises in constructive mathematics, logic, proof theory and higher-type computability 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 the selection monad.

AB - Bar recursion arises in constructive mathematics, logic, proof theory and higher-type computability 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 the selection monad.

KW - Higher-type computability

KW - exhaustible set

KW - Kleene-Kreisel spaces of continuous functionals

U2 - 10.1017/S0960129509990351

DO - 10.1017/S0960129509990351

M3 - Article

VL - 20

SP - 127

EP - 168

JO - Mathematical Structures in Computer Science

JF - Mathematical Structures in Computer Science

SN - 0960-1295

IS - 2

ER -