Distribution of variables in lambda-terms with restrictions on De Bruijn indices and De Bruijn levels

TL;DR

This paper analyzes the distribution of variables in restricted lambda-terms with bounded De Bruijn indices and levels, showing asymptotic normality and deriving formulas for key constants, with insights into their structural profiles.

Contribution

It provides the first asymptotic analysis of variable distribution in lambda-terms with bounded De Bruijn indices and levels, including explicit formulas for constants and structural profiles.

Findings

Variables are asymptotically normally distributed in both subclasses.

Mean and variance of variables grow linearly with the size of the lambda-terms.

The study reveals a distinctive 'unary profile' across De Bruijn levels.

Abstract

We investigate the number of variables in two special subclasses of lambda-terms that are restricted by a bound of the number of abstractions between a variable and its binding lambda, the so-called De-Bruijn index, or by a bound of the nesting levels of abstractions, \textit{i.e.}, the number of De Bruijn levels, respectively. These restrictions are on the one hand very natural from a practical point of view, and on the other hand they simplify the counting problem compared to that of unrestricted lambda-terms in such a way that the common methods of analytic combinatorics are applicable. We will show that the total number of variables is asymptotically normally distributed for both subclasses of lambda-terms with mean and variance asymptotically equal to $Cn$ and $\tilde{C}n$, respectively, where the constants $C$ and $\tilde{C}$ depend on the bound that has been imposed. So far we just derived closed formulas for the constants in case of the class of lambda-terms with bounded De Bruijn index. However, for the other class of lambda-terms that we consider, namely lambda-terms with a bounded number of De Bruijn levels, we investigate the number of variables, as well as abstractions and applications, in the different De Bruijn levels and thereby exhibit a so-called "unary profile" that attains a very interesting shape.