An inverse of the evaluation functional for typed lambda-calculus
Ulrich Berger and Helmut Schwichtenberg

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

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}

Draft copy