Understanding and using spector's bar recursive interpretation of classical analysis

Abstract

This note reexamines Specter's remarkable computational interpretation of full classical analysis. Specter'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 ∀∃-theorems in classical analysis. © Springer-Verlag Berlin Heidelberg 2000.