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}