Polymorphic extensions of simple type structures. With an application to a bar recursive minimization Original Research Article

The technical contribution of this paper is threefold. First we show how to encode functionals in a ‘flat’ applicative structure by adding oracles to untyped λ-calculus and mimicking the applicative behaviour of the functionals with an impredicatively defined reduction relation. The main achievement here is a Church-Rosser result for the extended reduction relation. Second, by combining the previous result with the model construction based on partial equivalence relations, we show how to extend a λ-closed simple type structure to a model of the polymorphic λ-calculus. Third, we specialize the previous result to a counter model against a simple minimization. This minimization is realized by a bar recursive functional, which contrasts the results of Spector and Girard which imply that the bar recursive functions are exactly those that are definable in the polymorphic λ-calculus. As a spin-off, we obtain directly the non-conservativity of the extensions of Gödelʹs T with bar recursion, fan functional, and Luckhardtʹs minimization functional, respectively. For the latter two extensions these results are new.