Abstract
This dissertation concerns the computational interpretation of analysis via proof interpretations, and examines the variants of bar recursion that have been used to interpret the axiom of choice. It consists of an applied and a theoretical component.
The applied part contains a series of case studies which address the issue of understanding the meaning and behaviour of bar recursive programs extracted from proofs in analysis. Taking as a starting point recent work of Escardo and Oliva on the product of selection functions, solutions to Goedel’s functional interpretation of several well known theorems of mathematics are given, and the semantics of the extracted programs described. In particular, new gametheoretic computational interpretations are found for weak Koenig’s lemma for Σ^0_1trees and for the minimalbadsequence argument.
On the theoretical side several new definability results which relate various modes of
bar recursion are established. First, a hierarchy of fragments of system T based on finite
bar recursion are defined, and it is shown that these fragments are in onetoone correspondence with the usual fragments based on primitive recursion. Secondly, it is shown that the so called ‘special’ variant of Spector’s bar recursion actually defines the general one. Finally, it is proved that modified bar recursion (in the form of the implicitly controlled product of selection functions), open recursion, update recursion and the BerardiBezemCoquand realizer for countable choice are all primitive recursively equivalent in the model of continuous functionals.
The applied part contains a series of case studies which address the issue of understanding the meaning and behaviour of bar recursive programs extracted from proofs in analysis. Taking as a starting point recent work of Escardo and Oliva on the product of selection functions, solutions to Goedel’s functional interpretation of several well known theorems of mathematics are given, and the semantics of the extracted programs described. In particular, new gametheoretic computational interpretations are found for weak Koenig’s lemma for Σ^0_1trees and for the minimalbadsequence argument.
On the theoretical side several new definability results which relate various modes of
bar recursion are established. First, a hierarchy of fragments of system T based on finite
bar recursion are defined, and it is shown that these fragments are in onetoone correspondence with the usual fragments based on primitive recursion. Secondly, it is shown that the so called ‘special’ variant of Spector’s bar recursion actually defines the general one. Finally, it is proved that modified bar recursion (in the form of the implicitly controlled product of selection functions), open recursion, update recursion and the BerardiBezemCoquand realizer for countable choice are all primitive recursively equivalent in the model of continuous functionals.
Original language  English 

Qualification  Ph.D. 
Awarding Institution 

Supervisors/Advisors 

Award date  31 Oct 2013 
Publication status  Published  2013 