BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.bham.ac.uk//v3//EN
BEGIN:VEVENT
CATEGORIES:Lab Lunch
SUMMARY:Selection functions\, bar recursion and backward i
nduction - Martin Escardo
DTSTART:20090929T120000Z
DTEND:20090929T130000Z
UID:TALK74AT
URL:/talk/index/74
DESCRIPTION:I'll talk about my recent work with Paulo Oliva fr
om Queen Mary\nreported in the paper "Selection fu
nctions\, bar recursion and backward\ninduction".
Here is the abstract of the paper:\n Bar recursi
on arises in constructive mathematics\, logic\, pr
oof\ntheory and higher-type computability theory.
We explain bar recursion\nin terms of sequential g
ames\, and show how it can be naturally\nunderstoo
d as a generalisation of the principle of backward
induction\nthat arises in game theory. In summary
\, bar recursion calculates\noptimal plays and opt
imal strategies\, which\, for particular games of\
ninterest\, amount to equilibria. We consider fini
te games and\ncontinuous countably infinite games\
, and relate the two. The above\ndevelopment is fo
llowed by a conceptual explanation of how the fini
te\nversion of the main form of bar recursion cons
idered here arises from\na strong monad of selecti
ons functions that can be defined in any\ncartesia
n closed category. Finite bar recursion turns out
to be a\nwell-known morphism available in any str
ong monad\, specialised to the\nselection monad.\n
Obviously I won't have time to talk about all that
(and the monad\nstuff was already done in previou
s lab lunches).
LOCATION:CS 217
CONTACT:Dan Ghica
END:VEVENT
END:VCALENDAR