On the number of lambda terms with prescribed size of their de Bruijn representation

DOI10.4230/LIPICS.STACS.2016.40zbMATH Open1434.03051arXiv1509.06139OpenAlexW2963632202MaRDI QIDQ4601892FDOQ4601892

Authors: Bernhard Gittenberger, Zbigniew Gołȩbiewski 

Publication date: 24 January 2018

Abstract: John Tromp introduced the so-called 'binary lambda calculus' as a way to encode lambda terms in terms of binary words. Later, Grygiel and Lescanne conjectured that the number of binary lambda terms with $m$ free indices and of size $n$ (encoded as binary words of length $n$) is $o(n^{-3/2}a{u}^{-n})$ for $auapprox1.963448ldots$. We generalize the proposed notion of size and show that for several classes of lambda terms, including binary lambda terms with $m$ free indices, the number of terms of size $n$ is $Theta(n^{-3/2}h{o}^{-n})$ with some class dependent constant $ho$, which in particular disproves the above mentioned conjecture. A way to obtain lower and upper bounds for the constant near the leading term is presented and numerical results for a few previously introduced classes of lambda terms are given.

Full work available at URL: https://arxiv.org/abs/1509.06139

Recommendations

• Enumerating lambda terms by weighted length of their de Bruijn representation
• Counting terms in the binary lambda calculus
• Counting and generating terms in the binary lambda calculus
• A natural counting of lambda terms
• On counting untyped lambda terms

zbMATH Keywords

lambda-calculusanalytic combinatoricsterms enumeration

Mathematics Subject Classification ID

Exact enumeration problems, generating functions (05A15) Combinatory logic and lambda calculus (03B40)

Cited In (8)

• Statistical properties of lambda terms
• On the enumeration of closures and environments with an application to random generation
• Binary lambda calculus and combinatory logic
• Title not available (Why is that?)
• Tuning as convex optimisation: a polynomial tuner for multi-parametric combinatorial samplers
• Enumerating lambda terms by weighted length of their de Bruijn representation
• On the number of unary-binary tree-like structures with restrictions on the unary height
• Normal-order reduction grammars

This page was built for publication: On the number of lambda terms with prescribed size of their de Bruijn representation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4601892)