We consider a special case of Dickson's lemma: for any two functions $f,g$ on the natural numbers there are two numbers $i

The importance of an abstract approach to a computation theory over general data types has been stressed by Tucker in many of his papers. Berger and Seisenberger recently elaborated the idea for extraction out of proofs involving (only) abstract reals. They considered a proof involving coinduction of the proposition that any two reals in [−1, 1] have their average in the same interval, and informally extract a Haskell program from this proof, which works with stream representations of reals. Here we formalize the proof, and machine extract its computational content using the Minlog proof assistant. This required an extension of this system to also take coinduction into account.

A syntactical proof is given that all functions definable in a certain affine linear typed λ-calculus with iteration in all types are polynomial time computable. The proof provides explicit polynomial bounds that can easily be calculated.

A purely syntactical proof is given that all functions definable in a certain affine linear typed /spl lambda/-calculus with iteration in all types are polynomial time computable. The proof also gives explicit polynomial bounds that can easily be calculated.

A functional p to e (procedure to expression) that inverts the evaluation functional for typed lambda -terms in any model of typed lambda -calculus containing some basic arithmetic is defined. Combined with the evaluation functional, p to e yields an efficient normalization algorithm. The method is extended to lambda -calculi with constants and is used to normalize (the lambda -representations of) natural deduction proofs of (higher order) arithmetic. A consequence of theoretical interest is a strong completeness theorem for beta eta -reduction. If two lambda -terms have the same value in some model containing representations of the primitive recursive functions (of level 1) then they are probably equal in the beta eta -calculus.>

For general information on bar recursion the reader should consult the papers of Spector [8], where it was introduced, Howard [2] and Tait [11]. In this note we shall prove that the terms of Gödel's theory T(in its extensional version of Spector [8]) are closed under the rule BR0,1 of bar recursion of types 0 and 1. Our method of proof is based on the notion of an infinite term introduced by Tait [9]. The main tools of the proof are (i) the normalization theorem for (notations for) infinite terms and (ii) valuation functionals. Both are elaborated in [6]; for brevity some familiarity with this paper is assumed here. Using (i) and (ii) we reduce BR0,1 to ξ-recursion with ξ < ε0. From this the result follows by work of Tait [10], who gave a reduction of 2ξ-recursion to ξ-recursion at a higher type. At the end of the paper we discuss a perhaps more natural variant of bar recursion introduced by Kreisel in [4]. Related results are due to Kreisel (in his appendix to [8]), who obtains results which imply, using the reduction given by Howard [2] of the constant of bar recursion of type τ to the rule of bar recursion of type (0 → τ) → τ, that T is not closed under the rule of bar recursion of a type of level ≥ 2, to Diller [1], who gave a reduction of BR0,1 to ξ-recursion with ξ bounded by the least ω-critical number, and to Howard [3], who gave an ordinal analysis of the constant of bar recursion of type 0. I am grateful to H. Barendregt, W. Howard and G. Kreisel for many useful comments and discussions.