Berger, Ulrich; Schwichtenberg, Helmut
(1991):
An inverse of the evaluation functional for typed Lambdacalculus.
6th Annual IEE Symposium on Logic in Computer Science (LICS'91), 15.  18. Juli 1991, Amsterdam.

Preview 

1MB 
Abstract
In any model of typed λcalculus conianing some basic
arithmetic, a functional p  * (procedure—* expression)
will be defined which inverts the evaluation functional
for typed Xterms, Combined with the evaluation
functional, pe yields an efficient normalization algorithm.
The method is extended to Xcalculi with constants
and is used to normalize (the Xrepresentations
of) natural deduction proofs of (higher order) arithmetic.
A consequence of theoretical interest is a strong
completeness theorem for βηreduction, generalizing
results of Friedman [1] and Statman [31: If two Xterms
have the same value in some model containing
representations of the primitive recursive functions
(of level 1) then they are provably equal in the βη
calculus.