# Quantitative aspects of linear and affine closed lambda terms

## TL;DR

This paper provides combinatorial counts and generation algorithms for various classes of closed affine and linear lambda-terms and their normal forms, based on size measurements and context data structures.

## Contribution

It introduces formulas for counting and generating closed affine and linear lambda-terms and their normal forms using context-based data structures.

## Key findings

- Formulas for counting lambda-terms and normal forms by size.
- Algorithms for generating all terms of a given size.
- Use of context data structures for term enumeration.

## 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 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.