# On the number of lambda terms with prescribed size of their De Bruijn
representation111This work was partially supported by FWF grant SFB F50-03.

Bernhard Gittenberger  Zbigniew Gołębiewski Institute for Discrete Mathematics
and Geometry, Technische Universität Wien, Wiedner Hauptstrasse 8-10/104,
A-1040 Wien, Austria. Supported by FWF grant SFB F50-03

###### 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\left(n^{-3/2}\tau^{-n}\right)$ for $\tau\approx 1.963448\ldots$. 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 $\mathrm{\Theta}\left(n^{-3/2}\rho^{-n}\right)$ with
some class dependent constant $\rho$, 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.

##  1 Introduction

The objects of our interest are lambda terms which are a basic object of
lambda calculus. A lambda term is a formal expression which is described by
the grammar $M\,::=\,x\,|\,\lambda x.M\,|\,(M\,N)$ where $x$ is a variable,
the operation $(M\,N)$ is called application, and using the quantifier
$\lambda$ is called abstraction. In a term of the form $\lambda x.M$ each
occurrence of $x$ in $M$ is called a bound variable. We say that a variable
$x$ is free in a term $M$ if it is not in the scope of any abstraction. A term
with no free variables is called closed, otherwise open. Two terms are
considered equivalent if they are identical up to renaming of the variables,
_i.e._ , more formally speaking, they can be transformed into each other by
$\alpha$-conversion.

In this paper we are interested in counting lambda terms whose size
corresponds to their De Bruijn representation (_i.e._ nameless expressions in
the sense of [3]).

######  Definition 1.

A De Bruijn representation is a word described by the following specification:

$M\,::=\,n\,|\,\lambda M\,|\,M\,N$

where $n$ is a positive integer, called a De Bruijn index. Each occurrence of
a De Bruijn index is called a variable and each $\lambda$ an abstraction. A
variable $n$ of a De Bruijn representation $w$ is bound if the prefix of $w$
which has this variable as its last symbol contains at least $n$ times the
symbol $\lambda$, otherwise it is free. The abstraction which binds a variable
$n$ is the $n$th $\lambda$ before the variable when parsing the De Bruijn
representation from that variable $n$ backwards to the first symbol.

For the purpose of the analysis we will use the notation consistent with the
one used in [1]. This means that the variable $n$ will be represented as a
sequence of $n$ symbols, namely as a string of $n-1$ so-called ’successors’
$S$ and a so-called ’zero’ $0$ at the end. Obviously, there is a one to one
correspondence between equivalence classes of lambda terms (as described in
the first paragraph) and De Bruijn representations. For instance, the De
Bruijn representation of the lambda-term $\lambda x.\lambda y.xy$ (which is
e.g. equivalent to $\lambda a.\lambda b.ab$ or $\lambda y.\lambda x.yx$) is
$\lambda\lambda 21$; using the notation with successors this becomes
$\lambda\lambda((S0)0)$.

In this paper we are interested in counting lambda terms of given size where
we use a general notion of size which covers several previously studied models
from the literature. We count the building blocks of lambda terms, zeros,
successors, abstractions and applications, with size $a,b,c$ and $d$,
respectively. Formally,

$|0|=a,\qquad|Sn|=|n|+b,\qquad|\lambda M|=|M|+c,\qquad|MN|=|M|+|N|+d.$

Thus we have for the example given above $|\lambda\lambda((S0)0)|=2a+b+2c+d.$
Assigning sizes for the symbols like above covers several previously
introduced notions of size:

  * •

so called ’natural counting’ (introduced in [1]) where $a=b=c=d=1$,

  * •

so called ’less natural counting’ (introduced in [1]) where $a=0,b=c=1,d=2$.

  * •

binary lambda calculus (introduced in [7]) where $b=1,a=c=d=2$,

######  Assumption 1.

Throughout the paper we will make the following assumptions about the
constants $a,b,c,d$:

  1. 1.

$a,b,c,d$ are nonnegative integers,

  2. 2.

$a+d\geq 1$,

  3. 3.

$b,c\geq 1$,

  4. 4.

$\gcd(b,c,a+d)=1$.

If the zeros and the applications both had size $0$ (_i.e._ $a+d=0$), then we
would have infinitely many terms of the given size, because one can insert
arbitrary many applications and zeros into a term without increasing its size.
If the successors or the abstractions had size $0$ (_i.e._ $b$ or $c$ equals
to $0$), then we would again have infinitely many terms of given size, because
one can insert arbitrarily long strings of successors or abstractions into a
term without increasing its size. The last assumption is more technical in its
nature. It ensures that the generating function associated with the sequence
of the number of lambda-terms will have exactly one singularity on the circle
of convergence.

Notations. We introduce some notations which will be frequently used
throughout the paper: If $p$ is a polynomial, then
$\mathrm{RootOf}\left\\{p\right\\}$ will denote the smallest positive root of
$p$. Moreover, we will write $[z^{n}]f(z)$ for the $n$th coefficient of the
power series expansion of $f(z)$ at $z=0$ and $f(z)\prec g(z)$ (or
$f(z)\preceq g(z)$) to denote that
$\left[z^{n}\right]f(z)<\left[z^{n}\right]g(z)$ (or
$\left[z^{n}\right]f(z)\leq\left[z^{n}\right]g(z)$) for all integers $n$.

Plan of the paper. The primary aim of this paper is the asymptotic enumeration
of closed lambda terms of given size with the size tending to infinity. In the
next section we define several classes of lambda terms as well as the
generating function associated with them, present our main results and prove
several auxiliary results which will be important in the sequel. We derive the
asymptotic equivalent of the number of closed terms of given size up to a
constant factor. This is established by construction of upper and lower bounds
for the coefficients of the generating functions. These constructions are done
in Sections 3 and 4. To get fairly accurate numerical bounds we present a
method for improving the previously obtained bounds in Section 5. Finally,
Section 6 is devoted to the derivation of very accurate results for classes of
lambda terms which have been previously studied in the literature.

##  2 Main results

In order to count lambda terms of a given size we set up a formal equation
which is then translated into a functional equation for generating functions.
For this we will utilise the symbolic method developped in [5].

Let us introduce the following atomic classes: the class of zeros
$\mathcal{Z}$, the class of successors $\mathcal{S}$, the class of
abstractions $\mathcal{U}$ and the class of applications $\mathcal{A}$. Then
the class $\mathcal{L}_{\infty}$ of lambda terms can be described as follows:

$\mathcal{L}_{\infty}=\textsc{Seq}(\mathcal{S})\times\mathcal{Z}+\mathcal{U}\times\mathcal{L}_{\infty}+\mathcal{A}\times\mathcal{L}_{\infty}^{2}$
(1)

The number of lambda terms of size $n$, denoted by $L_{\infty,n}$, is
$\left|\left\\{t\in\mathcal{L}_{\infty}:|t|=n\right\\}\right|$. Let
$L_{\infty}(z)=\sum_{n\geq 0}L_{\infty,n}z^{n}$ be the generating function
associated with $\mathcal{L}_{\infty}$. Then specification (1) gives rise to a
functional equation for the generating function $L_{\infty}(z)$:

$L_{\infty}(z)=z^{a}\sum_{j=0}^{\infty}z^{bj}+z^{c}L_{\infty}(z)+z^{d}L_{\infty}(z)^{2}.$
(2)

Solving (2) we get

$L_{\infty}(z)=\frac{1-z^{c}-\sqrt{(1-z^{c})^{2}-\frac{4z^{a+d}}{1-z^{b}}}}{2z^{d}},$

which defines an analytic function in a neighbourhood of $z=0$.

######  Proposition 1.

Let $\rho=\mathrm{RootOf}\left\\{(1-z^{b})(1-z^{c})^{2}-4z^{a+d}\right\\}$.
Then

$L_{\infty}(z)=a_{\infty}+b_{\infty}\left(1-\frac{z}{\rho}\right)^{\frac{1}{2}}+O\left(\left|1-\frac{z}{\rho}\right|\right),$
(3)

for some constants $a_{\infty}>0,b_{\infty}<0$ that depend on $a,b,c,d$.

###### Proof.

Let $f(z)=(1-z^{b})(1-z^{c})^{2}-4z^{a+d}$. Then $\rho$ is the solution of
$f(z)=0$. If we compute derivative
$f^{\prime}(z)=-4(a+b)z^{a+b-1}-2cz^{c-1}(1-z^{b})(1-z^{c})-bz^{b-1}(1-z^{c})^{2}$
we can observe that all three terms are negative for $0<z<1$. Since
$0<\rho<1$, the function $L_{\infty}(z)$ has an algebraic singularity of type
$\frac{1}{2}$ which means that its Newton-Puiseux expansion is of the form
(3).

Since $L_{\infty}(z)$ is a power series with positive coefficients, we know
that $a_{\infty}=L_{\infty}(\rho)>0$ and $b_{\infty}<0$. ∎

######  Corollary 1.

The coefficients of $L_{\infty}(z)$ satisfy $[z^{n}]L_{\infty}(z)\sim
C\rho^{-n}n^{-3/2}$, as $n\to\infty$, where $C=-b_{\infty}/(2\sqrt{\pi})$.

Let us define the class of $m$-open lambda terms, denoted $\mathcal{L}_{m}$,
as

$\mathcal{L}_{m}=\left\\{t\in\mathcal{L}_{\infty}:\textrm{a prefix of at most
}m\textrm{ abstractions }\lambda\textrm{ is needed to close the
term}\right\\}.$

The number of $m$-open lambda terms of size $n$ is denoted by $L_{m,n}$ and
the generating function associated with the class by $L_{m}(z)=\sum_{n\geq
0}L_{m,n}z^{n}$. Similarly to $\mathcal{L}_{\infty}$, the class
$\mathcal{L}_{m}$ can be specified, and this specification yields the
functional equation

$L_{m}(z)=z^{a}\sum_{j=0}^{m-1}z^{bj}+z^{c}L_{m+1}(z)+z^{d}L_{m}(z)^{2}$ (4)

Note that $L_{0}(z)$ is the generating function of the set $\mathcal{L}_{0}$
of closed lambda terms.

Let $\mathcal{K}_{m}=\mathcal{L}_{\infty}\setminus\mathcal{L}_{m}$ and
$K_{m}(z)=L_{\infty}(z)-L_{m}(z)$. Then using (2) and (4) we obtain

$K_{m}(z)=z^{a}\sum_{j=m}^{\infty}z^{bj}+z^{c}K_{m+1}(z)+z^{d}K_{m}(z)L_{\infty}(z)+z^{d}K_{m}(z)L_{m}(z).$
(5)

which implies

$K_{m}(z)=\frac{z^{a+bm}}{(1-z^{b})(1-z^{d}(L_{\infty}(z)+L_{m}(z)))}+\frac{z^{c}}{1-z^{d}(L_{\infty}(z)+L_{m}(z))}{}K_{m+1}(z).$
(6)

Note that $K_{m}(z)$ as well as $L_{m}(z)$ define analytic functions in a
neighbourhood of $z=0$.

Let us state the main theorem of the paper:

######  Theorem 1.

Let $\rho=\mathrm{RootOf}\left\\{(1-z^{b})(1-z^{c})^{2}-4z^{a+d}\right\\}$.
Then there exist positive constants $\underline{C}$ and $\overline{C}$
(depending on $a,b,c,d$ and $m$) such that the number of $m$-open lambda terms
of size $n$ satisfies

$\liminf_{n\to\infty}\frac{\left[z^{n}\right]L_{m}(z)}{\underline{C}n^{-\frac{3}{2}}\rho^{-n}}\geq
1\quad\textrm{and}\quad\limsup_{n\to\infty}\frac{\left[z^{n}\right]L_{m}(z)}{\overline{C}n^{-\frac{3}{2}}\rho^{-n}}\leq
1,$ (7)

######  Remark 1.

In case of given $a,b,c,d$ and $m$ we can compute numerically such constants
$\underline{C}$ and $\overline{C}$. This will be done for some of the models
mentioned in the introduction.

Before proving this theorem we will present the key ideas needed for our
proof. We introduce the class $\mathcal{L}_{m}^{(h)}$ of lambda terms in
$\mathcal{L}_{m}$ where the length of each string of successors is bounded by
a constant integer $h$. As before, set
$L_{m,n}^{(h)}=\left|\left\\{t\in\mathcal{L}_{m}^{(h)}:|t|=n\right\\}\right|$
and $L_{m}^{(h)}(z)=\sum_{n\geq 0}L_{m,n}^{(h)}z^{n}$. Then $L_{m}^{(h)}(z)$
satisfies the functional equation

$L_{m}^{(h)}(z)=\begin{cases}z^{a}\sum_{j=0}^{m-1}z^{bj}+z^{c}L_{m+1}^{(h)}(z)+z^{d}L_{m}^{(h)}(z)^{2}&\textrm{if
}m<h,\\\
z^{a}\sum_{j=0}^{h-1}z^{bj}+z^{c}L_{h}^{(h)}(z)+z^{d}L_{h}^{(h)}(z)^{2}&\textrm{if
}m\geq h.\end{cases}$ (8)

Notice that for $m\geq h$ we have a quadratic equation for
$L_{m}^{(h)}(z)=L_{h}^{(h)}(z)$ that has the solution

$L_{h}^{(h)}(z)=\frac{1-z^{c}-\sqrt{(1-z^{c})^{2}-4z^{a+d}\frac{1-z^{bh}}{1-z^{b}}}}{2z^{d}}.$

For $m<h$ we have a relation between $L_{m}^{(h)}(z)$ and $L_{m+1}^{(h)}(z)$
which gives rise to a representation of $L_{m}^{(h)}(z)$ in terms of nested
radicands (_cf._ [2]) after all. Indeed, for $m<h$ we have

$L_{m}^{(h)}(z)=\frac{1-\sqrt{r_{m}(z)+2z^{c}\sqrt{r_{m+1}(z)+2z^{c}\sqrt{\cdots\sqrt{r_{h-1}(z)+2z^{c}\sqrt{r_{h}(z)}}}}}}{2z^{d}}$
(9)

where

$r_{j}(z)=\begin{cases}1-4z^{a+d}\frac{1-z^{jb}}{1-z^{b}}-2z^{c}&\textrm{if
}m\leq j<h-1,\\\
1-4z^{a+d}\frac{1-z^{(h-1)b}}{1-z^{b}}-2z^{c}+2z^{2c}&\textrm{if }j=h-1,\\\
(1-z^{c})^{2}-4z^{a+d}\frac{1-z^{bh}}{1-z^{b}}&\textrm{if }j=h.\end{cases}$

One can check that the dominant singularity $\rho_{m}^{(h)}$ of
$L_{m}^{(h)}(z)$ comes from the real root of $r_{h}(z)$ which is closest to
the origin and that it is of type $\frac{1}{2}$ (_i.e._
$L_{m}^{(h)}(z)=a_{m}^{(h)}+b_{m}^{(h)}\left(1-\frac{z}{\rho^{(h)}}\right)^{\frac{1}{2}}+O\left(\left|1-\frac{z}{\rho^{(h)}}\right|\right)$
as $z\to\rho_{m}^{(h)}$ for some constants $a_{m}^{(h)},b_{m}^{(h)}$ depending
on $m$ and $h$). Notice that for all $m,k\geq 0$ we have
$\rho_{m}^{(h)}=\rho_{k}^{(h)}$ and that is why we can drop the lower index
and write just $\rho^{(h)}$ instead of $\rho_{m}^{(h)}$. Moreover,
$\rho^{(h)}>\rho$ as well as $\lim_{h\to\infty}\rho^{(h)}=\rho$.

Let us begin with computing the radii of convergence of the functions
$K_{m}(z)$ and $L_{m}(z)$. For the case of binary lambda calculus Lemmas 2 and
3 were already proven in [6]. To extend those results to our more general
setting, we will use different techniques.

######  Lemma 1.

For all $m\geq 0$ the radius of convergence of $K_{m}(z)$ equals $\rho$ (the
radius of convergence of $L_{\infty}(z)$).

###### Proof.

Inspecting (6) reveals that the key part is
$\frac{1}{1-z^{d}(L_{\infty}(z)+L_{i}(z))}$. This is the generating function
of a sequence of combinatorial structures associated with the generating
function $z^{d}(L_{\infty}(z)+L_{i}(z))$. One can check that we are not in the
supercritical sequence schema case (_i.e._ a singularity of considered
fraction does not come from the root of its denominator, see [5, pp. 293])
because $1-\rho^{d}\left(L_{\infty}(\rho)+L_{i}(\rho)\right)>0$. This follows
from

$\rho^{d}\left(L_{\infty}(\rho)+L_{i}(\rho)\right)\leq
2\rho^{d}L_{\infty}(\rho)=1-\rho^{c}<1.$

The first inequality holds because $L_{\infty}(\rho)\geq L_{i}(\rho)$ for all
$i\geq 0$ and the second one because $\rho>0$. Moreover, the radius of
convergence of $L_{i}(z)$ is larger than or equal to the radius of convergence
of $L_{\infty}(z)$ because $\mathcal{L}_{i}\subseteq\mathcal{L}_{\infty}$.
Therefore, for all $m\geq 0$ the radius of convergence of $K_{m}(z)$ equals
$\rho$, the radius of convergence of $L_{\infty}(z)$. ∎

######  Lemma 2.

All the functions $L_{m}(z)$, $m\geq 0$, have the same radius of convergence.

###### Proof.

Let $\rho_{m}$ denote the radius of convergence of the function $L_{m}(z)$.
From the definition of the function $L_{m}(z)$ it is known that for all $m\geq
0$ and for all $n$ we have
$\left[z^{n}\right]L_{m}(z)\leq\left[z^{n}\right]L_{m+1}(z)$ and therefore
$\rho_{m}\geq\rho_{m+1}$. Moreover, from (4) we know

$L_{m+1}(z)=-z^{a-c}\sum_{j=0}^{m-1}z^{bj}+z^{-c}L_{m}(z)-z^{d-c}L_{m}(z)^{2}.$

Notice that $\rho_{m}\leq 1$ because $\rho_{m}\leq\rho^{(h)}<1$ for $h\geq m$.
Then due to the fact that $z^{-c}L_{m}(z)-z^{d-c}L_{m}(z)^{2}$ has radius of
convergence bigger or equal $\rho_{m}$, we have $\rho_{m}\leq\rho_{m+1}$. ∎

######  Lemma 3.

For all $m\geq 0$ the radius of convergence of $L_{m}(z)$ equals $\rho$.

###### Proof.

Take $L_{m}^{(m)}$, defined in (8). Recall that $\rho^{(m)},\rho_{m}$ and
$\rho$ denote the radii of convergence of $L_{m}^{(m)}(z),L_{m}(z)$ and
$L_{\infty}(z)$, respectively. Notice that for all $m,n\geq 0$ we have
$\left[z^{n}\right]L_{m}^{(m)}(z)\leq\left[z^{n}\right]L_{m}(z)\leq\left[z^{n}\right]L_{\infty}(z)$.
Thus we also have $\rho^{(m)}\geq\rho_{m}\geq\rho$. Since $\rho^{(m)}$ is the
smallest positive solution of the equation
$(1-z)^{c}-4z^{a+d}\frac{1-z^{bm}}{1-z^{b}}=0$, we have
$\lim_{m\to\infty}\rho^{(m)}=\rho$, therefore Lemma 2 implies $\rho_{m}=\rho$.
∎

In the next sections we will present how to obtain an upper and a lower bound
for $\left[z^{n}\right]L_{m}(z)$. The idea is to construct auxiliary functions
satisfying certain inequalities and to use them to construct further ones
until we have the desired bound. The procedure follows the flowchart depicted
in Fig. 1.

$L_{m}^{(h,H)}(z)\succeq L_{m}(z)$$4$$K_{m}^{(h,H)}(z)\succeq
K_{m}(z)$$5$$\overline{L_{m}}(z)\succeq L_{m}(z)$$3$$2$$L_{m}^{(h)}(z)\preceq
L_{m}(z)$$1$$K_{m}^{(h)}(z)\preceq K_{m}(z)$$\underline{L_{m}}(z)\preceq
L_{m}(z)$ Figure 1: The diagram illustrates the idea how we obtain the upper
and the lower bound (in terms of the coefficients) for the function
$L_{m}(z)$. Starting point is denoted by a blue node, the finish nodes are
red.

##  3 Upper bound for $\left[z^{n}\right]L_{m}(z)$

Notice that for all integers $h$ and $m$ we have
$\mathcal{L}_{m}^{(h)}\subset\mathcal{L}_{m}$. Moreover, for all $m,h\geq 0$
there exists $n_{m}^{(h)}$ such that
$\left[z^{n}\right]L_{m}^{(h)}(z)=\left[z^{n}\right]L_{m}(z)$ if
$n<n_{m}^{(h)}$ and
$\left[z^{n}\right]L_{m}^{(h)}(z)<\left[z^{n}\right]L_{m}(z)$ else. We will
use those properties of $L_{m}^{(h)}(z)$ in order to derive a lower bound for
the asymptotics of $\left[z^{n}\right]K_{m}(z)$.

Note that (5) corresponds to an equation of the form
$\mathcal{K}_{m}=\mathcal{F}\left(\mathcal{K}_{m},\mathcal{K}_{m+1},\mathcal{L}_{\infty},\mathcal{L}_{m}\right)$.
Now, define the new set
$\mathcal{K}_{m}^{(h)}:=\mathcal{F}\left(\mathcal{K}_{m}^{(h)},\mathcal{K}_{m+1}^{(h)},\mathcal{L}_{\infty},\mathcal{L}_{m}^{(h)}\right)$.
From the construction of $\mathcal{F}$ and the properties of
$\mathcal{L}_{m}^{(h)}$ we know that
$\mathcal{K}_{m}^{(h)}\subseteq\mathcal{K}_{m}$. Let
$K_{m,n}^{(h)}=\left|\left\\{t\in\mathcal{K}_{m}^{(h)}:|t|=n\right\\}\right|$
and $K_{m}^{(h)}(z)=\sum_{n\geq 0}K_{m,n}^{(h)}z^{n}$. Then $K_{m}^{(h)}(z)$
satisfies the functional equation

$K_{m}^{(h)}(z)=z^{a}\sum_{j=m}^{\infty}z^{bj}+z^{c}K_{m+1}^{(h)}(z)+z^{d}K_{m}^{(h)}(z)L_{\infty}(z)+z^{d}K_{m}^{(h)}(z)L_{m}^{(h)}(z).$
(10)

In fact, what we did is that we replaced in the application operation every
$m$-open lambda term (corresponding to the subterm $z^{d}K_{m}(z)L_{m}(z)$ of
(5)) by an $m$-open lambda term where each string of successors has bounded
length (corresponding to $z^{d}K_{m}(z)L_{m}^{(h)}(z)$). Solving (10) we get

$K_{m}^{(h)}(z)=\frac{z^{a-cm}}{1-z^{b}}\sum_{j=m}^{\infty}z^{j(b+c)}\prod_{i=m}^{j}\frac{1}{1-z^{d}\left(L_{\infty}(z)+L_{i}^{(h)}(z)\right)}=:S_{m,\infty}(z).$
(11)

######  Lemma 4.

Let $\rho,a_{\infty},b_{\infty}$ be as in Proposition 1 and
$\tilde{c}_{i}=1/(1-\rho^{d}(a_{\infty}+L_{i}^{(h)}(\rho)))$ and
$\tilde{d}_{i}=b_{\infty}\rho^{d}/(1-\rho^{d}(a_{\infty}+L_{i}^{(h)}(\rho)))^{2}$.
Then $K_{m}^{(h)}(z)$ admits the expansion

$K_{m}^{(h)}(z)=c_{m}^{(h)}+d_{m}^{(h)}\left(1-\frac{z}{\rho}\right)^{\frac{1}{2}}+O\left(\left|1-\frac{z}{\rho}\right|\right),\textrm{
as }z\to\rho,$ (12)

where

$\displaystyle c_{m}^{(h)}$
$\displaystyle=\begin{cases}S_{m,h-1}(\rho)+R_{c_{m}^{(h)}}&\textrm{if
}m<h,\\\
\frac{\rho^{a+bm}}{\left(1-\rho^{b}\right)\left(1-\rho^{b+c}-\rho^{d}\left(a_{\infty}+L_{h}^{(h)}(\rho)\right)\right)}&\textrm{else},\end{cases}$
$\displaystyle d_{m}^{(h)}$
$\displaystyle=\begin{cases}\frac{\rho^{a-cm}}{1-\rho^{b}}\sum_{j=m}^{h-1}\rho^{j(b+c)}\sum_{i=m}^{j}\frac{\tilde{d}_{i}}{\tilde{c}_{i}}\prod_{k=m}^{j}\tilde{c}_{k}+R_{d_{m}^{(h)}}&\textrm{if
}m<h,\\\
\frac{b_{\infty}\rho^{a+bm+d}}{\left(1-\rho^{b}\right)\left(1-\rho^{b+c}-\rho^{d}\left(a_{\infty}+L_{h}^{(h)}(\rho)\right)\right)^{2}}&\textrm{else},\end{cases}$

with

$\displaystyle R_{c_{m}^{(h)}}$
$\displaystyle=\frac{\rho^{a+bh+c(h-m)}}{\left(1-\rho^{b}\right)\left(1-\rho^{b+c}-\rho^{d}\left(a_{\infty}+L_{h}^{(h)}(\rho)\right)\right)}\prod_{i=m}^{h-1}\tilde{c}_{i},$
$\displaystyle R_{d_{m}^{(h)}}$
$\displaystyle=\frac{b_{\infty}\rho^{a+bh+c(h-m)+d}}{\left(1-\rho^{b}\right)\left(1-\rho^{b+c}-\rho^{d}\left(a_{\infty}+L_{h}^{(h)}(\rho)\right)\right)}\left(\prod_{i=m}^{h-1}\tilde{c}_{i}\right)$
$\displaystyle\qquad\qquad\times\left(\sum_{i=m}^{h-1}\tilde{c}_{i}+\frac{1}{1-\rho^{b+c}-\rho^{d}\left(a_{\infty}+L_{h}^{(h)}(\rho)\right)}\right).$

###### Proof.

Let us recall that for all $m\geq h$ we have $L_{m}^{(h)}(z)=L_{h}^{(h)}(z)$.
Therefore we can split the infinite sum $S_{m,\infty}(z)$ in (11) into the
finite one $S_{m,h-1}(z)$ and the rest $S_{h,\infty}(z)$.

Case I: $m<h$. First, consider the finite sum $S_{m,h-1}(z)$. As in the proof
of Lemma 1 we identify the key term, show that we are not in the supercritical
case, and expand by means of Proposition 1. Eventually, this yields

$\prod_{i=m}^{j}\frac{1}{1-z^{d}(L_{\infty}(z)+L_{i}^{(h)}(z))}=\tilde{c}_{m,j}+\tilde{d}_{m,j}\left(1-\frac{z}{\rho}\right)^{\frac{1}{2}}+O\left(\left|1-\frac{z}{\rho}\right|\right)$

where $\tilde{c}_{m,j}=\prod_{i=m}^{j}\tilde{c}_{i}$ and
$\tilde{d}_{m,j}=\sum_{i=m}^{j}\frac{\tilde{d}_{i}}{\tilde{c}_{i}}\prod_{k=m}^{j}\tilde{c}_{k}$.
Since $\left(1-\frac{z}{\rho}\right)^{\frac{1}{2}}$ does neither depend on $m$
nor on $j$ and $\frac{z^{a-cm}}{1-z^{b}}$ has poles only on the unit circle,
for all $m\geq 0$ we have

$S_{m,h-1}(z)=\tilde{\tilde{c}}_{m}+\tilde{\tilde{d}}_{m}\left(1-\frac{z}{\rho}\right)^{\frac{1}{2}}+O\left(\left|1-\frac{z}{\rho}\right|\right)$

where
$\tilde{\tilde{c}}_{m}=\frac{\rho^{a-cm}}{1-\rho^{b}}\sum_{j=m}^{h-1}\rho^{j(b+c)}\tilde{c}_{m,i}$
and
$\tilde{\tilde{d}}_{m}=\frac{\rho^{a-cm}}{1-\rho^{b}}\sum_{j=m}^{h-1}\rho^{j(b+c)}\tilde{d}_{m,i}$.

Now, let us look on the infinite part of the sum in (11). We will refer to its
contributions to the first and second coefficient of the Newton-Puiseux
expansion (12) as the remainders $R_{c_{m}^{(h)}}$ and $R_{d_{m}^{(h)}}$,
respectively. Since for all $m\geq h$ we have $L_{m}^{(h)}(z)=L_{h}^{(h)}(z)$,
the sum can be rewritten as

$S_{h,\infty}(z)=\left(\prod_{i=m}^{h-1}\frac{1}{1-z^{d}\left(L_{\infty}(z)+L_{i}^{(h)}(z)\right)}\right)\cdot\frac{z^{a+bh+c(h-m)}}{\left(1-z^{b}\right)\left(1-z^{b+c}-z^{d}\left(L_{\infty}(z)+L_{h}^{(h)}(z)\right)\right)}.$

We already know how to handle the product part of this expression, so let us
consider the fraction
$\frac{z^{a+bh+c(h-m)}}{\left(1-z^{b}\right)\left(1-z^{b+c}-z^{d}\left(L_{\infty}(z)+L_{h}^{(h)}(z)\right)\right)}$.
Similarly to before, we have to check that the singularity of this function
does not come from the root of the denominator but from $L_{\infty}(z)$ (it
cannot come from $L_{h}^{(h)}$ because it has a bigger radius of convergence
than $L_{\infty}(z)$). So, we have to show the inequality
$1-\rho^{b+c}-\rho^{d}\left(L_{\infty}(\rho)+L_{h}^{(h)}(\rho)\right)>0$. But
from $L_{\infty}(\rho)\geq L_{h}^{(h)}(\rho)$ and $0<\rho^{b+c}<\rho^{c}<1$ we
obtain $\rho^{d}(L_{\infty}(\rho)+L_{h}^{(h)}(\rho))\leq
2\rho^{d}L_{\infty}(\rho)=1-\rho^{c}<1-\rho^{b+c}$ and hence the desired
inequality indeed holds. Now, similarly to the previous case we use the
Newton-Puiseux expansion of $L_{\infty}(z)$ at $\rho$ to derive an expansion
of the infinite part of the sum in (11) and get the asserted result.

Case II: $m\geq h$. This case is easier, because the finite part of the sum in
(11) does not exist and the other part can be evaluated to a closed form which
can be treated as above. ∎

Using the transfer lemmas of [4] (applied to $K_{m}^{(h)}(z)$) and
$\left[z^{n}\right]K_{m}^{(h)}(z)\leq\left[z^{n}\right]K_{m}(z)$, we get
$\liminf_{n\to\infty}\left(\left[z^{n}\right]K_{m}(z)\right)\cdot\Gamma(-1/2)n^{3/2}\rho^{n}/d_{m}^{(h)}\geq
1$.

######  Corollary 2.

The number of $m$-open lambda terms of size $n$ satisfies

$\limsup_{n\to\infty}\frac{\left[z^{n}\right]L_{m}(z)}{\overline{C}n^{-\frac{3}{2}}\rho^{-n}}\leq
1\textrm{ where
}\overline{C}=\frac{b_{\infty}-d_{m}^{(h)}}{\Gamma\left(-\frac{1}{2}\right)}.$

##  4 Lower bound for $\left[z^{n}\right]L_{m}(z)$

The idea behind obtaining a lower bound for $\left[z^{n}\right]L_{m}(z)$ is
similar to the one used for the upper bound. First we will find an upper bound
for $\left[z^{n}\right]K_{m}(z)$ using the function

$L_{m}^{(h,H)}(z)=\sum_{n\geq
0}L_{m,n}^{(h,H)}z^{n}=\begin{cases}L_{\infty}(z)-K_{m}^{(h)}(z)&\textrm{if
}m<H,\\\ L_{\infty}(z)&\textrm{else.}\end{cases}$ (13)

Notice that for all $m,h,H,n\geq 0$ we have
$\left[z^{n}\right]L_{m}(z)\leq\left[z^{n}\right]L_{m}^{(h,H)}$. Let
$\mathcal{L}_{m}^{(h,H)}$ denote the class of combinatorial structures
associated with $L_{m}^{(h,H)}(z)$ and define the new set
$\mathcal{K}_{m}^{(h,H)}:=\mathcal{F}\left(\mathcal{K}_{m}^{(h,H)},\mathcal{K}_{m+1}^{(h,H)},\mathcal{L}_{\infty},\mathcal{L}_{m}^{(h,H)}\right)$.
From the construction of $\mathcal{F}$ and the above properties of
$\mathcal{L}_{m}^{(h,H)}$ we know that
$\mathcal{K}_{m}\subseteq\mathcal{K}_{m}^{(h,H)}$. Let
$K_{m,n}^{(h,H)}=\left|\left\\{t\in\mathcal{K}_{m}^{(h,H)}:|t|=n\right\\}\right|$
and $K_{m}^{(h,H)}(z)=\sum_{n\geq 0}K_{m,n}^{(h,H)}z^{n}$. Then
$K_{m}^{(h,H)}(z)$ is given by

$K_{m}^{(h,H)}(z)=z^{a}\sum_{j=m}^{\infty}z^{bj}+z^{c}K_{m+1}^{(h,H)}(z)+z^{d}K_{m}^{(h,H)}(z)L_{\infty}(z)+z^{d}K_{m}^{(h,H)}(z)L_{m}^{(h,H)}(z).$

Solving this equation and using (13) we get

$\displaystyle K_{m}^{(h,H)}(z)$
$\displaystyle=\frac{z^{a-cm}}{1-z^{b}}\sum_{j=m}^{H-1}z^{j(b+c)}\prod_{i=m}^{j}\frac{1}{1-z^{d}\left(L_{\infty}(z)+L_{m}^{(h,H)}(z)\right)}$
$\displaystyle=\frac{z^{a-cm}}{1-z^{b}}\sum_{j=m}^{H-1}z^{j(b+c)}\prod_{i=m}^{j}\frac{1}{1-z^{d}\left(2L_{\infty}(z)-K_{i}^{(h)}(z)\right)}+$
$\displaystyle\frac{z^{a+bH+c(H-m)}}{\left(1-z^{d}\right)(1-z^{b+c}-2z^{d}L_{\infty}(z))}\left(\prod_{i=m}^{H-1}\frac{1}{1-z^{d}\left(2L_{\infty}(z)-K_{i}^{(h)}(z)\right)}\right).$
(14)

######  Lemma 5.

Let $\rho$ be the radius of convergence of the function $L_{\infty}(z)$. Then
the generating function $K_{m}^{(h,H)}(z)$ admits the following expansion

$K_{m}^{(h,H)}(z)=c_{m}^{(h,H)}+d_{m}^{(h,H)}\left(1-\frac{z}{\rho}\right)^{\frac{1}{2}}+O\left(\left|1-\frac{z}{\rho}\right|\right),$
(15)

where

$\displaystyle c_{m}^{(h,H)}$
$\displaystyle=\frac{\rho^{a-cm}}{1-\rho^{b}}\sum_{j=m}^{H-1}\rho^{j(b+c)}\prod_{i=m}^{j}\frac{1}{1-\rho^{d}\left(2a_{\infty}-c_{i}^{(h)}\right)}+R_{c_{m}^{(h,H)}},$
$\displaystyle d_{m}^{(h,H)}$
$\displaystyle=\frac{\rho^{a-cm}}{1-\rho^{b}}\sum_{j=m}^{H-1}\rho^{j(b+c)}\sum_{i=m}^{j}\frac{\rho^{d}\left(2b_{\infty}-d_{i}^{(h)}\right)}{1-\rho^{d}\left(2a_{\infty}-c_{i}^{(h)}\right)}\prod_{i=m}^{j}\frac{1}{1-\rho^{d}\left(2a_{\infty}-c_{i}^{(h)}\right)}+R_{d_{m}^{(h,H)}},$

$a_{\infty},b_{\infty}$ and $c_{i}^{(h)},d_{i}^{(h)}$ come from the expansion
of $L_{\infty}(z)$ and $K_{i}^{(h)}(z)$, respectively, at $\rho$ (see
Proposition 1 and the proof of Lemma 4) and

$\displaystyle R_{c_{m}^{(h,H)}}$
$\displaystyle=\frac{\rho^{a+bH+c(H-m)}}{\left(1-\rho^{d}\right)\left(1-\rho^{b+c}-2\rho^{d}a_{\infty}\right)}\left(\prod_{i=m}^{H-1}\frac{1}{1-\rho^{d}\left(2a_{\infty}-c_{i}^{(h)}\right)}\right),$
$\displaystyle R_{d_{m}^{(h,H)}}$
$\displaystyle=\frac{\rho^{a+bH+c(H-m)+d}}{\left(1-\rho^{d}\right)\left(1-\rho^{b+c}-2\rho^{d}a_{\infty}\right)}\left(\prod_{i=m}^{H-1}\frac{1}{1-\rho^{d}\left(2a_{\infty}-c_{i}^{(h)}\right)}\right)$
$\displaystyle\qquad\qquad\times\left(\frac{2b_{\infty}}{1-\rho^{b+c}-2\rho^{d}a_{\infty}}+\sum_{i=m}^{H-1}\frac{\left(2b_{\infty}-d_{i}^{(h)}\right)}{1-\rho^{d}\left(2a_{\infty}-c_{i}^{(h)}\right)}\right).$

As in the previous section, we apply the the transfer lemmas of [4] to
$K_{m}^{(h,H)}(z)$ and use
$\left[z^{n}\right]K_{m}^{(h,H)}(z)\geq\left[z^{n}\right]K_{m}(z)$ to arrive
at the following result:

######  Corollary 3.

The number of $m$-open lambda terms of size $n$ satisfies

$\liminf_{n\to\infty}\frac{\left[z^{n}\right]L_{m}(z)}{\underline{C}n^{-\frac{3}{2}}\rho^{-n}}\geq
1\,\textrm{where
}\underline{C}=\frac{b_{\infty}-d_{m}^{(h,H)}}{\Gamma\left(-\frac{1}{2}\right)}.$

##  5 Improvement of the bounds

The bounding functions $\underline{L_{m}}(z)=L_{\infty}(z)-K_{m}^{(h,H)}(z)$
and $\overline{L_{m}}(z)=L_{\infty}(z)-K_{m}^{(h)}(z)$ derived in the previous
sections can be used in a straightforward way to compute numerical values for
$\underline{C}$ and $\overline{C}$, given concrete values for $a,b,c,d$. If we
choose $h$ and $H$ big enough, then this will give us proper bounds. But in
practice they still leave a large gap, at least for values $h$ and $H$ that
allow us to perform the computation within a few hours on a standard PC. For
instance, in case of the natural counting for $h=H=15$ we get
$\underline{C}^{(nat)}\approx 0.00404525\ldots$ and
$\overline{C}^{(nat)}\approx 0.18086721\ldots$.

We show a simple way to improve $\underline{C}$ and $\overline{C}$. Let us
introduce the functions $L_{m,M}^{(h)}(z)$ and $L_{m,M}^{(h,H)}(z)$, defined
by the following equations:

$\displaystyle L_{m,M}^{(h)}(z)$
$\displaystyle=\begin{cases}z^{a}\sum_{j=0}^{m-1}z^{bj}+z^{c}L_{m+1,M}^{(h)}(z)+z^{d}L_{m,M}^{(h)}(z)^{2}&\textrm{
if }m<M,\\\ L_{\infty}(z)-K_{M}^{(h)}(z)&\textrm{ if }m=M,\end{cases}$
$\displaystyle L_{m,M}^{(h,H)}(z)$
$\displaystyle=\begin{cases}z^{a}\sum_{j=0}^{m-1}z^{bj}+z^{c}L_{m+1,M}^{(h,H)}(z)+z^{d}L_{m,M}^{(h,H)}(z)^{2}&\textrm{
if }m<M,\\\ L_{\infty}(z)-K_{M}^{(h,H)}(z)&\textrm{ if }m=M.\end{cases}$

These two function admit a representation in terms of nested radicals which is
similar to (9):

$\displaystyle L_{m,M}^{(h)}(z)=$
$\displaystyle\quad\frac{1}{2z^{d}}\cdot\scriptstyle\left(1-\sqrt{1-4z^{a+d}\frac{1-z^{mb}}{1-z^{b}}-2z^{c}+2z^{c}\sqrt{\cdots\sqrt{1-4z^{a+d}\frac{1-z^{(M-1)b}}{1-z^{b}}-2z^{c}+2z^{c}\sqrt{L_{\infty}(z)-K_{M}^{(h)}}(z)}}}\right)\displaystyle,$
$\displaystyle L_{m,M}^{(h,H)}(z)=$
$\displaystyle\quad\frac{1}{2z^{d}}\cdot\scriptstyle\left(1-\sqrt{1-4z^{a+d}\frac{1-z^{mb}}{1-z^{b}}-2z^{c}+2z^{c}\sqrt{\cdots\sqrt{1-4z^{a+d}\frac{1-z^{(M-1)b}}{1-z^{b}}-2z^{c}+2z^{c}\sqrt{L_{\infty}(z)-K_{M}^{(h,H)}(z)}}}}\right)\displaystyle.$

So, in $L_{m,M}^{(h)}(z)$ and $L_{m,M}^{(h,H)}(z)$ we are using exact
expressions for $L_{m}(z)$ up to some constant $M$ and then replace $L_{M}(z)$
by a function that is its upper and lower bound, respectively. Numerical
results for some previously studied notions of size (see Sections 6.1 and 6.2)
reveal a significant improvement in closing the gap between the constants
$\overline{C},\underline{C}$ obtained by utilizing the functions
$L_{m,M}^{(h)}(z),L_{m,M}^{(h,H)}(z)$.

##  6 Results for some previously introduced notions of size

###  6.1 Natural counting

######  Lemma 6.

The following bounds hold

$\liminf_{n\to\infty}\frac{\left[z^{n}\right]L_{0}^{(nat)}(z)}{\underline{C}^{(nat)}n^{-\frac{3}{2}}\rho^{-n}}\geq
1\quad\textrm{and}\quad\limsup_{n\to\infty}\frac{\left[z^{n}\right]L_{0}^{(nat)}(z)}{\overline{C}^{(nat)}n^{-\frac{3}{2}}\rho^{-n}}\leq
1\,$ (16)

where $\rho=\mathrm{RootOf}\\{-1+3x+x^{2}+x^{3}\\}\approx 0.295598...$ and
$\underline{C}^{(nat)},\overline{C}^{(nat)}$ are computable constants with
numerical values $\underline{C}^{(nat)}\approx 0.00404525\ldots$ and
$\overline{C}^{(nat)}\approx 0.18086721\ldots$.

###### Proof.

For ’natural counting’ we have $a=b=c=d=1$. From Theorem 1 we know that the
radius of convergence of $L_{0}^{(nat)}(z)$ equals
$\rho=\mathrm{RootOf}\left\\{-1+3x+x^{2}+x^{3}\right\\}\approx
0.295598\ldots$. We can also easily get $L_{\infty}(z)\sim
a_{\infty}+b_{\infty}\sqrt{1-z/\rho}$ with

$a_{\infty}=\frac{1-\rho}{2\rho}\approx 1.19149\ldots\textrm{ and
}b_{\infty}=\frac{1}{\rho-1}\sqrt{\frac{1+\rho+\rho^{2}-\rho^{3}}{2\rho}}\approx
2.15093\ldots,$

and from the transfer lemmas of [4] we obtain
$\left[z^{n}\right]L_{\infty}(z)\sim
b_{\infty}n^{-3/2}\rho^{-n}/\Gamma(-1/2)\simeq(0.606767\ldots)\cdot
n^{-\frac{3}{2}}(3.38298\ldots)^{n}$, as $n\to\infty$.

$h,H$ | $c_{0}^{(h)}$ | $d_{0}^{(h)}$ | $c_{0}^{(h,H)}$ | $d_{0}^{(h,H)}$
---|---|---|---|---
$1$ | $0.855448$ | $-1.153959$ | $1.086200$ | $-3.803686$
$2$ | $0.898032$ | $-1.313246$ | $0.979519$ | $-2.581823$
$3$ | $0.917305$ | $-1.397536$ | $0.958215$ | $-2.324953$
$4$ | $0.927248$ | $-1.444672$ | $0.950295$ | $-2.236290$
$5$ | $0.932849$ | $-1.472308$ | $0.946185$ | $-2.192353$
$6$ | $0.936128$ | $-1.488826$ | $0.943824$ | $-2.167379$
$7$ | $0.938055$ | $-1.498647$ | $0.942443$ | $-2.152790$
$8$ | $0.939174$ | $-1.504385$ | $0.941643$ | $-2.144335$
$9$ | $0.939813$ | $-1.507673$ | $0.941187$ | $-2.139511$
$10$ | $0.940172$ | $-1.509525$ | $0.940931$ | $-2.136799$
$11$ | $0.940372$ | $-1.510556$ | $0.940788$ | $-2.135291$
$12$ | $0.940482$ | $-1.511125$ | $0.940710$ | $-2.134460$
$13$ | $0.940543$ | $-1.511438$ | $0.940667$ | $-2.134004$
$14$ | $0.940576$ | $-1.511608$ | $0.940643$ | $-2.133755$
$15$ | $0.940594$ | $-1.511701$ | $0.940630$ | $-2.133619$
Table 1: Numbers rounded up to $7$ digits.

Since we are most interested in the enumeration of closed lambda terms, we
examine the multiplicative constants in the leading term of the asymptotical
lower and upper bound for $\left[z^{n}\right]L_{0}(z)$. From the formulas in
Lemmas 4 and 5 we have computed the values for $c_{0}^{(h)},d_{0}^{(h)}$ and
$c_{0}^{(h,H)},d_{0}^{(h,H)}$ for different constants $h$ and $H$ (see Table
1).

Figure 2: Plot of the exact value of
$\frac{\left[z^{n}\right]L_{0}^{(nat)}(z)}{n^{-\frac{3}{2}}\rho^{-n}}$ and
computed lower and upper bound for $h=H=15$ and $10\leq n\leq 150$.

As expected, the bigger $h$ and $H$ are, the more accurate is the bound we get
(in this case for $\left[z^{n}\right]K_{0}(z)$). Taking the values of
$d_{0}^{(h,H)}$ and $d_{0}^{(h)}$ for $h=H=15$, Corollaries 3 and 2 yield
$\underline{C}^{(nat)}\approx 0.00404525\ldots$ and
$\overline{C}^{(nat)}\approx 0.18086721\ldots$. Notice that using the values
of $d_{0}^{(h,H)}$ to compute $\underline{C}^{(nat)}$ gives non-trivial values
only for $h>7$ (for $1\leq h\leq 7$ we get negative numbers because in this
case we have $\left|d_{0}^{(h,H)}\right|>\left|b_{\infty}\right|$). ∎

Figure 2 illustrates the bounds we obtained and the exact values of the
coefficients $\left[z^{n}\right]L_{0}^{(nat)}(z)$ for $10\leq n\leq 150$.
Applying the approach discussed in Section 5 for $h=H=M=13$ we get the
following improvement.

######  Lemma 7.

The following bounds hold

$\liminf_{n\to\infty}\frac{\left[z^{n}\right]L_{0}^{(nat)}(z)}{\underline{\underline{C}}^{(nat)}n^{-\frac{3}{2}}\rho^{-n}}\geq
1\quad\textrm{and}\quad\limsup_{n\to\infty}\frac{\left[z^{n}\right]L_{0}^{(nat)}(z)}{\overline{\overline{C}}^{(nat)}n^{-\frac{3}{2}}\rho^{-n}}\leq
1\,$ (17)

where $\rho=\mathrm{RootOf}\\{-1+3x+x^{2}+x^{3}\\}\approx 0.295598\ldots$ and
$\underline{\underline{C}}^{(nat)},\overline{\overline{C}}^{(nat)}$ are
computable constants with numerical values
$\underline{\underline{C}}^{(nat)}\approx 0.07790995266\ldots$ and
$\overline{\overline{C}}^{(nat)}\approx 0.07790998229\ldots$.

Figure 3: Plot of the numerical values for the constants
$\underline{\underline{C}}^{(nat)},\overline{\overline{C}}^{(nat)}$ for $8\leq
h=H=M\leq 13$.

Figure 3 illustrates how the improvement discussed in Section 5 allows to
reduce the gap between the constants
$\underline{\underline{C}}^{(nat)},\overline{\overline{C}}^{(nat)}$ for the
lower and the upper bound.

###  6.2 Binary lambda calculus

######  Lemma 8.

The following bounds hold

$\liminf_{n\to\infty}\frac{\left[z^{n}\right]L_{0}^{(bin)}(z)}{\underline{\underline{C}}^{(bin)}n^{-\frac{3}{2}}\rho^{-n}}\geq
1\quad\textrm{and}\quad\limsup_{n\to\infty}\frac{\left[z^{n}\right]L_{0}^{(bin)}(z)}{\overline{\overline{C}}^{(bin)}n^{-\frac{3}{2}}\rho^{-n}}\leq
1\,$ (18)

where $\rho=\mathrm{RootOf}\\{-1+x+2x^{2}-2x^{3}+3x^{4}+x^{5}\\}\approx
0.509308\ldots$ and
$\underline{\underline{C}}^{(bin)},\overline{\overline{C}}^{(bin)}$ are
computable constants with numerical values
$\underline{\underline{C}}^{(bin)}\approx 0.01252417\ldots$ and
$\overline{\overline{C}}^{(bin)}\approx 0.01254593\ldots$.

In order to proof this lemma it is enough to recall that in case of binary
lambda calculus the size defining constants are $b=1$ and $a=c=d=2$. Then we
used the functions $L_{0,13}^{13,13}(z),L_{0,13}^{13,13}(z)$ to obtain the
numerical constants stated in Lemma 8.

## References

  * [1] Maciej Bendkowski, Katarzyna Grygiel, Pierre Lescanne, and Marek Zaionc.  A natural counting of lambda terms.  CoRR, abs/1506.02367, 2015.
  * [2] Olivier Bodini, Danièle Gardy, and Bernhard Gittenberger.  Lambda-terms of bounded unary height.  In Philippe Flajolet and Daniel Panario, editors, Proceedings of the Eighth Workshop on Analytic Algorithmics and Combinatorics, ANALCO 2011, San Francisco, California, USA, January 22, 2011, pages 23–32. SIAM, 2011.
  * [3] N. G. de Bruijn.  Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem.  Nederl. Akad. Wetensch. Proc. Ser. A 75=Indag. Math., 34:381–392, 1972.
  * [4] Philippe Flajolet and Andrew M. Odlyzko.  Singularity analysis of generating functions.  SIAM J. Discrete Math., 3(2):216–240, 1990.
  * [5] Philippe Flajolet and Robert Sedgewick.  Analytic Combinatorics.  Cambridge University Press, New York, NY, USA, 1 edition, 2009.
  * [6] Katarzyna Grygiel and Pierre Lescanne.  Counting terms in the binary lambda calculus.  In DMTCS. 25th International Conference on Probabilistic, Combinatorial and Asymptotic Methods for the Analysis of Algorithms. Discrete Mathematics & Theoretical Computer Science, Jun 2014.
  * [7] John Tromp.  Binary lambda calculus and combinatory logic.  In Marcus Hutter, Wolfgang Merkle, and Paul M.B. Vitanyi, editors, Kolmogorov Complexity and Applications, number 06051 in Dagstuhl Seminar Proceedings, Dagstuhl, Germany, 2006. Internationales Begegnungs- und Forschungszentrum für Informatik (IBFI), Schloss Dagstuhl, Germany.

## Appendix

Below we present the proof of Lemma 5.

###### Proof.

Throughout the proof we will make use of Equation (14). Let us first focus on
the finite sum:
$\frac{z^{a-cm}}{1-z^{b}}\sum_{j=m}^{H-1}z^{j(b+c)}\prod_{i=m}^{j}\frac{1}{1-z^{d}\left(2L_{\infty}(z)-K_{i}^{(h)}(z)\right)}$.
The key part of it
$\frac{1}{1-z^{d}\left(2L_{\infty}(z)-K_{i}^{(h)}(z)\right)}$ is the
generating function of a sequence of structures enumerated by the denominator
$z^{d}\left(2L_{\infty}(z)-K_{i}^{(h)}(z)\right)$. Like in case of Equation
(11), one can check that we are not in the supercritical sequence schema case
because

$\displaystyle 1-\rho^{d}\left(2L_{\infty}(\rho)-K_{i}^{(h)}(\rho)\right)$
$\displaystyle>0$
$\displaystyle\rho^{d}\left(2L_{\infty}(\rho)-K_{i}^{(h)}(\rho)\right)\leq
2\rho^{d}L_{\infty}(\rho)=1-\rho^{c}$ $\displaystyle<1.$

Second inequality holds because $K_{i}^{(h)}(\rho)>0$ for all $i\geq 0$. The
last inequality holds because we have $\rho>0$ for all $a,b,c,d$ that
satisfies Assumption 1. Therefore, for all $i$ from the Newton-Puiseux
expansion of $L_{\infty}(z)$ and $K_{i}^{(h)}(z)$ at singularity $\rho$ (see
Proposition 1 and Lemma 4) we have :

$\frac{1}{1-z^{d}\left(2L_{\infty}(z)-K_{i}^{(h)}(z)\right)}=\dot{c}_{i}+\dot{d}_{i}\left(1-\frac{z}{\rho}\right)^{\frac{1}{2}}+O\left(1-\frac{z}{\rho}\right),$
(19)

where
$\dot{c}_{i}=\frac{1}{1-\rho^{d}\left(2a_{\infty}-c_{i}^{(h)}\right)},\dot{d}_{i}=\frac{\rho^{d}\left(2b_{\infty}-d_{i}^{(h)}\right)}{\left(1-\rho^{d}\left(2a_{\infty}-c_{i}^{(h)}\right)\right)^{2}}$.
Moreover, we have

$\prod_{i=m}^{j}\frac{1}{1-z^{d}(2L_{\infty}(z)-K_{i}^{(h)}(z))}=\dot{c}_{m,j}+\dot{d}_{m,j}\left(1-\frac{z}{\rho}\right)^{\frac{1}{2}}+O\left(1-\frac{z}{\rho}\right),$

where
$\dot{c}_{m,j}=\prod_{i=m}^{j}\dot{c}_{i},\dot{d}_{m,j}=\sum_{i=m}^{j}\frac{\dot{d}_{i}}{\dot{c}_{i}}\prod_{k=m}^{j}\dot{c}_{k}$.
Since $\left(1-\frac{z}{\rho}\right)^{\frac{1}{2}}$ does not depend on $m$ and
$j$ and $\frac{z^{a-cm}}{1-z^{b}}$ have poles only on the unit circle, we have
for all $m\geq 0$ the following

$\frac{z^{a-cm}}{1-z^{b}}\sum_{j=m}^{H-1}z^{j(b+c)}\prod_{i=m}^{j}\frac{1}{1-z^{d}\left(2L_{\infty}(z)-K_{i}^{(h)}(z)\right)}=\ddot{c_{m}}+\ddot{d_{m}}\left(1-\frac{z}{\rho}\right)^{\frac{1}{2}}+O\left(1-\frac{z}{\rho}\right),$

where
$\ddot{c_{m}}=\frac{\rho^{a-cm}}{1-\rho^{b}}\sum_{j=m}^{H}\rho^{j(b+c)}\dot{c}_{m,j},\ddot{d_{m}}=\frac{\rho^{a-cm}}{1-\rho^{b}}\sum_{j=m}^{H}\rho^{j(b+c)}\dot{d}_{m,j}$.

In case of the remainder:
$\frac{z^{a+bH+c(H-m)}}{\left(1-z^{d}\right)(1-z^{b+c}-2z^{d}L_{\infty}(z))}\left(\prod_{i=m}^{H-1}\frac{1}{1-z^{d}\left(2L_{\infty}(z)-K_{i}^{(h)}(z)\right)}\right)$
we proceed similarly to the proof of Lemma 4. We already know how to handle
the product part of this expression, so let us consider the fraction:
$\frac{z^{a+bH+c(H-m)}}{\left(1-z^{d}\right)(1-z^{b+c}-2z^{d}L_{\infty}(z))}$.
Similarly to before, we have to check that the singularity of this function
does not come from the root of the denominator but from the function
$L_{\infty}(z)$. So the following inequality has to hold:

$\displaystyle 1-\rho^{b+c}-2\rho^{d}L_{\infty}(\rho)$ $\displaystyle>0$
$\displaystyle 2\rho^{d}L_{\infty}(\rho)=1-\rho^{c}$
$\displaystyle<1-\rho^{b+c}.$

Second inequality holds because we have $0<\rho^{b+c}<\rho^{c}$ for all
$a,b,c,d$ that satisfies Assumption 1. Now, similarly to the previous case
using the Newton-Puiseux expansion of $L_{\infty}(z)$ at $\rho$ we can derive
expansion of this part of Equation (14). ∎