| Böhm's Theorem for Berarducci Trees (2000) | |||||||||||||||
Abstract | |||||||||||||||
| We propose an extension of lambda calculus which internally discriminates two lambda terms if and only if they have dierent Berarducci trees. 1 Introduction The Lambda Calculus is a theory of functions that serves as a foundation for the functional programming paradigm. Lambda terms in this view are idealized programs. There are essentially two ways of characterizing the meaning of lambda terms. The rst one is to run the program and to study the output. The second one is to observe the eect of the program when used as a subprogram in other programs. With respect to the rst approach, traditionally the output of a lambda term was described by its Bohm tree. But also Levy-Longo trees and more recently Berarducci trees have been used. In this paper we will focus on Berarducci trees. These trees provide the possible output of a lambda term in greatest detail. The idea behind all these dierent concepts of tree is stable information, that we can recover by reducing the terms. This is ... | |||||||||||||||
Details der Publikation | |||||||||||||||
| |||||||||||||||