## Paper: An inverse of the evaluation functional for typed λ-calculus (at LICS 1991)

**Ulrich Berger Helmut Schwichtenberg**

### Abstract

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

### BibTeX

@InProceedings{BergerSchwichtenber-Aninverseoftheevalu, author = {Ulrich Berger and Helmut Schwichtenberg}, title = {An inverse of the evaluation functional for typed λ-calculus }, booktitle = {Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science (LICS 1991)}, year = {1991}, month = {July}, pages = {203--211}, location = {Amsterdam, The Netherlands}, publisher = {IEEE Computer Society Press} }