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

Katarzyna Grygiel (1) , Pierre Lescanne (1, 2)

1 TCS - Theoretical Computer Science Department [Krakow]
2 LIP - Laboratoire de l'Informatique du Parallélisme

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.

Keywords: lambda calculus; combinatorics; functional programming; test; random generator; ranking; unranking; Boltzmann sampler

Domains: Computer Science [cs]; Computer Science and Game Theory [cs.GT]

Katarzyna Grygiel, Pierre Lescanne. Counting and Generating Terms in the Binary Lambda Calculus (Extended version). 2015. ⟨ensl-01229794⟩