An inverse of the evaluation functional for typed Lambda-calculus

Berger, Ulrich und Schwichtenberg, Helmut (1991): An inverse of the evaluation functional for typed Lambda-calculus. 6th Annual IEE Symposium on Logic in Computer Science (LICS'91), Amsterdam, 15. - 18. Juli 1991. Vermuri, R. (ed.) : In: Proceedings of the 6th Symposium on Logic in Computer Science (LICS'91), IEEE Computer Society Press, Los Alamitos. pp. 203-211

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.

• Item Type: Conference or Workshop Item (Other)
• Faculties: Mathematics, Computer Science and Statistics > Mathematics
• Subjects: 500 Science > 510 Mathematics
• Language: English