Enumerating lambda terms by weighted length of their de Bruijn representation

DOI10.1016/J.DAM.2017.12.042MaRDI QIDQ1706116zbMATH OpenOpenAlexFDO

Authors Olivier Bodini, Bernhard Gittenberger, Zbigniew Gołȩbiewski

Publication date 21 March 2018

Published in Discrete Applied Mathematics (Search for Journal in Brave)

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

zbMATH Keywords

generating functionasymptotic enumerationBoltzmann samplinginfinitely nested radicallambda term

Mathematics Subject Classification ID

Asymptotic enumeration (05A16) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Combinatory logic and lambda calculus (03B40)

Abstract: John Tromp introduced the so-called 'binary lambda calculus' as a way to encode lambda terms in terms of 0-1-strings using the de Bruijn representation along with a weighting scheme. 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$ and according to Tromp's weights) 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. The methodology used is setting up the generating functions for the classes of lambda terms. These are infinitely nested radicals which are investigated then by a singularity analysis. We show further how some properties of random lambda terms can be analyzed and present a way to sample lambda terms uniformly at random in a very efficient way. This allows to generate terms of size more than one million within a reasonable time, which is significantly better than the samplers presented in the literature so far.

Recommendations

• On the number of lambda terms with prescribed size of their de Bruijn representation
• Unary profile of lambda terms with restricted De Bruijn indices
• scientific article; zbMATH DE number 1890156
• Ranking/unranking of lambda terms with compressed de Bruijn indices
• Distribution of variables in lambda-terms with restrictions on De Bruijn indices and De Bruijn levels
• Weight class distributions of de Bruijn sequences
• scientific article; zbMATH DE number 2154131
• De Bruijn enumeration applied to some genetical problems
• De Bruijn sequences for fixed-weight binary strings
• On weight of the Pólya-Redfield-de Bruijn counting and twelvefold way

Cites work

• scientific article; zbMATH DE number 2050057 (Why is no real title available?)
• scientific article; zbMATH DE number 6148924 (Why is no real title available?)
• scientific article; zbMATH DE number 3400430 (Why is no real title available?)
• 2-Xor revisited: satisfiability and probabilities of functions
• A natural counting of lambda terms
• Analytic combinatorics
• And/Or Trees Revisited
• And/or tree probabilities of Boolean functions
• Asymptotic properties of combinatory logic
• Asymptotically almost all \lambda-terms are strongly normalizing
• Asymptotics and random sampling for BCI and BCK lambda terms
• Binary lambda calculus and combinatory logic
• Boltzmann Samplers for the Random Generation of Combinatorial Structures
• Coloring rules for finite trees, and probabilities of monadic second order sentences
• Counting and generating lambda terms
• Counting and generating terms in the binary lambda calculus
• Counting finite models
• Counting proofs in propositional logic
• Counting terms in the binary lambda calculus
• Enumeration of generalized BCI lambda-terms
• Generalised and quotient models for random and/or~trees and application to satisfiability
• How big is BCI fragment of BCK logic
• In the full propositional logic, 5/8 of classical tautologies are intuitionistically valid
• On counting untyped lambda terms
• On the density of truth of locally finite logics
• On the number of lambda terms with prescribed size of their de Bruijn representation
• On the number of unary-binary tree-like structures with restrictions on the unary height
• Periodic oscillations in the analysis of algorithms and their cancellations
• Pointed versus singular Boltzmann samplers: a comparative analysis
• Probabilities of Boolean functions given by random implicational formulas
• Singularity Analysis of Generating Functions
• Some typical properties of large AND/OR Boolean formulas
• Tautologies over implication with negative literals
• The Boolean functions computed by random Boolean formulas or how to grow the right function
• The asymptotics of group Russian roulette
• The fraction of large random trees representing a given Boolean function in implicational logic
• The number of Boolean functions computed by formulas of a given size
• The relation between tree size complexity and probability for Boolean functions generated by uniform random trees

Cited in

(16)

• A natural counting of lambda terms
• On the enumeration of closures and environments with an application to random generation
• Statistical properties of lambda terms
• Ranking/unranking of lambda terms with compressed de Bruijn indices
• Counting terms in the binary lambda calculus
• Combinatorics of \(\lambda\)-terms: a natural approach
• On the number of unary-binary tree-like structures with restrictions on the unary height
• On the number of lambda terms with prescribed size of their de Bruijn representation
• Counting and generating terms in the binary lambda calculus
• Distribution of variables in lambda-terms with restrictions on De Bruijn indices and De Bruijn levels
• Counting and generating lambda terms
• Lambda terms of bounded unary height
• Binary lambda calculus and combinatory logic
• Unary profile of lambda terms with restricted De Bruijn indices
• Sampling \(\beta\)-normal linear \(\lambda\)-terms
• scientific article; zbMATH DE number 845591 (Why is no real title available?)

This page was built for publication: Enumerating lambda terms by weighted length of their de Bruijn representation

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