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. (Hrsg.): In: Proceedings of the 6th Symposium on Logic in Computer Science (LICS'91), IEEE Computer Society Press, Los Alamitos. S. 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.

• Dokumententyp: Konferenzbeitrag (Anderer)
• Fakultät: Mathematik, Informatik und Statistik > Mathematik
• Themengebiete: 500 Naturwissenschaften und Mathematik > 510 Mathematik
• Sprache: Englisch