Logical Approaches to Computational Barriers

Understanding and Using Spector's Bar Recursive Interpretation of Classical Analysis

Speaker:
| Paulo Oliva |

Author(s): |
Paulo Oliva |

This note reexamines Spector's remarkable computational interpretation of full classical analysis. Spector's interpretation makes use of a rather abstruse recursion schema, so-called bar recursion, used to interpret the double negation shift DNS. In this note bar recursion is presented as a generalisation of a simpler primitive recursive functional needed for the interpretation of a finite (intuitionistic) version of DNS. I will also present two concrete applications of bar recursion in the extraction of programs from proofs of forall-exists-theorems in classical analysis.

websites: Arnold Beckmann | 2006-07-04 |