Logo Logo
Hilfe
Hilfe
Switch Language to English

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 [PDF, 1MB]

[thumbnail of 4261.pdf]
Vorschau
Download (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.

Dokument bearbeiten Dokument bearbeiten