**
**

**Berger, Ulrich and 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 [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.

Item Type: | Conference or Workshop Item (Other) |
---|---|

Faculties: | Mathematics, Computer Science and Statistics > Mathematics |

Subjects: | 500 Science > 510 Mathematics |

URN: | urn:nbn:de:bvb:19-epub-4261-0 |

Language: | English |

Item ID: | 4261 |

Date Deposited: | 05. Jun 2008, 13:08 |

Last Modified: | 13. Aug 2024, 12:40 |