University of Birmingham > Talks@bham > Theoretical computer science seminar > Closure of system T under the bar recursion rule

## Closure of system T under the bar recursion ruleAdd to your list(s) Download to your calendar using vCal - Paulo Oliva (Queen Mary, University of London)
- Friday 24 February 2017, 11:00-12:00
- Computer Science, The Sloman Lounge (UG).
If you have a question about this talk, please contact Paul Taylor. Bar recursion (BR) is a form of recursive definition proposed by Spector [1] to extend system T so as to give a computational interpretation to proofs in classical analysis. It follows that T + BR is strictly more expressive than system T. Bar recursion can be viewed as form of recursion on well-founded trees. A celebrated result of Schwichtenberg [2] implies that if we restrict to T-definable trees, then BR of lowest type will not take us outside T-definability. This closure property is proven in [2] via a reduction to an infinitary version of system T, following by the use of ordinal recursion, and the translation of these back into system T. In [3] we have given a more direct proof, with an explicit construction that given a term in T + BR of restricted type, will convert that into a T term. [1] Spector, C., Provably recursive functionals of analysis, Recursive Function Theory: Proc. Symposia in Pure Mathematics, 5, 1–27, 1962 [2] Schwichtenberg, H., On bar recursion of types 0 and 1, The Journal of Symbolic Logic, 44, 325–329, 1979 [3] Oliva, P. and Steila, S., A direct proof of Schwichtenberg’s bar recursion closure theorem, under review. This talk is part of the Theoretical computer science seminar series. ## This talk is included in these lists:- Computer Science Departmental Series
- Computer Science Distinguished Seminars
- Computer Science, The Sloman Lounge (UG)
- Theoretical computer science seminar
- computer sience
Note that ex-directory lists are not shown. |
## Other listsCentre for Computational Biology Seminar Series Analysis seminar Type the title of a new list here## Other talksTest talk TBC Quantum simulations using ultra cold ytterbium Extending the Lax type operator for finite W-algebras Provably Convergent Plug-and-Play Quasi-Newton Methods for Imaging Inverse Problems Ultrafast, all-optical, and highly efficient imaging of molecular chirality |