|
Berger, Ulrich; Schwichtenberg, Helmut
(1991):
An inverse of the evaluation functional for typed Lambda-calculus.
6th Annual IEE Symposium on Logic in Computer Science (LICS'91), 15. - 18. Juli 1991, Amsterdam.
|
![[img]](https://epub.ub.uni-muenchen.de/4261/1.hassmallThumbnailVersion/4261.pdf)  Vorschau |
|
PDF
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 X-terms, Combined with the evaluation
functional, p-e yields an efficient normalization algorithm.
The method is extended to X-calculi with constants
and is used to normalize (the X-representations
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.
