Related papers: Counting and Generating Terms in the Binary Lambda…
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…
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…
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$…
Lambda calculus is the basis of functional programming and higher order proof assistants. However, little is known about combinatorial properties of lambda terms, in particular, about their asymptotic distribution and random generation.…
We survey several methods of generating large random lambda-terms, focusing on their closed and simply-typed variants. We discuss methods of exact- and approximate-size generation, as well as methods of achieving size-uniform and…
We present several results on counting untyped lambda terms, i.e., on telling how many terms belong to such or such class, according to the size of the terms and/or to the number of free variables.
A natural approach to software quality assurance consists in writing unit tests securing programmer-declared code invariants. Throughout the literature a great body of work has been devoted to tools and techniques automating this…
Randomly generating structured objects is important in testing and optimizing functional programs, whereas generating random $'l$-terms is more specifically needed for testing and optimizing compilers. For that a tool called QuickCheck has…
We investigate the asymptotic number of elements of size $n$ in a particular class of closed lambda-terms (so-called $BCI(p)$-terms) which are related to axiom systems of combinatory logic. By deriving a differential equation for the…
We study the sequences of numbers corresponding to lambda terms of given sizes, where the size is this of lambda terms with de Bruijn indices in a very natural model where all the operators have size 1. For plain lambda terms, the sequence…
Contrary to several other families of lambda terms, no closed formula or generating function is known and none of the sophisticated techniques devised in analytic combinatorics can currently help with counting or generating the set of {\em…
This text gives a rough, but linear summary covering some key definitions, notations, and propositions from Lambda Calculus: Its Syntax and Semantics, the classical monograph by Barendregt. First, we define a theory of untyped extensional…
We consider various classes of Motzkin trees as well as lambda-terms for which we derive asymptotic enumeration results. These classes are defined through various restrictions concerning the unary nodes or abstractions, respectively: We…
Enumerating the number of times one word occurs in another is a much-studied combinatorial subject. By utilizing a method that we call ``lexicographic extreme referencing'', we provide a formula for computing occurrences of one binary word…
We present a quantitative, statistical analysis of random lambda terms in the de Bruijn notation. Following an analytic approach using multivariate generating functions, we investigate the distribution of various combinatorial parameters of…
This paper addresses the uniform random generation of words from a context-free language (over an alphabet of size $k$), while constraining every letter to a targeted frequency of occurrence. Our approach consists in a multidimensional…
The Boltzmann model for the random generation of "decomposable" combinatorial structures is a set of techniques that allows for efficient random sampling algorithms for a large class of families of discrete objects. The usual requirement of…
Tandem duplication is an evolutionary process whereby a segment of DNA is replicated and proximally inserted. The different configurations that can arise from this process give rise to some interesting combinatorial questions. Firstly, we…
A binary string representation of prime occurrences is a sequence of bits, where $1$ entries encode positions of prime numbers. This is a convenient representation for analysis of prime distribution, since it allows for application of a…
In compositional model-theoretic semantics, researchers assemble truth-conditions or other kinds of denotations using the lambda calculus. It was previously observed that the lambda terms and/or the denotations studied tend to follow the…