Computability in Europe 2006
Logical Approaches to Computational Barriers

Special Session Talk:
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