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

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 -theorems in classical analysis.

• Type: Conference
• Year: 2006
• Where: CIE
• Authors: Paulo Oliva
• Keywords: Abstruse Recursion Schema, Applied Computing, Bar Recursion, CIE 2006, So-called Bar Recursion