Counting and Generating Terms in the Binary Lambda Calculus (Extended version)

TL;DR

This paper analyzes the enumeration of lambda calculus terms encoded as binary sequences, deriving growth rates and introducing a method to generate random terms using Boltzmann samplers.

Contribution

It provides a detailed enumeration of binary-encoded lambda terms and presents a novel approach to randomly generate such terms using Boltzmann sampling techniques.

Findings

Number of lambda terms of size n grows roughly like 1.963447954^n.

Derived generating functions for counting lambda terms.

Introduced a method for random generation of lambda terms.

Abstract

In a paper entitled Binary lambda calculus and combinatory logic, John Tromp presents a simple way of encoding lambda calculus terms as binary sequences. In what follows, we study the numbers of binary strings of a given size that represent lambda terms and derive results from their generating functions, especially that the number of terms of size n grows roughly like 1.963447954. .. n. In a second part we use this approach to generate random lambda terms using Boltzmann samplers.