2017/07/07 by Olivier Bodini, Bodini, Olivier, Bernhard Gittenberger +3
Computer Science · #semigroups and automata theory #Advanced Algebra and Logic #Authorship Attribution and Profiling
paper · pdf · doi:10.48550/arxiv.1707.02101
John Tromp introduced the so-called 'binary lambda calculus' as a way to\nencode lambda terms in terms of 0-1-strings using the de Bruijn representation\nalong with a weighting scheme. Later, Grygiel and Lescanne conjectured that the\nnumber of binary lambda terms with m free indices and of size n (encoded as\nbinary words of length n and according to Tromp's weights) is o(n-3/2\n\τ-n) for \τ \≈ 1.963448\…. We generalize the proposed\nnotion of size and show that for several classes of lambda terms, including\nbinary lambda terms with m free indices, the number of terms of size n is\n\Θn-3/2 \ρ-n with some class dependent constant \ρ, which\nin particular disproves the above mentioned conjecture.\n The methodology used is setting up the generating functions for the classes\nof lambda terms. These are infinitely nested radicals which are investigated\nthen by a singularity analysis.\n We show further how some properties of random lambda terms can be analyzed\nand present a way to sample lambda terms uniformly at random in a very\nefficient way. This allows to generate terms of size more than one million\nwithin a reasonable time, which is significantly better than the samplers\npresented in the literature so far.\n