Katarzyna Grygiel
email: grygiel@tcs.uj.edu.pl

Pierre Lescanne
email: pierre.lescanne@ens-lyon.fr

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

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

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.

Introduction

In recent years growing attention has been given to quantitative research in logic and computational models. Investigated objects (e.g., propositional formulae, tautologies, proofs, programs) can be seen as combinatorial structures, 1 providing therefore the inspiration for combinatorists and computer scientists. In particular, several works have been devoted to studying properties of lambda calculus terms. From the practical point of view, generation of random λ-terms is the core of debugging functional programs using random tests [START_REF] Claessen | QuickCheck: a lightweight tool for random testing of Haskell programs[END_REF] and the present paper offers an answer to an open question (see introduction of [START_REF] Claessen | QuickCheck: a lightweight tool for random testing of Haskell programs[END_REF]) since we are able to generate closed typable terms following a uniform distribution. But this work applies beyond λ-calculus to any system with bound variables, like the first order predicate calculus (quantifiers are binders like λ) or block structures in programming languages.

First traces of the combinatorial approach to lambda calculus date back to the work of Jue Wang [START_REF] Wang | The efficient generation of random programs and their applications[END_REF], who initiated the idea of enumerating λ-terms. In her report, Wang defined the size of a term as the total number of abstractions, applications and occurrences of variables, which corresponds to the number of all vertices in the tree representing the given term.

This size model, although natural from the combinatorial viewpoint, turned out to be difficult to handle. The question that arises immediately concerns the number of λ-terms of a given size. This task has been done for particular classes of terms by Bodini, Gardy, and Gittenberger [START_REF] Bodini | Enumeration of generalized BCI lambda-terms[END_REF] and Lescanne [START_REF] Lescanne | On counting untyped lambda terms[END_REF].

The approach applied in the latter paper has been extended in [START_REF] Grygiel | Counting and generating lambda terms[END_REF] by the authors of the current paper to the model in which applications and abstractions are the only ones that contribute to the size of a λ-term. The same model has been studied by David et al. [START_REF] David | Asymptotically almost all λ-terms are strongly normalizing[END_REF], where several properties satisfied by random λ-terms are provided.

When dealing with the two described models, it is not difficult to define recurrence relations for the number of λ-terms of a given size. Furthermore, by applying standard tools of the theory of generating functions one obtains generating functions that are expressed in the form of infinitely nested radicals. Moreover, the radii of convergence are in both cases equal to zero, which makes the analysis of those functions very difficult to cope with.

In this paper, we study the binary encoding of lambda calculus introduced in [START_REF] Tromp | Binary lambda calculus and combinatory logic[END_REF]. This representation results in another size model. It comes from the binary lambda calculus defined by Tromp, in which he builds a minimal selfinterpreter of lambda calculus1 as a basis of algorithmic complexity theory [START_REF] Li | An introduction to Kolmogorov complexity and its applications[END_REF]. Such a binary approach is more realistic from the functional programming viewpoint. Indeed, for compiler builders it is counter-intuitive to assign the same size to all the variables, because in the translation of a program written in Haskell, Ocaml or LISP variables are put in a stack. A variable deep in the stack is not as easily reachable as a variable shallow in the stack. Therefore the weight of the former should be larger than the weight of the latter. Hence it makes sense to associate a size with a variable proportional to its distance to its binder. When we submitted [START_REF] Grygiel | Counting and generating lambda terms[END_REF] to the Journal of Functional Programming, a referee wrote: "If the authors want to use the de Bruijn representation, another interesting experiment could be done: rather than to count variables as size 0, they should be counted using their unary representation. This would penalize deep lexical scoping, which is not a bad idea since 'local' terms are much easier to understand and analyze than deep terms". In this model, recurrence relations for the number of terms of a given size are built using this specific notion of size. From that, we derive corresponding generating functions defined as infinitely nested radicals. However, this time the radius of convergence is positive and enables a further analysis of the functions. We are able to compute the asymptotics of the number of all (not necessarily closed) terms and we also prove an upper bound of the asymptotics of the number of closed ones. Moreover, we define an unranking function, i.e., a generator of terms from their indices from which we derive a uniform generator of random λ-terms (general and typable) of a given size. This allows us to provide outcomes of computer experiments in which we estimate the number of simply typable λ-terms of a given size.

Recall that Boltzmann samplers are programs for efficient generation of random combinatorial objects. Based on generating functions, they are parameterized by the radius of convergence of the generating function. In addition to a more realistic approach of the size of the λ-terms, binary lambda calculus terms are associated with a generating function with a positive radius of convergence, which allows us to build a Boltzmann sampler, hence a very efficient way to generate random λ-terms. In Section 9 and Section 10 we introduce the notion of Boltzmann sampler and we propose a Boltzmann sampler for λ-terms together with a Haskell program.

A version [START_REF] Grygiel | Counting terms in the binary lambda calculus[END_REF] of the first part of this paper was presented at the 25th International Conference on Probabilistic, Combinatorial and Asymptotic Methods for the Analysis of Algorithms.

Lambda calculus and its binary representation

In order to eliminate names of variables from the notation of λ-terms, de Bruijn introduced an alternative way of representing equivalent terms.

Let us assume that we are given a countable set {1, 2, 3, . . .}, elements of which are called de Bruijn indices. We define de Bruijn terms (called terms for brevity) in the following way:

(i) each de Bruijn index i is a term, (ii) if M is a term, then (λM ) is a term (called an abstraction), (iii) if M and N are terms, then (M N ) is a term (called an application).

For the sake of clarity, we will omit the outermost parentheses. Moreover, we sometimes omit other parentheses according to the convention that application associates to the left, and abstraction associates to the right. Therefore, instead of (M N )P we will write M N P , and instead of λ(λM ) we will write λλM .

Given a term λN we say that the λ encloses all indices occurring in the term N . Given a term M , we say that an occurrence of an index i in the term M is free in M if the number of λ's in M enclosing the occurrence of i is less than i. Otherwise, we say the given occurrence of i is bound by the i-th lambda enclosing it. A term M is called closed if there are no free occurrences of indices.

For instance, given a term λλ1(λ1 4), the first occurrence of 1 is bound by the second lambda, the second occurrence of 1 is bound by the third lambda, and the occurrence of 4 is free. Therefore, the given term is not closed.

Following John Tromp, we define the binary representation of de Bruijn indices in the following way:

λM = 00 M , M N = 01 M N , i = 1 i 0.
However, notice that unlike Tromp [START_REF] Tromp | Binary lambda calculus and combinatory logic[END_REF] and Lescanne [START_REF] Lescanne | From λσ to λυ, a journey through calculi of explicit substitutions[END_REF], we start the de Bruijn indices at 1 like de Bruijn [START_REF] Nicolaas | Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem[END_REF]. Given a de Bruijn term, we define its size as the length of the corresponding binary sequence, i.e.,

|n| = n + 1, |λM | = |M | + 2, |M N | = |M | + |N | + 2.
For instance, the de Bruijn term λλ1(λ1 4) is represented by the binary sequence 0000011000011011110 and hence its length is [START_REF] Nijenhuis | Combinatorial algorithms, 2nd edition. Computer science and applied mathematics[END_REF].

In contrast to models studied previously, the number of all (not necessarily closed) λ-terms of a given size is always finite. This is due to the fact that the size of each variable depends on the distance from its binder.

Combinatorial facts

In order to determine the asymptotics of the number of all/closed λ-terms of a given size, we will use the following combinatorial notions and results.

We say that a sequence (F n ) n≥0 is of

• order G n , for some sequence (G n ) n≥0 (with G n = 0), if lim n→∞ F n /G n = 1,
and we denote this fact by F n ∼ G n ;

• exponential order A n , for some constant A, if lim sup

n→∞ |F n | 1/n = A,
and we denote this fact by F n A n .

Given the generating function F (z) for a sequence (F n ) n≥0 , we write [z n ]F (z) to denote the n-th coefficient of the Taylor expansion of F (z), therefore [z n ]F (z) = F n .

The theorems below (Theorem IV.7 and Theorem VI.1 of [START_REF] Flajolet | Analytic Combinatorics[END_REF]) serve as powerful tools that allow us to estimate coefficients of certain functions that frequently appear in combinatorial considerations.

Fact 1 If F (z) is analytic at 0 and R is the modulus of a singularity nearest to the origin, then

[z n ]F (z) (1/R) n .
Fact 2 Let α be an arbitrary complex number in

C \ Z ≤0 . The coefficient of z n in f (z) = (1 -z) α
admits the following asymptotic expansion:

[z n ]f (z) ∼ n α-1 Γ(α) 1 + α(α -1) 2n + α(α -1)(α -2)(3α -1) 24n 2 + O 1 n 3 ,
where Γ is the Euler Gamma function.

The sequences S m,n

Let us denote the number of λ-terms of size n with at most m distinct free indices by S m,n . First, let us notice that there are no terms of size 0 and 1. Let us consider a λ-term of size n + 2 with at most m distinct free indices. Then we have one of the following cases.

• The term is a de Bruijn index n + 1, provided m is greater than or equal to n + 1.

• The term is an abstraction whose binary representation is given by 00 M , where the size of M is n and M has at most m + 1 distinct free variables.

• The term is an application whose binary representation is given by 01 M N , where M is of size i and N is of size n -i, with i ∈ {0, . . . , n}, and each of the two terms has at most m distinct free variables.

This leads to the following recursive formula2 :

S m,0 = S m,1 = 0, (1)
S m,n+2 = [m ≥ n + 1] + S m+1,n + n k=0 S m,k S m,n-k . (2)
The sequence (S 0,n ) n≥0 , i.e., the sequence of numbers of closed λ-terms of size n, can be found in the On-line Encyclopedia of Integer Sequences under the number A114852. Its first 20 values are as follows: 0, 0, 0, 0, 1, 0, 1, 1, 2, 1, 6, 5, 13, 14, 37, 44, 101, 134, 298, 431.

More values are given in Figure 5. The values of S m,n can be computed by the function we call tromp given in Figure 1.

--Iverson symbol

iv b = if b then 1 else 0 --Tromp size a114852Tab :: [[ Integer]] a114852Tab = [0,0..] : [0,0..] : [[ iv (n -2 < m) + a114852Tab !! (n-2) !! (m+1) + s n m | m <-[0..]] | n <-[2..]]
where Most of all, we are interested in the generating function for the number of closed terms, i.e.,

s n m = let ti = [a114852Tab !! i !! m | i <-[0..(n-2)]] in sum (zipWith ( * ) ti (reverse ti)) tromp m n = a114852Tab !! n !! m
S 0 (z) = ∞ n=0 S 0,n z n .
Applying the recurrence on S m,n , we get

S m (z) = z 2 ∞ n=0 S m,n+2 z n = z 2 ∞ n=0 [m ≥ n + 1]z n + z 2 ∞ n=0 S m+1,n z n + z 2 ∞ n=0 n k=0 S m,k S m,n-k z n = z 2 m-1 k=0 z k + z 2 S m+1 (z) + z 2 S m (z) 2 = z 2 (1 -z m ) 1 -z + z 2 S m+1 (z) + z 2 S m (z) 2 .
Solving the equation

z 2 S m (z) 2 -S m (z) + z 2 (1 -z m ) 1 -z + z 2 S m+1 (z) = 0 (3)
gives us

S m (z) = 1 -1 -4z 4 1-z m 1-z + S m+1 (z) 2z 2 . ( 4
)
This means that the generating function S m (z) is expressed by means of infinitely many nested radicals, a phenomenon which has already been encountered in previous research papers on enumeration of λ-terms, see e.g., [START_REF] Bodini | Lambda-terms of bounded unary height[END_REF]. However, in Tromp's binary lambda calculus we are able to provide more results than in other representations of λ-terms.

First of all, let us notice that the number of λ-terms of size n has to be less than 2 n , the number of all binary sequences of size n. This means that in the considered model of λ-terms the radius of convergence of the generating function enumerating closed λ-terms is positive (it is at least 1/2), which is not the case in other models, where the radius of convergence is equal to zero.

The number of all λ-terms

Let us now consider the sequence enumerating all binary λ-terms, i.e., including terms that are not closed. Let S ∞,n denote the number of all such terms of size n. Repeating the reasoning from the previous section, we obtain the following recurrence relation:

S ∞,0 = S ∞,1 = 0, S ∞,n+2 = 1 + S ∞,n + n k=0 S ∞,k S ∞,n-k .
The sequence (S ∞,n ) n∈N can be found in On-line Encyclopedia of Integer Sequences with the entry number A114851. Its first 20 values are as follows: 0, 0, 1, 1, 2, 2, 4, 5, 10, 14, 27, 41, 78, 126, 237, 399, 745, 1292, 2404, 4259.

More values are given in Figure 5.

Obviously, we have S m,n ≤ S ∞,n for every m, n ∈ N. Moreover, lim

m→∞ S m,n = S ∞,n .
Let S ∞ (z) denote the generating function for the sequence (S ∞,n ) n∈N , that is

S ∞ (z) = ∞ n=0 S ∞,n z n . Notice that for m ≥ n -1 we have S m,n = S ∞,n . Therefore, S ∞ (z) = ∞ n=1 S n,n z n , which yields that [z n ]S n,n = [z n ]S ∞,n . Furthermore, S ∞ (z) = lim m→∞ S m (z) for all z ∈ (0, ρ), where ρ is the dominant singularity of S ∞ (z).
Theorem 1 The number of all binary λ-terms of size n satisfies

S ∞,n ∼ ρ -n • C n 3/2 ,
where ρ . = 0.509308127 and C . = 1.021874073.

Proof:

The generating function S ∞ (z) fulfills the equation

S ∞ (z) = z 2 1 -z + z 2 S ∞ (z) + z 2 S ∞ (z) 2 .
Solving the above equation gives us

S ∞ (z) = (1 -z)(1 -z 2 ) -(1 -z)(1 -z -2 z 2 + 2 z 3 -3 z 4 -z 5 ) 2z 2 (1 -z) .
The dominant singularity of the function S ∞ (z) is given by the root of smallest modulus of the polynomial

R ∞ (z) = 1 -z -2 z 2 + 2 z 3 -3 z 4 -z 5 .
The polynomial has three real roots: 0.509308127 . . . , -0.623845142 . . . , -3.668100004 . . . , and two complex ones that are approximately equal to 0.4 + 0.8i and 0.4 -0.8i. Therefore, ρ . = 0.509308127 is the singularity of S ∞ nearest to the origin. Let us write S ∞ (z) in the following form:

S ∞ (z) = 1 -z 2 -ρ(1 -z ρ ) • Q(z) 2z 2 ,
where Q(z) is a rational function defined for all |z| ≤ ρ.

We get that the radius of convergence of S ∞ (z) is equal to ρ and its inverse

1 ρ . = 1.963447954 gives the growth of S ∞,n . Hence, S ∞,n (1/ρ) n .
Fact 2 allows us to determine the subexponential factor of the asymptotic estimation of the number of terms. Applying it, we obtain

[z n ]S ∞ (z) = ρ -n [z n ]S ∞ (ρz) ∼ ρ -n [z n ] - √ 1 -z • ρQ(ρz) 2ρ 2 z 2 ∼ ρ -n • n -3/2 Γ(-1 2 ) • C,
where the constant C is given by

C = -ρ • Q(ρ) 2ρ 2 . = -0.288265354. Since C Γ(- 1 2 )
. = 1.021874073, the theorem is proved.

The number of closed λ-terms

Proposition 1 Let ρ m denote the dominant singularity of S m (z). Then for every natural number m we have

ρ m = ρ 0 ,
which means that all functions S m (z) have the same dominant singularity.

Proof: First, let us notice that for every m, n ∈ N we have S m,n ≤ S m+1,n . This means that the radius of convergence of the generating function for the sequence (S m,n ) n∈N is not smaller than the radius of convergence of the generating function for (S m+1,n ) n∈N . Therefore, for every natural number m, we have

ρ m ≥ ρ m+1 .
Additionally, from Equation (4) we see that every singularity of S m+1 (z) is also a singularity of S m (z). Hence, the dominant singularity of S m (z) is less than or equal to the dominant singularity of S m+1 (z), i.e., we have

ρ m ≤ ρ m+1 .
These two inequalities show that dominant singularities of all functions S m (z) are the same. In particular, for every m we have ρ m = ρ 0 .

Proposition 2

The dominant singularity of S 0 (z) is equal to the dominant singularity of S ∞ (z), i.e., ρ 0 = ρ . = 0.509308127.

Proof: Since the number of closed binary λ-terms is not greater than the number of all binary terms of the same size, we conclude immediately that ρ 0 ≥ ρ.

Let us now consider the functionals Φ ∞ and Φ m for every m ∈ N. By Equation ( 4), for every m the functional Φ m applied to S m+1 gives us S m , while Φ ∞ is the limit of the sequence (Φ m ) m∈N :

Φ m (F ) = 1 -1 -4z 4 ( 1-z m 1-z + F ) 2z 2 , Φ ∞ (F ) = 1 -1 -4z 4 ( 1 1-z + F ) 2z 2 .
In particular, when m = 0, we have

Φ 0 (F ) = 1 - √ 1 -4z 4 F 2z 2 .
By Equation ( 4) and the definition of Φ m , we have

S m (z) = Φ m (S m+1 (z)).
The Φ m 's and Φ ∞ are monotonic over functions over (0, 1), which means that for every z ∈ (0, 1) we have

F (z) ≤ G(z) ⇒ Φ m (F (z)) ≤ Φ m (G(z)), F (z) ≤ G(z) ⇒ Φ ∞ (F (z)) ≤ Φ ∞ (G(z)).
For each m ∈ N, let us consider the function S m (z) defined as the fixed point of Φ m . In other words, S m (z) is defined as the solution of the following equation:

S m (z) = Φ m ( S m (z)).
Notice that S m,n ≤ S m+1,n ≤ S ∞,n , for the reasons that given a size n, there are less trees with at most m free variables than trees with at most m + 1 free variables and less trees with at most m + 1 free variables than trees with any numbers of free variables. For z ∈ (0, ρ) we can claim that S m (z) ≤ S m+1 (z) ≤ S ∞ (z). Applying Φ m to the first inequality, we obtain, for z ∈ (0, ρ),

Φ m (S m (z)) ≤ S m (z) Then we get Φ k+1 m (S m (z)) ≤ Φ k m (S m (z)) ≤ ... ≤ Φ m (S m (z)) ≤ S m (z)
and since

S m (z) = lim k→∞ Φ k m (S m (z)) = inf k∈N Φ k m (S m (z))
we infer

S m (z) ≤ S m (z) ≤ S ∞ (z).
Since S m (z) satisfies

2z 2 S m (z) = 1 -1 -4z 4 1 -z m 1 -z + S m (z) ,
we get

z 2 S 2 m (z) -(1 -z 2 ) S m (z) + z 2 (1 -z m ) 1 -z = 0.
The discriminant of this equation is:

∆ m = (1 -z 2 ) 2 - 4z 4 (1 -z m ) 1 -z .
The values for which ∆ m = 0 are the singularities of S m (z). Let us denote the main singularity of S m (z) by σ m . From Equation [START_REF] David | Asymptotically almost all λ-terms are strongly normalizing[END_REF] we see that

σ m ≥ ρ m ≥ ρ.
The value of σ m is equal to the root of smallest modulus of the following polynomial:

P m (z) := (z -1)∆ m = 4z 4 (1 -z m ) -(1 -z) 3 (1 + z) 2 .
In the case of the function S ∞ (z), we get the polynomial

P ∞ (z) = -1 + z + 2 z 2 -2 z 3 + 3 z 4 + z 5 = -R ∞ (z),
whose root of smallest modulus is the same as for R ∞ (z), hence it is equal to ρ. Now, let us show that the sequence (σ m ) m∈N of roots of smallest modulus of polynomials P m (z) is decreasing and that it converges to ρ. As a hint, Figure 2 The number of closed terms of a given size cannot be greater than the number of all terms. Therefore, we immediately obtain what follows. Figure 3 shows values S m,n • ρ n • n 3/2 for a few initial values of m and n up to 600 and allows us to state the following conjecture.

Conjecture 1 For every natural number m, we have

S m,n ∼ o 1.963448 . . . n • n -3/2 .

Unrankings

The recurrence relation [START_REF] Bodini | Lambda-terms of bounded unary height[END_REF] for S m,n allows us to define the function generating λ-terms. More precisely, we construct bijections s m,n , called unranking functions, between all non-negative integers not greater than S m,n and binary λ-terms of size n with at most m distinct free variables [START_REF] Karttunen | Ranking and unranking functions[END_REF]. This approach is also known as the recursive method, originating with Nijenhuis and Wilf [START_REF] Nijenhuis | Combinatorial algorithms, 2nd edition. Computer science and applied mathematics[END_REF] (see especially Chapter 13).

Let us recall that for n ≥ 2 we have, by [START_REF] Bodini | Lambda-terms of bounded unary height[END_REF],

S m,n = [m ≥ n -1] + S m+1,n-2 + n-2 j=0
S m,j S m,n-2-j . • If m ≥ n -1 and k is equal to S m,n , the function returns the string 1 n-1 0.

• If k is less than or equal to S m+1,n-2 , then the corresponding term is in the form of abstraction 00 M , where M is the value of the unranking function s m+1,n-2 on k.

• Otherwise, i.e., if k is greater than S m+1,n-2 and less than S m,n for m ≥ n + 1 or less than or equal to S m,n for m < n + 1, the corresponding term is in the form of application 01 M N . In order to get strings M and N , we compute the maximal value ∈ {0, . . . , n -2} for which

k -S m+1,n-2 = -1 j=0 S m,j S m,n-2-j + r with r ≤ S m, S m,n-2-.
The In Figure 4 the reader may find a Haskell definition of the data type Term and a program [START_REF]Haskell 98 language and libraries: the Revised Report[END_REF] for computing the values s m,n (k). In this program, the function s m,n (k) is written as unrankT m n k and the sequence S m,n is written as tromp m n.

data Term = Index Int | Abs Term | App Term Term unrankT :: Int -> Int -> Integer -> Term unrankT m n k | m >= n -1 && k == (tromp m n) = Index (n -1) | k <= (tromp (m+1) (n-2)) = Abs (unrankT (m+1) (n-2) k) | otherwise = unrankApp (n-2) 0 (k -tromp (m+1) (n-2))
where unrankApp n j r

| r <= tmjtmnj = let (dv,rm) = (r-1) 'divMod' tmnj in App (unrankT m j (dv+1)) (unrankT m (n-j) (rm+1)) | otherwise = unrankApp n (j + 1) (r -tmjtmnj)
where tmnj = tromp m (n-j) tmjtmnj = (tromp m j) * tmnj

Number of typable terms

The unranking function allows us to traverse all the closed terms of size n and to filter those that are typable (see [START_REF] Hindley | Basic Simple Type Theory[END_REF]) in order to count them and similarly to traverse all the terms of size n to count those that are typable.

The comparison of the numbers of λ-terms and the numbers of typable λterms is presented in Figure 5. From left to right:

1. the numbers S 0,n of closed terms (typable and untypable) of size n, 2. the numbers T 0,n of closed typable terms of size n, 3. the numbers S ∞,n of all terms (typable and untypable) of size n, 4. the numbers T ∞,n of all typable terms of size n.

In particular, let us notice that S 0,n and T 0,n are the same up to n = 8, where we meet the smallest untypable closed term namely λ1 1. Similarly, S ∞,n and T ∞,n are the same up to n = 6, where we meet the smallest untypable term, namely [START_REF] Bacher | Efficient random sampling of binary and unary-binary trees via holonomic equations[END_REF] require too many computations, between 14 millions and 96 millions of λ-terms have to be checked for typability in each case. Paul Tarau [START_REF] Tarau | On type-directed generation of lambda terms[END_REF] gives a Prolog implementation and applies it to the generation of typed λ-terms.

Thanks to the unranking function, we can build a uniform generator of λterms and, using this generator, we can build a uniform generator of simply typable λ-terms, which sieves the uniformly generated terms through a program that checks their typability (see for instance [START_REF] Grygiel | Counting and generating lambda terms[END_REF]). This way, it is possible to generate typable closed terms uniformly up to size 4503 .

Boltzmann samplers

In this section we present the basic ideas related to Boltzmann models, which combined with the theory of generating functions allow us to develop efficient algorithms for generating random λ-terms. A thorough and clear overview of Boltzmann samplers, including many examples, can be found in [START_REF] Duchon | Boltzmann samplers for the random generation of combinatorial structures[END_REF]. For readers not acquainted with the theory, we provide necessary notions and constructions.

Let C be a combinatorial class, i.e., a set of combinatorial objects endowed with a size function |•|: C → N such that there are finitely many elements of size n for every n ∈ N. Let C n denote the cardinality of the subset of C consisting of elements of size n. Furthermore, let C(z) denote the generating functions associated with the sequence (C n ) n∈N , which means that

C(z) = ∞ n=0 C n z n . Notice that C(z) = γ∈C z |γ| .
Given a positive real x ∈ R + , we define a Boltzmann model for the class C as the probability distribution that assigns to every element γ ∈ C a probability

P C ,x (γ) = 1 C(x) • x |γ| .
This is a probability since

γ∈C P C ,x (γ) = γ∈C 1 C(x) • x |γ| = 1.
The role of x will become clear later on, but for now we may consider x as a parameter used to "tune" the sampler, that is to center the mean value around a chosen number. In other words, if we want to set an expected mean value, we have to compute the proper value of x. In order the probability P C ,x (γ) to be well-defined, we assume the values of x to be taken from the interval (0, ρ C ), where ρ C denotes the radius of convergence of C(z). Provided C(z) converges at ρ C , we may also consider the case x = ρ C . The size of an object in a Boltzmann model is a random variable N . The Boltzmann sampler for a class C and a parameter x is a random object generator, which draws from the class C an object of size n with probability

P x (N = n) = C n x n C(x) .
This is indeed a well-defined probability since

n≥0 P x (N = n) = 1 C(x) n≥0 C n x n = 1.
When generating random objects, we require either the size to be a fixed value n or, in order to increase the efficiency of the generation process, we admit some flexibility on the size. In other words, we want the objects to be generated in some cloud around a given size n so that the size N of the objects lies in some interval (1 -ε)n ≤ N ≤ (1 + ε)n for some factor ε > 0 called a tolerance. Such a method is called approximate-size uniform random generation. What we want to preserve is the uniformity of the distribution among objects of the same size, i.e., we want all objects of the same size to be drawn with the same probability.

The random variable N has a first moment and a second moment [START_REF] Duchon | Boltzmann samplers for the random generation of combinatorial structures[END_REF]:

E x (N ) = x C (x) C(x) E x (N 2 ) = x 2 C (x) + xC (x) C(x) ,
and a standard deviation:

σ x (N ) = E x (N 2 ) -E x (N ) 2 = x 2 C (x) + xC (x) C(x) -x 2 C (x) 2 C(x) 2 .
In the case of approximate-size generation, in order to maximize chances of drawing an object of a desired size, say n, we need to choose a proper value of the parameter x. It turns out that the best value of x is such for which E x (N ) = n (for a detailed study see [START_REF] Flajolet | Boltzmann sampling of unlabeled structures[END_REF]). Given size n, we will denote by x n the value of the parameter chosen in such a way. Moreover, if n tends to infinity, then x n tends to ρ C (see Appendix).

Design of Boltzmann generator

A Boltzmann generator for a class C is built according to a recursive specification of the class C . Since we are interested in designing a Boltzmann sampler for binary λ-terms, we present the way of defining samplers for classes which are specified by means of the following recursive constructions: disjoint unions where StdGen is the type of standard random generators. For the following we assume a function rand :: Gen Double that generates a random double precision real in the interval (0, 1) together with an update of the random generator. In our case it is defined in Figure 6.

P C ,x (γ ∈ A ) = A(x) C(x) , P C ,x (γ ∈ B) = B(x) C(

x) .

A generator for the disjoint union, i.e., a Bernoulli variable, may have the following type:

genEither :: Double -> (Gen a) -> (Gen b) -> (Either a b -> c) -> Gen c
and then it is given by the Haskell function:

genEither p ga gb caORb = do x <-rand if x < p then do ga' <-ga return (caORb $ Left ga') else do gb' <-gb return (caORb $ Right gb')
Notice the type of genEither which assumes that genEither takes a number, two monad values Gen a and Gen b (which can be seen as pairs of a random generator and a value of type a and b respectively), and a continuation c of type Either a b and returns a value of the monad Gen c. Similar frames will appear in the programs describing other generators.

Cartesian product

Given classes A and B, let C be the class defined as their Cartesian product, i.e., C = A × B. Let a and b be Haskell types corresponding to classes A and B. Then the type of the class C is (a, b). The size of an object γ = α, β ∈ C equals the sum of sizes |α| + |β|. In more concrete terms, if an object is the pair of an object of size p and an object of size q, then its size is p + q. Hence, the generating functions satisfy the equation

C(z) = A(z) • B(z), since C(z) = α,β ∈A ×B z |α|+|β| .
The probability of drawing γ = α, β ∈ C is equal to

P C ,x (γ) = x |γ| C(x) = x |α+β| A(x) • B(x) = x |α| A(x) • x |β| B(x) .
In this case the Boltzmann sampler is as follows:

1 genPair :: (Gen a) -> (Gen b) -> (a -> b -> c) -> (Gen c)
S ∞ (z) = z 2 1 -z + z 2 S ∞ (z) + z 2 S ∞ (z) 2 .
It is derived from the description of the set S ∞ of λ-terms as:

S ∞ = D + λS ∞ + S ∞ S ∞ .
That means that the set of λ-terms S ∞ has three components: the first component D corresponds to de Bruijn indices, the second component λS ∞ corresponds to abstractions, the third component S ∞ S ∞ corresponds to applications. We build a sampler of random terms based on this trichotomy. In Haskell this corresponds to a data type Term defined in Figure 4. Since there are three components in the union, the value p which we considered in genEither will be replaced by two values p1 and p2. First we describe in Haskell a function corresponding to S ∞ (z):

sInfinity z = num z / den z where num z = zˆ3 -zˆ2 -z + 1 -sqrt(sq z) den z = 2 * z * z * (1 -z) sq z = zˆ6 + 2 * (zˆ5) -5 * (zˆ4) + 4 * (zˆ3) -zˆ2 -2 * z + 1
and two functions:

p1 x = x * x / (1-x) / sInfinity x p2 x = p1 x + xˆ2
Using Sage we computed the values:

x 100 = 0.5092252666102192 x 600 = 0.5093058457062517 x 1000 = 0.5093073063214039 which correspond to the values of the parameter x appropriate for an expected value E xi (N ) equal to i = 100, i = 600, and i = 1000, respectively. In other words if the values x 100 , x 600 and x 1000 are passed to the sampler, it will generate objects with average size 100, 600, and 1000, respectively. They are obtained by solving in x the equations

E x (N ) = 100, E x (N ) = 600, E x (N ) = 1000, in which C(x) is replaced by S ∞ (x).

General samplers of λ-terms

The values of the probabilities for a given x are

• p v (x) = x 2
(1-x)S∞(x) for variables,

• p abs (x) = x 2 for abstractions,

• p app (x) = x 2 S ∞ (x) for applications.

We get the following Haskell function which selects among Index, Abs and App As discussed in the previous section, in order to generate random large λ-terms, i.e., λ-terms with average size ∞, we set the value of x to ρ = 0.5093081270242373 . . ., which we call rho in Haskell. Its square is ρ 2 = 0.25939476825293667 . . . . Notice that since ρ is a root of the polynomial below the square root, S ∞ (ρ) = 1-ρ 2 2ρ 2 . The values of the probabilities for selecting among variables, abstractions and applications are:

• p v (ρ) = 2ρ 4
(1-ρ)(1-ρ 2 ) for variables,

• p abs (ρ) = ρ 2 for abstractions,

• p app (ρ) = 1-ρ 2 2
for applications.

Let us simplify

2ρ 4 (1-ρ)(1-ρ 2 ) into 1-ρ 2 2
by computing the difference:

2ρ 4 (1 -ρ)(1 -ρ 2 ) - 1 -ρ 2 2 = 4ρ 4 -(1 -ρ 2 ) 2 (1 -ρ) 2(1 -ρ)(1 -ρ 2 ) = ρ 5 + 3ρ 4 -2ρ 3 + 2ρ 2 + ρ -1 2(1 -ρ)(1 -ρ 2 ) = 0.
Therefore to generate random terms of mean size going to infinity we get the results

• p v (ρ) = 1-ρ 2 2
≈ 0.3703026 for variables,

• p abs (ρ) = ρ 2 ≈ 0.25939476 for abstractions,

• p app (ρ) = 1-ρ 2 2 ≈ 0.3703026 for applications.

We build the function genTerm which generates random terms and the function genInt which generates integers necessary for the de Bruijn indices (see Figure 7). The list is the list of term sizes generated by genTerm when the seeds of the random generator are 0, 1, 2, . . . up to 30. In the same list of term sizes the 50 th element is 127 358 and the 51 st element is 4 379 394, showing that generating a random term of size more than four million is easy.

Assume now that we want to generate terms that are below a certain uplimit, as required by practical applications. The function called ceiledGenTerm is almost the same as genTerm, except that when the up limit is passed it returns Nothing. Therefore the type of ceiledGenTerm differs from genTerm type in the sense that it takes a Gen (Maybe Term) (instead of a Gen Term) and returns a Gen (Maybe Term) (instead of a Gen Term). A Boltzmann sampler ceiledGenTerm for large λ-terms of size limited by uplimit is given in Figure 8.

Suppose now that we want to generate terms within a size interval, i.e., with an up limit and a down limit. By definition, ceiledGenTerm generates terms within an up limit. For terms within the down limit, terms generated by ceiledGenTerm are filtered so that only terms large enough are kept. Recall that the method is linear in time complexity. Thus the generation of a term of size 100 000 takes a few seconds, the generation of a term of size one million takes three minutes and the generation of a term of size five million takes five minutes.

To generate large typable λ-terms we generate λ-terms and check their typability. Currently we are able to generate random typable λ-terms of size 500. This outperforms methods based on ranking and unranking like the method proposed in [START_REF] Grygiel | Counting and generating lambda terms[END_REF]. This is in particular due to the fact that such methods need to handle numbers of arbitrary precision and their random generation, which it not efficient. Indeed ranking or unranking requires handling integers with hundred digits or more and performing computations on them for their random generations. On the other hand, Boltzmann samplers ignore numbers, go directly toward the terms to be generated and do that efficiently.

Related works

We look at related works from two perspectives: works on counting λ-terms and works specifically related to Boltzmann samplers.

Works on counting λ-terms

Connected to this work, let us mention papers on counting λ-terms [START_REF] Lescanne | On counting untyped lambda terms[END_REF][START_REF] Grygiel | Counting and generating lambda terms[END_REF] and on evaluating their combinatorial properties, namely [START_REF] Bodini | Lambda-terms of bounded unary height[END_REF][START_REF] David | Asymptotically almost all λ-terms are strongly normalizing[END_REF][START_REF] Bodini | Enumeration of generalized BCI lambda-terms[END_REF][START_REF] Bodini | Asymptotics and random sampling for BCI and BCK lambda terms[END_REF]. A comparison of our results with those of [START_REF] Grygiel | Counting and generating lambda terms[END_REF] can be made, since [START_REF] Grygiel | Counting and generating lambda terms[END_REF] gives a precise counting of λ-terms when variables (de Bruijn indices) have size 0, yielding sequence A220894 in the On-line Encyclopedia of Integer Sequences for the number of closed terms of size n. The first fifteen terms are: 0, 1, 3, 14, 82, 579, 4741, 43977, 454283, 5159441, 63782411, 851368766, 12188927818, 186132043831, 3017325884473.

If one compares them with the first fifteen terms of S 0,n : 0, 0, 0, 0, 1, 0, 1, 1, 2, 1, 6, 5, 13, 14, 37, one sees that S 0,n grows much more slowly than A220894, which is not surprising since S 0,n grows exponentially, whereas A220894 grows super-exponentially (the radius of convergence of its generating function is 0). This super-exponential growth and the related 0 radius of convergence prevent from building a Boltzmann sampler. Moreover, it does not make sense to count all (including open) terms of size n when variables have size 0 for the reason that there are infinitely many such terms for each n. Notice that taking the size of variables to be 1, like [START_REF] Lescanne | On counting untyped lambda terms[END_REF][START_REF] Bodini | Lambda-terms of bounded unary height[END_REF], does not make much difference for growth and generation.

Works related to Boltzmann samplers for terms

In the introduction we cited papers that are clearly connected to this work. In a recent work, Bacher et al. [START_REF] Bacher | Efficient random sampling of binary and unary-binary trees via holonomic equations[END_REF] propose an improved random generation of binary trees and Motzkin trees, based on Rémy algorithm [START_REF] Rémy | Un procédé itératif de dénombrement d'arbres binaires et son application à leur génération aléatoire[END_REF] (or algorithm R in Knuth [START_REF] Knuth | The Art of Computer Programming, Volume 4, Fascicle 4: Generating All Trees, History of Combinatorial Generation[END_REF]). They propose like Rémy to grow the trees from inside by an operation called grafting. It is not clear how this can be generalized to λ-terms as one needs "to find a combinatorial interpretation for the holonomic equations [which] is not [...] always possible, and even for simple combinatorial objects this is not elementary" (Conclusion of [START_REF] Bacher | Efficient random sampling of binary and unary-binary trees via holonomic equations[END_REF] page 16).

Conclusion

We have shown that if the size of a lambda term is yielded by its binary representation [START_REF] Tromp | Binary lambda calculus and combinatory logic[END_REF], we get an exponential growth of the sequence enumerating λ-terms of a given size. This applies to closed λ-terms, to λ-terms with a bounded number of free variables, and to all λ-terms of size n. Except for the case of all λ-terms, the question of finding the non-exponential factor of the asymptotic approximation of the numbers of those terms is still open. Moreover, we have described unranking functions (recursive methods) for generating λ-terms, which allow us to derive tools for their uniform generation and for enumeration of typable λ-terms. The process of generating random (typable) terms is limited by the performance of the generators based on the recursive methods aka unranking since huge numbers are involved. It turns out that implementing Boltzmann samplers, central tools for the uniform generation of random structures such as trees or λ-terms, gives significantly better results. There are now two directions for further development: the first one consists in integrating the programs proposed here in actual testers and optimizers [START_REF] Claessen | QuickCheck: a lightweight tool for random testing of Haskell programs[END_REF] and the second one in extending Boltzmann samplers to other kinds of programs, for instance programs with block structures. From the theoretical point of view, more should be known about generating functions for closed λ-terms or λ-terms with fixed bounds on the number of free variables. Boltzmann samplers should be designed for such terms, which requires extending the theory. As concerns combinatorial properties of simply typable λ-terms, many question are left open and seem to be hard. Besides, since we are interested in generating typable terms, it is worth designing random uniform samplers that deliver typable terms directly.

The case x = ρ C : generating objects with mean size ∞

In this section we show that choosing a value x = ρ C for the parameter of a sampler yields mean size ∞ of the generated objects. Assume that a generating function we consider is of the form:

C(x) = P C (x) -Q C (x) R C (x) ,
where P C (x), Q C (x) and R C (x) are three polynomials and where ρ C is such that Q C (ρ C ) = 0 and where Q C (x) > 0 and R C (x) = 0 for 0 < x < ρ C . Those properties are fulfilled by the generating function S ∞ (x). Indeed,

P S∞ (z) = (1 -z)(1 -z 2 ), Q S∞ (z) = (1 -z)(1 -z -2 z 2 + 2 z 3 -3 z 4 -z 5 ), R S∞ = 2z 2 (1 -z).
Notice that Q C (ρ C ) < 0 in the vicinity of ρ C , i.e., in an interval (ρ C -ε, ρ C ) (because Q C (ρ C ) = 0 and Q C (x) > 0 for x ∈ (0, ρ C ]) and

C(ρ C ) = P C (ρ C ) R C (ρ C )
is finite. On the other hand,

C (x) = P C (x) R C (x) - Q C (x) 2 Q C (x)R C (x) - (P C (x) -Q C (x))R C (x) R C (x) 2
shows that lim

x→ρ C C (x) = ∞.
Hence lim

x→ρ C E x (N ) = lim x→ρ C xC (x) C(x) = ∞.
Therefore, if we choose x to be ρ C , the size of the generated structures will be distributed all over the natural numbers, with an infinite average size.

Figure 1 :

 1 Figure 1: The function tromp computing the S m,n Now let us define the family of generating functions for sequences (S m,n ) n≥0 :

  illustrates plots of polynomials P m 's (for several values of m) in the interval [0.3, 1]. It shows the roots of the P m 's at the intersection of the curves and of the horizontal axis, between ρ (for P ∞ ) and 1 (for P 0 ). Notice that P m (z) = P ∞ (z) -4z m+4 . Given a value ζ such that ρ < ζ < 1 (for instance ζ = 0.8), P m (z) converges uniformly to P ∞ (z) in the interval [0, ζ]. Therefore σ m → ρ when m → ∞. By σ m ≥ ρ m ≥ ρ, we get ρ m → ρ, as well. Since all the ρ m 's are equal, we obtain that ρ m = ρ for every natural m.

Figure 2 :Theorem 2

 22 Figure2: Plots of the P m 's. The top curve is P ∞ , below there is P 100 , then P 10 , P 9 etc. until P 1 and P 0 .

Figure 3 :

 3 Figure 3: S m,n ρ n n 3/2 up to n = 600 for m = 0 (bottom) to 10 (top)

  strings M and N are the values s m, (k ) and s m,n-2-(k ), respectively, where k is the integer quotient upon dividing r by S m,n-2-, and k is the remainder. Notice that in this definition, extremal values of k are considered first. Namely, first the maximal value S m,n (for m ≥ n -1) is considered, then values from the set {1, . . . , S m+1,n-2 } are taken into account, and finally, in the third case, the remaining values.

Figure 4 :

 4 Figure 4: The data type Term and a program for computing values of the function s m,n

Figure 5 :

 5 Figure 5: Numbers of terms and numbers of typable terms

(

  data type Either a b), products (data type Pair) and sequences (data type List). First we assume a monad Gen defined from the monad State of the Haskell library by type Gen = State StdGen

  rand :: Gen Double rand = do generator <-get let (value , newGenerator) = randomR (0,1) generator put newGenerator return value

Figure 6 :

 6 Figure 6: The function rand

2 genPair ga gb caANDb = do 3 ga' <-ga 4 gb' <-gb 5 return

 2345 (caANDb ga' gb') 10 Boltzmann samplers for λ-terms Let us consider the equation involving the generating function for all λ-terms:

  genTermGeneric :: Double -> Gen Int -> Gen Term genTermGeneric x gi = do p <-rand if p < p1 x then do i <-genIntGeneric x return (Index i) else if p < p2 x then do t <-genTermGeneric x gi return (Abs t) else genPair (genTermGeneric x gi) (genTermGeneric x gi) App Notice the call to the function genIntGeneric :: Double -> Gen Int genIntGeneric x = do p <-rand if p < x then do n <-genIntGeneric x return (n+1) else return 1 which is used to generate random de Bruijn indices.

10. 2

 2 Samplers for large λ-terms rho :: Double rho = 0.509308127024237357194177485 rhosquare = rho * rho p1rho = (1 -rhosquare) / 2 p2rho = p1rho + rhosquare genTerm :: Gen Int -> Gen Term genTerm gi = do p <-rand if p < p1rho then do i <-genInt return (Index i) else if p < p2rho then do t <-genTerm gi return (Abs t) else genPair (genTerm gi) (genTerm gi) App genInt :: Gen Int genInt = do p <-rand if p < rho then do n <-genInt return (n+1) else return 1

Figure 7 :

 7 Figure 7: The function genTerm

  ceiledGenTerm :: Int -> Gen Int -> Gen (Maybe Term) ceiledGenTerm uplimit gi = do p <-rand if p < p1rho then do --generate an index i <-genInt return $ if i < uplimit then Just (Index i) else Nothing else if p < p2rho then do --generate an abstraction mbt <-ceiledGenTerm uplimit gi return $ case mbt of Just t -> if 2 + size t <= uplimit then Just (Abs t) else Nothing Nothing -> Nothing else do --generate an application mbt1 <-ceiledGenTerm uplimit gi mbt2 <-ceiledGenTerm uplimit gi return $ case mbt1 of Just t1 -> case mbt2 of Just t2 -> if 2 + size t1 + size t2 <= uplimit then Just (App t1 t2) else Nothing Nothing -> Nothing

Figure 8 :

 8 Figure 8: Boltzmann sampler for large λ-terms

  1. Values T ∞,43 , T ∞,44 , T ∞,45 and T ∞,46 are not available since they

	n S0,n	n T0,n	n S∞,n	n T∞,n
	0 0	0 0	0 0	0
	1 0	1 0	1 0	0
	2 0	2 0	2 1	1
	3 0	3 0	3 1	1
	4 1	4 1	4 2	2
	5 0	5 0	5 2	2
	6 1	6 1	6 4	3
	7 1	7 1	7 5	5
	8 2	8 1	8 10	8
	9 1	9 1	9 14	13
	10 6	10 5	10 27	22
	11 5	11 4	11 41	36
	12 13	12 9	12 78	58
	13 14	13 13	13 126	103
	14 37	14 23	14 237	177
	15 44	15 29	15 399	307
	16 101	16 67	16 745	535
	17 134	17 94	17 1292	949
	18 298	18 179	18 2404	1645
	19 431	19 285	19 4259	2936
	20 883	20 503	20 7915	5207
	21 1361	21 795	21 14242	9330
	22 2736	22 1503	22 26477	16613
	23 4405	23 2469	23 48197	29921
	24 8574	24 4457	24 89721	53588
	25 14334	25 7624	25 164766	96808
	26 27465	26 13475	26 307294	174443
	27 47146	27 23027	27 568191	316267
	28 89270	28 41437	28 1061969	572092
	29 156360	29 72165	29 1974266	1040596
	30 293840	30 128905	30 3698247	1888505
	31 522913	31 227510	31 6905523	3441755
	32 978447	32 405301	32 12964449	6268500
	33 1761907	33 715078	33 24295796	11449522
	34 3288605	34 1280127	34 45711211	20902152
	35 5977863	35 2279393	35 85926575	38256759
	36 11148652	36 4086591	36 161996298	70004696
	37 20414058	37 7316698	37 305314162	128336318
	38 38071898	38 13139958	38 576707409	235302612
	39 70125402	39 23551957	39 1089395667	432050796
	40 130880047	40 42383667	40 2061428697	793513690
	41 242222714	41 76278547	41 3901829718	1459062947
	42 452574468	42 137609116	42 7395529009	2683714350
	43 840914719	43 248447221	43 14023075765	unknown
	44 1573331752	44 449201368	44 26620080576	unknown
	45 2933097201	45 812315229	45 50556677634	unknown
	46 5495929096	46 1470997501	46 96108150292	unknown

An alternative to universal Turing machine.

Given a predicate P , [P ( x)] denotes the Iverson symbol, i.e., [P ( x)] = 1 if P ( x) and [P ( x)] = 0 if ¬P ( x).

Tromp constructed a self-interpreter (which is not typable) for the λ-calculus of size 210.

Acknowledgements

The authors are happy to acknowledge people who commented early versions of this paper, and contributed to improve it, especially the editors and the referees of the Journal of Functional Programming and of the 25th International Conference on Probabilistic, Combinatorial and Asymptotic Methods for the Analysis of Algorithms. The authors would like to give special mentions to Olivier Bodini, Bernhard Gittenberger, Éric Fusy, Patrik Jansson, Marek Zaionc and the participants of the 8th Workshop on Computational Logic and Applications.

* This work was partially supported by the grant 2013/11/B/ST6/00975 founded by the Polish National Science Center.