Infinite λ-calculus and non-sensible models*
Alessandro Berarducci · 2017
We define a model of λ β -calculus which is similar to the model of Böhm trees, but it does not identify all the unsolvable lambda-terms. The role of the unsolvable terms is taken by a much smaller class of terms which we call mute. Mute terms are those zero terms which are not β -convertible to a zero term applied to something else. We prove that it is consistent with the λ β -calculus to simultaneously equate all the mute terms to a fixed arbitrary closed term. This allows us to strengthen some results of Jacopini and Venturini Zilli concerning easy λ-terms. Our results depend on an infinitary version of λ-calculus. We set the foundations for such a calculus, which might turn out to be a useful tool for the study of non-sensible models of λ-calculus.