A natural counting of lambda terms

TL;DR

This paper investigates the enumeration and properties of lambda terms of given sizes, establishing bijections with binary trees and analyzing the distribution of normal forms, revealing that strongly normalizing terms are rare.

Contribution

It introduces a natural size model for lambda terms, connects them to binary trees via bijections, and studies the distribution of various normal forms.

Findings

Strongly normalizing terms have density zero among plain lambda terms.

Bijections between lambda terms and binary trees are established.

Distribution analysis of normal forms and head normal forms.

Abstract

We study the sequences of numbers corresponding to lambda terms of given sizes, where the size is this of lambda terms with de Bruijn indices in a very natural model where all the operators have size 1. For plain lambda terms, the sequence corresponds to two families of binary trees for which we exhibit bijections. We study also the distribution of normal forms, head normal forms and strongly normalizing terms. In particular we show that strongly normalizing terms are of density 0 among plain terms.