**
An inverse of the evaluation functional for
typed lambda-calculus
**

*
Ulrich Berger and Helmut Schwichtenberg
*

**Abstract**

In any model of the typed lambda-calculus contaning some basic
arithmetic, a functional is defined which
inverts the evaluation functional for typed lambda-terms.
Combined with the evaluation functional, this 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, generalizing results of Friedman
and Statman: If two lambda-terms have the same value
in some model containing
representations of the primitive recursive functions (of level 1)
then they are provably equal in the beta-eta-calculus.

**Bibtex entry**

@Inproceedings{Berger91, Author = "Ulrich Berger and Helmut Schwichtenberg", Title = "An inverse of the evaluation functional for typed $\lambda$--calculus", Booktitle = "Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science", Editor = "R. Vemuri", Pages = "203--211", Publisher = "IEEE Computer Society Press, Los Alamitos", Year = 1991}