Tags:affine closed lambda term, affine closed term, affine term, closed term, combinatoric, de bruijn index, de bruijn indices, integer sequence, lambda calculus, linear closed term, linear term, natural size and variable size

Abstract:

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 variable occurs once and only once. In this paper we count the number of affine closed lambda-terms of size n, linear closed lambda-terms of size n, affine closed beta-normal forms of size n and linear closed beta-normal forms of size n, for several measures of 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. The foundation of all of this is a specific data structure, made of contexts in which one counts all the holes at each level of abstractions by lambda's.

How to count linear and affine closed lambda terms?