Understanding Exhaustible Sets and Bar Recursion
Martin Escardo ( University of Birmingham )
- 14:00 15th May 2009 ( week 3, Trinity Term 2009 )Lecture Theatre B
In my recent paper "exhaustible sets in higher-type computation", I studied infinite sets that admit exhaustive search in finite time, which is possible to do fast in some surprising instances. I'll briefly summarize this, which will be the background for the talk. A main tool of that paper was a certain functional that, given countably many selection functions for countably many types, produces a selection function for the product of the types.
In this talk, which reports ongoing joint work with Paulo Oliva, I'll show that this product functional turns out to be a form of Bar Recursion, and that it has a specification much more general than that given in the paper mentioned above. For example, it computes winning strategies for sequential games (where selection functions play the role of pay-off functions), and can be seen as a formalization of the principle of backward induction that is often applied in game theory. As another example, fixed-point operators are selection functions, and the product of two fpo's seen as selection functions gives Bekic's fixed-point theorem. More examples and applications (and theorems) will be given in the talk. Moreover, I'll show that the finite product of selection functions is a morphism that exists in any strong monad, specialized to a certain selection monad, which is related to the continuation monad by a monad morphism. The infinite product is the countable iteration of the binary product, but doesn't exist for all strong monads.
In this talk, which reports ongoing joint work with Paulo Oliva, I'll show that this product functional turns out to be a form of Bar Recursion, and that it has a specification much more general than that given in the paper mentioned above. For example, it computes winning strategies for sequential games (where selection functions play the role of pay-off functions), and can be seen as a formalization of the principle of backward induction that is often applied in game theory. As another example, fixed-point operators are selection functions, and the product of two fpo's seen as selection functions gives Bekic's fixed-point theorem. More examples and applications (and theorems) will be given in the talk. Moreover, I'll show that the finite product of selection functions is a morphism that exists in any strong monad, specialized to a certain selection monad, which is related to the continuation monad by a monad morphism. The infinite product is the countable iteration of the binary product, but doesn't exist for all strong monads.
Share this:
