An inverse of the evaluation functional for typed λ-calculus

A functional p→e (procedure→expression) that inverts the evaluation functional for typed λ-terms in any model of typed λ-calculus containing some basic arithmetic is defined. Combined with the evaluation functional, p→e yields an efficient normalization algorithm. The method is extended to λ-calculi with constants and is used to normalize (the λ-representations of) natural deduction proofs of (higher order) arithmetic. A consequence of theoretical interest is a strong completeness theorem for βη-reduction. If two λ-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 βη-calculus