Quantitative aspects of linear and affine closed lambda terms


Abstract in English

Affine $lambda$-terms are $lambda$-terms in which each bound variable occurs at most once and linear $lambda$-terms are $lambda$-terms in which each bound variables occurs once. and only once. In this paper we count the number of closed affine $lambda$-terms of size $n$, closed linear $lambda$-terms of size $n$, affine $beta$-normal forms of size $n$ and linear $beta$-normal forms of ise $n$, for different ways of measuring the size of $lambda$-terms. From these formulas, we show how we can derive programs for generating all the terms of size $n$ for each class. For this we use a specific data structure, which are contexts taking into account all the holes at levels of abstractions.

Download