Lambda counting

counting.pdf : [1] version on wednesday 07/01 at 17h30. the files below are the good ones. René

Introduction

intro : [2]

lambda

[3]

combinatorics

section 3 : [4]

generating : [5]

bounds

[6]

main results

[7]

section 5-2

[8]

section 5-2-2  : [9]

section 5-2-3  : [10]

section 5-2-4  : [11]

section 5-3

[12]

section 5-3-1  : [13]

section 5-3-2  : [14]

section 5-3-3  : [15]

section 5-3-4  : [16]

other systems

[17]

section 6.1 : [18]

section 6.2 : [19]

conclusion

[20]

section 7.1 : [21]

section 7.2 : [22]

section 7.3 : [23]

biblio

[24]

appendix

[25]

appendix-1 : [26]

appendix-2 : [27]

What appears below is the old version

Known results for Turing machines and cellular automata

In this section I propose to comment on paper [28] and [29].

Guillaume says: I am very skeptical about paper 2 by D'Abramo. I suggest to replace it by the paper by Calude and Stay [30].

Lambert function, Catalan and Motzkin numbers

Catalan numbers

• $C(n)$ : Catalan numbers

Usual equivalent: $C(n)\sim {\frac {4^{n}}{n^{3/2}{\sqrt {\pi }}}}$ which is obtained using Strirling formula. However, using stirling formula which can be extended as the following double inequality: ${\sqrt {2\pi n}}n^{n}e^{\left(-n+{\frac {1}{12n+1}}\right)}<n!<{\sqrt {2\pi n}}n^{n}e^{\left(-n+{\frac {1}{12n}}\right)}$

$C(n)={\frac {(2n)!}{(n+1)!n!}}\geq {\frac {4^{n}}{{\sqrt {\pi }}(n+1)^{\frac {3}{2}}}}\left({\frac {n}{n+1}}\right)^{n}e^{\left(1+{\frac {1}{24n+1}}-{\frac {1}{12n+12}}-{\frac {1}{12n}}\right)}$

Thus, using this and $\left({\frac {n}{n+1}}\right)^{n}>e^{-1}$, we have:

$C(n)\geq {\frac {4^{n}}{{\sqrt {\pi }}(n+1)^{\frac {3}{2}}}}e^{\left({\frac {1}{24n+1}}-{\frac {1}{12n+12}}-{\frac {1}{12n}}\right)}$

Then, we can check that

${\frac {1}{24n+1}}-{\frac {1}{12n+12}}-{\frac {1}{12n}}={\frac {-36n^{2}-14n-1}{12(24n+1)(n+1)n}}\geq -{\frac {51}{288n}}$

Thus finally $C(n)\geq {\frac {4^{n}}{{\sqrt {\pi }}(n+1)^{\frac {3}{2}}}}e^{\left(-{\frac {17}{96n}}\right)}\geq {\frac {4^{n}}{{\sqrt {\pi }}(n+1)^{\frac {3}{2}}}}e^{\left(-{\frac {17}{96}}\right)}$ for all $n\geq 1$.

Motzkin numbers

In fact, these are not usual Motzkin's numbers because in $M(n)$, $n$ is the number of inner nodes while usually, this is the total number of nodes, including leaves. The number we use are known as large Schroeder numbers.

Let us define $M(n,k)$ the number of unary-binary trees with $n$ inner nodes and $k$ leafs. A tree with $n$ inner node $k$ leafs has exactly $k-1$ binary nodes and therefore $n-k+1$. Hence we get the following formula

$M(n,k)=C(k-1){n+k-1 \choose n-k+1}$

Then, by summing we define $M(n)$ the number of unary-binary trees with $n$ inner nodes and give an equivalent:

$M(n)=\sum _{k\geq 1}M(n,k)\sim \left({\frac {1}{3-2{\sqrt {2}}}}\right)^{n}{\frac {1}{n^{\frac {3}{2}}}}$

Lambert W function

The Lambert function $W(x)$ is defined by the equation $x=W(x)e^{W(x)}$ which has a unique solution in $\mathbb {R} _{+}$.

For $x\geq e$, we have $\ln(x)-\ln(\ln(x))\leq W(x)\leq \ln(x)$ which implies that $W(x)\sim \ln(x)$ near $+\infty$. To prove this, it is enough to remark that

$(\ln(x)-\ln(\ln(x))e^{\ln(x)-\ln(\ln(x))}=x\left(1-{\frac {\ln(\ln(x))}{\ln(x)}}\right)\leq x\leq x\ln(x)=\ln(x)e^{\ln(x)}$

This is not precise enough for our purpose. Using one step of the Newton method from $\ln(x)-\ln(\ln(x))$, we can find a better upper bound for $W(x)$ because $y\mapsto ye^{y}$ is increasing and convex when $y\geq 0$. This gives for $x\geq e$:

$\ln(x)-\ln(\ln(x))\leq W(x)\leq \ln(x)-\ln(\ln(x))+{\frac {\ln(\ln(x))}{\ln(x)-\ln(\ln(x))+1}}$

Indeed, if we define $f(y)=ye^{y}$, we have $f'(y)=(1+y)e^{y}$ and therefore, newton's method from $A=\ln(x)-\ln(\ln(x))$ gives a point at position:

$A-{\frac {f(A)-x}{f'(A)}}=A+{\frac {x\ln(\ln(x))}{\ln(x)}}{\frac {\ln(x)}{x(\ln(x)-\ln(\ln(x))+1)}}=A+{\frac {\ln(\ln(x))}{\ln(x)-\ln(\ln(x))+1}}$

Finally, we show that for $x\geq e$, we have:

$\ln(x)-\ln(\ln(x))\leq W(x)\leq \ln(x)-\ln(\ln(x))+1$

Indeed, for $x>1$, we have $e^{\sqrt {ex}}\geq 1+{\sqrt {ex}}+{\frac {ex}{2}}\geq x$, which implies $ex\geq \ln ^{2}(x)$ and therefore $\ln(x)-\ln \ln(x)+1\geq \ln \ln(x)$.

combinatory logic

Basically the paper already written by Marek

tex file : [31]

pdf file :[32]

+ the following

As we will see in section ??, theorem ?? does not holds for the Lambda calculus. This may be surprising since there are translations between these systems which respect many properties (for exemple the one of being terminating). However these translations do not preserve the size.

The translation $T$ from combinatory logic to lambda calculus is linear, i.e. there is a constant $k$ such that, for all terms, $size(T(t))\leq k*size(t)$ but the translation $S$ in the other direction is not linear. As far as we know, there is no known bound on the size of $S(t)$ but it is not difficult to find exemples where $size(S(t))$ is of order $size(t)^{3}$.

The point is that $S$ has to code the binding in some way and this takes place. It will be interesting to compare the size of $S(t)$ with the one of $t$ using other notion of size than the usual one. See section ?? for some complement.

Generality on lambda calculus

definition

The set $\Lambda$ of lambda terms (or, simply, terms) is defined by the following grammar

$t,u:=Var\ \mid \ \lambda x.t\ \mid \ (t\ u)$

To be able to define the notion of a random term we have to define a distribution law on $\Lambda$. There are many possibilities for that. We choose here the simplest one. Note that this is the one for which, at least at present, we are able to prove some results. It is based on densities. For that we first have to define the size of a term.

The usual definition is the following.

definition

The size (denoted as $size_{1}(t)$) of a term $t$ is defined by the following rules.

- $size_{1}(t)=1$ if $t$ is a variable.

- $size_{1}(\lambda x.t)=size_{1}(t)+1$

- $size_{1}((t\ u))=size_{1}(t)+size_{1}(u)+1$

In the rest of the paper we will use another definition (denoted as $size_{0}(t)$) which is similar but gives simpler computations. We believe (but we have not yet checked the details) that, with $size_{1}$ we would have similar results. The computation, with $size_{1}$, of the upper and lower bounds of the number of terms of size $n$ will be done in section ??

definition

The size (denoted as $size_{0}(t)$ or, more simply $size(t)$) of a term $t$ is defined by the following rules.

- $size_{0}(t)=1$ if $t$ is a variable.

- $size_{0}(\lambda x.t)=size_{0}(t)+1$

- $size_{0}((t\ u))=size_{0}(t)+size_{0}(u)+1$

These definitions of the size are, for the implementation point of view, not realistic because, in case a term has a lot of distinct variables, it is not realistic to use a single bit to code them. The usual way to implement this coding is to replace the names of variables by their so called de Bruijn indices: a variable is replaced by the number of $\lambda$ that occur, on the path from the variable to the root, between the variable and the $lambda$ that binds it. Note that, in this case, different occurrences of the same variable may be represented by different indices.

Choosing the way we code these de Bruijn indices gives different other ways of defining the size of a term. This can be done in the following ways

- Use unary notation, i.e. the size of the index $n$ simply is $n$ itself

- Use optimal binary notation, i.e. the size of the index $n$ is $log_{2}(n)$ i.e. the logarithm of $n$ in base 2.

- Use uniform binary notation, i.e. the size of an index is the logarithm, in base 2, of the number of leaves of the term.

Remark

See section ?? for a discusion about these different size.

definition

Let $n$ be an integer. We denote by $\Lambda _{n}$ the set of $\lambda$ terms of size n.

definition

Let A be a set of $\lambda$ terms.

1) We denote by $\#(A)$ the cardinality of A.

2) We denote by $d(A)$ the limit, for n going to $\infty$, of ${\frac {\#(A\cap \Lambda _{n})}{\#(\Lambda _{n})}}$.

Remark

Note that d is not exactly a measure since $d(A)$ is undefined if the previous limit does not exist

definition

Let P be a property of terms. We will say that almost every term satisfies P (this will be also stated as P holds a.e.) if $d(\{t\ |\ P(t)holds\})=1$

generating functions

this does not work (by now) because radius of convergence 0

no known results for the number of terms of size n (denoted $L_{n}$)

our results

(the proof of result of section k needs the result of section (k-1))

Upper and lower bounds for $L_{n}$

For the lower bound, we will first count the number $LB(n,k)$ of lambda-terms of size $n$ starting with $k$ lambdas and having no other lambda below. This means that the lower part of the term is a binary tree with $n-k$ inner nodes with $k$ possibility for each leaf. Therefore we have:

$LB(n,k)=C(n-k)k^{n-k+1}$

And therefore, for $n>k$, using our lower bound for $C(n)$ and $n+1\geq n-k+1$, we get:

$LB(n,k)\geq K{\frac {(4k)^{n-k+1}}{(n+1)^{\frac {3}{2}}}}$ with $K={\frac {e^{-{\frac {17}{96}}}}{4{\sqrt {\pi }}}}$

Now, for $n$ fixed, we define $f(\alpha )=\left(4n\alpha \right)^{n(1-\alpha )+1}$ (so $LB(n,k)\geq {\frac {K}{(n+1)^{\frac {3}{2}}}}f\left({\frac {k}{n}}\right)$) and look for the maximum of this function. We have $f'(\alpha )=f(\alpha )\left(-n\ln(4n\alpha )+{\frac {n(1-\alpha )+1}{\alpha }}\right)$. Thus, $f'(\alpha )\geq 0$ is equivalent to ${\frac {n+1}{n\alpha }}e^{\frac {n+1}{n\alpha }}\geq 4e(n+1)$. The Lambert function begin increasing this means that $f'(\alpha )\geq 0$ is equivalent to $\alpha \leq {\frac {n+1}{nW(4e(n+1))}}$. Therefore, $f(\alpha )$ reaches a maximum for $\alpha ={\frac {n+1}{nW(4e(n+1))}}$.

This means that $(4k)^{n-k}$ reaches its maximum for $n$ fixed when $k$ is near to ${\frac {n+1}{W(4e(n+1))}}$ which is likely not to be an integer. However, there are at least $\left\lfloor {\frac {(n+1)(\ln(\ln(4en))-1)}{\ln ^{2}(4en)}}\right\rfloor$ integer between ${\frac {n+1}{W(4e(n+1))}}$ and ${\frac {n+1}{\ln(4e(n+1))}}$. Indeed, using our inequalities on Lambert W function, we have:

${\frac {n+1}{W(4e(n+1))}}-{\frac {n+1}{\ln(4e(n+1))}}={\frac {(n+1)(\ln(4e(n+1))-W(4e(n+1)))}{W(4e(n+1))\ln(4e(n+1))}}\geq {\frac {(n+1)(\ln(\ln(4e(n+1)))-1)}{\ln ^{2}(4e(n+1))}}$

Thus, we get the following lowerbound for $L_{n}$:

$\#(L_{n})\geq \sum _{k=1}^{n}LB(n,k)\geq \sum _{k=\lceil {\frac {n+1}{\ln(4e(n+1))}}\rceil }^{\lfloor {\frac {n+1}{W(4e(n+1))}}\rfloor }K{\frac {(4k)^{n-k+1}}{(n+1)^{\frac {3}{2}}}}\geq K\left\lfloor {\frac {(n+1)(\ln(\ln(4e(n+1)))-1)}{\ln ^{2}(4e(n+1))}}\right\rfloor {\frac {\left({\frac {4(n+1)}{\ln(4e(n+1))}}\right)^{n-{\frac {n+1}{\ln(4e(n+1))}}+1}}{(n+1)^{\frac {3}{2}}}}$

To simplify, we first remove the constant $K$ and the integer part by replacing the $\ln(\ln(4e(n+1)))-1$ term by any constant $C$. This means that for any constant $C$, we can take $n$ large enough to have:

$\#(L_{n})\geq C{\frac {n+1}{\ln ^{2}(4e(n+1))}}{\frac {\left({\frac {4(n+1)}{\ln(4e(n+1))}}\right)^{n-{\frac {n+1}{\ln(4e(n+1))}}+1}}{(n+1)^{\frac {3}{2}}}}=C{\frac {\sqrt {n+1}}{\ln ^{3}(4e(n+1))}}\left({\frac {4(n+1)}{\ln(4e(n+1))}}\right)^{n-{\frac {n+1}{\ln(4e(n+1))}}}$

Then, using the facts that ${\frac {n+1}{\ln(4e(n+1))}}\leq {\frac {n}{\ln(n)}}$, $\lim _{n\to +\infty }{\frac {\ln(n)}{\ln(4e(n+1))}}=1$ and $\lim _{n\to +\infty }\left({\frac {\ln(n)}{\ln(4e(n+1))}}\right)^{n}=0$, we have the following lowerbound (still for $n$ large enough, with $C=1$):

$\#(L_{n})\geq {\frac {\sqrt {n}}{\ln ^{3}(n)}}\left({\frac {4n}{\ln(n)}}\right)^{n-{\frac {n}{\ln(n)}}}$

We now compute an upper bound $UB(n,k)$ for the number of lambda-terms of size $n$ with exactly $k$ lambdas (that is with $n-k+1$ leaves using the Motzkin numbers and allowing any lambda to bind any variable (regardless of the real scope):

$UB(n,k)=M(n,n-k+1)k^{n-k+1}$

If we sum this for all possible $k$ and get an upper bound of $k^{n-k+1}$ using Lambert function as for the lower bound, we get the following upper bound for $L_{n}$:

$\#(L_{n})\leq M(n)\left({\frac {n+1}{W(e(n+1))}}\right)^{n-{\frac {n+1}{W(e(n+1))}}+1}$

The ration between our upper bound and lower bound is equivalent to (NEEDS FURTHER CHECKING, OR IS REMOVED because we can do better using Jakob's remark at the end of 7.2):

$\left({\frac {1}{4(3-2{\sqrt {2}})}}\right)^{n}{\frac {\ln ^{3}(n)}{n^{2}}}\simeq 1.46^{n}{\frac {\ln ^{3}(n)}{n^{2}}}$

upper and lower bounds for number of lambdas in a term of size n

Let $S(n,k)$ be the number of lambda term of size n containing more than ${\frac {kn}{ln(n)}}$ lambdas. We search $k$ such that $\lim _{n\rightarrow +\infty }{\frac {S(n,k)}{L_{n}}}=0$.

Using the previous notation, we may write $S_{n}\leq \sum _{p\geq {\frac {kn}{ln(n)}}}UB(n,p)$. We observed that $UB(n,p)$ is decreasing in $p$ if $p>{\frac {n+1}{W(e(n+1))}}$.

Then, we have $W(e(n+1))\geq \ln(e(n+1))-\ln(\ln(e(n+1)))$. Therefore, if ${\frac {kn}{ln(n)}}>{\frac {n+1}{\ln(e(n+1))-\ln(\ln(e(n+1)))}}$ (i), we have

$S(n,k)\leq M(n)\left({\frac {kn}{ln(n)}}\right)^{n+1-{\frac {kn}{ln(n)}}}$

Then, (i) is equivalent to ${\frac {kn}{n+1}}>{\frac {ln(n)}{\ln(e(n+1))-\ln(\ln(e(n+1)))}}$ which is true for $n$ large enough if $k>1$ because $\lim _{n\rightarrow +\infty }{\frac {ln(n)}{\ln(e(n+1))-\ln(\ln(e(n+1)))}}=1$.

Using our lower bound for $L_{n}$, we find

${\frac {S(n,k)}{L_{n}}}\leq {\frac {M(n)\left({\frac {kn}{ln(n)}}\right)^{n+1-{\frac {kn}{ln(n)}}}}{{\frac {\sqrt {n}}{\ln ^{3}(n)}}\left({\frac {4n}{\ln(n)}}\right)^{n-{\frac {n}{\ln(n)}}}}}$

We now use the fact that $M(n)\sim \left({\frac {1}{3-2{\sqrt {2}}}}\right)^{n}{\frac {1}{n^{\frac {3}{2}}}}$, for $n$ large enough, we have (we introduce an extra log to compensate for the equivalent)

${\frac {S(n,k)}{L_{n}}}\leq {\frac {\ln ^{4}(n)\left({\frac {1}{3-2{\sqrt {2}}}}\right)^{n}\left({\frac {kn}{ln(n)}}\right)^{n+1-{\frac {kn}{ln(n)}}}}{n^{2}\left({\frac {4n}{\ln(n)}}\right)^{n-{\frac {n}{\ln(n)}}}}}$

We get a simpler upper bound by using the $n^{2}$ to compensate for the $+1$ exponent and the remaining $k{\frac {\ln ^{4}(n)}{\ln(n)}}$, which gives:

${\frac {S(n,k)}{L_{n}}}\leq {\frac {\left({\frac {1}{3-2{\sqrt {2}}}}\right)^{n}\left({\frac {kn}{ln(n)}}\right)^{n-{\frac {kn}{ln(n)}}}}{\left({\frac {4n}{\ln(n)}}\right)^{n-{\frac {n}{\ln(n)}}}}}=\left({\frac {k}{4(3-2{\sqrt {2}})}}\right)^{n}\left({\frac {kn}{ln(n)}}\right)^{\frac {-kn}{\ln(n)}}\left({\frac {4n}{ln(n)}}\right)^{\frac {n}{\ln(n)}}$

Let us remark that $\left({\frac {kn}{ln(n)}}\right)^{\frac {-kn}{\ln(n)}}=e^{-kn}\left({\frac {k}{ln(n)}}\right)^{\frac {-kn}{\ln(n)}}$ and $\left({\frac {4n}{ln(n)}}\right)^{\frac {n}{\ln(n)}}=e^{n}\left({\frac {4}{ln(n)}}\right)^{\frac {n}{\ln(n)}}$ .

Thus we have:

${\frac {S(n,k)}{L_{n}}}\leq \left({\frac {ke^{1-k}}{4(3-2{\sqrt {2}})}}\right)^{n}\left({\frac {4k^{-k}}{ln^{2}(n)}}\right)^{\frac {n}{\ln(n)}}$

This means that ${\frac {S(n,k)}{L_{n}}}$ converges toward zero if ${\frac {ke^{1-k}}{4(3-2{\sqrt {2}})}}<1$. $ke^{1-k}$ reaches its maximum $1$ in $k=1$ and $0<4(3-2{\sqrt {2}})<1$ This means that $ke^{1-k}=4(3-2{\sqrt {2}})$ has two solutions, one for $k>1$ the other for $k<1$. Because of (i) we need to keep the first solution. It is easy to see that the first solution is smaller than 3 because $3e^{1-3}<3{\frac {4}{25}}<4(3-2{\sqrt {2}})$.

Corollary. Random lambda term of size n contains asymptotically no more then ${\frac {3n}{ln(n)}}$ lambdas.

In the same way, we can consider lambda-terms with less than ${\frac {kn}{ln(n)}}$ and redo exactly the same computation, but replacing (i) by ${\frac {kn}{ln(n)}}<{\frac {n+1}{\ln(e(n+1))}}$ (ii). Then we have to take $k$ smaller than the other solution of the equation, and if it easy to see that $k<{\frac {1}{3}}$ works.

Corollary. Random lambda term of size n contains asymptotically no less then ${\frac {n}{3ln(n)}}$ lambdas.

Once we know this we can improve the upper bound.

Let Ll be $\Lambda \setminus Ls$. In a term from Ll the proportion between unary and binary nodes is smaller then ${\frac {3}{ln(n)}}$ which is far from typical proportion in unary-binary trees which tends to some nonzero constant. Rough estimation gives

$Ll_{n}\leq C(n){n \choose {\frac {3}{ln(n)}}}((1+\epsilon ){\frac {n}{ln(n)}})^{n}$

where C(n) corresponds to the binary structure, ${n \choose {\frac {3}{ln(n)}}}$ to the possible distribtions of lambdas in binary structure and $((1+\epsilon ){\frac {n}{ln(n)}})^{n}$ to the possibilities of bindings (one can optimal number of unary nodes involving Lambert's function to get rid of epsilon here). The crucial observation now is that ${n \choose {\frac {3}{ln(n)}}}$ is subexponential.

Comparing this upper bound with $LB(n,{\frac {n}{ln(n)}})$ we would obtain that the asymptotic ratio between upper and lower bound is subexponential.

I think it has some serious consequences. In particular it seems that in a random lambda term almost all lambdas lie on one path.

Proposition. \label{prop:typical_depth} There exists a function $f\in \Omega \left({\frac {n}{\log(n)}}\right)$ such that the set of terms t having a $\lambda$-depth greater than $f(size(t))$ has density 1.

Lambdas in head position

Theorem. \label{th:starting_lambdas} Let $g\in o\left({\frac {n}{\log(n)}}\right)$. The set $\Lambda _{g}$ of terms t starting with less than $g(size(t))$ lambdas has density 0.

Proof. By proposition \ref{prop:typical_depth}, for some function f such that $g\in o(f)$, we can restrict to the set $\Gamma _{f}$ of terms t having $\lambda$-depth at least $f(size(t))$ (because $\Gamma _{f}$ has density 1). To prove the theorem it is sufficient to exhibit a one-to-one function $\phi$ from $\Lambda _{g}\cap \Gamma _{f}$ into $\Gamma _{f}$ whose image set has density 0. We now define $\phi$ by describing $\phi (t)$ where t is an arbitrary term of size n belonging to $\Lambda _{g}\cap \Gamma _{f}$. By hypothesis, the term t starts with a chain of p $\lambda$-nodes, where $p\leq g(n)$. So $t=\lambda x_{1}\cdots \lambda x_{p}.A$ where A is a term starting by an application and containing at least one $\lambda$ (for n large enough). Now let B be the maximal purely applicative prefix of A. Precisely, B is the maximal binary tree whose leaves are either special leaves or variables among $x_{1},\ldots ,x_{p}$ and such that $A=B(t_{1},\ldots ,t_{k})$ where $t_{1},\ldots ,t_{k}$ are terms starting with a lambda, and $B(t_{1},\ldots ,t_{k})$ denotes the term obtained by replacing successive special leaves of B by terms $t_{1},\ldots ,t_{k}$ respectively. By hypothesis on term t, we have $k\geq 1$. Let $t'_{1},\ldots ,t'_{k}$ denote the terms obtained from $t_{1},\ldots ,t_{k}$ by removing the leading lambda. Consider the term $T=\lambda x_{1}\cdots \lambda x_{p}.(t'_{1}(t'_{2}(\cdots (t'_{k-1}t'_{k})\cdots )$ which is of size $n-1-b$, where b is the number of application nodes in B. Finally, let $U_{b,f(n)}$ be the set of purely applicative terms of size b whose variables are chosen among a set of size $f(n)$. Consider the leftmost deepmost lambda of term T (leftmost among deepmost), and let $\lambda y.C$ denote the term rooted at this position. For any $u\in U_{b,f(n)}$, we define the term $T(u)$ by subsituting $\lambda y.C$ with $\lambda y.(u.C)$ in T and binding all variables of u according to their name to lambda above u. Firstly, $T(u)$ is a well-defined closed term because the insertion of u occurs at depth at least $f(n)$ and u has at most $f(n)$ different variables. Secondly, $T(u)$ has size exactly n.

The set $X_{b,p}$ of binary trees with b internal nodes and leaves labelled either 'special' or by a variable among $x_{1},\ldots ,x_{p}$ has cardinality $(p+1)^{b+1}C(b)$ (where $C(b)$ denotes the Catalan number). Besides, the set $U_{b,f(n)}$ has carinality $f(n)^{b+1}C(b)$. Therefore, since $p\leq g(n)$ and $g\in o(f)$, there exists a function $\rho$ with $\rho (n)\rightarrow \infty$ and a function $\Psi _{b,p,n}$ from $X_{b,p}$ to subsets of $U_{b,f(n)}$ such that:

• for each $x\in X_{b,p}$, $\Psi _{b,p,n}(x)$ contains $\rho (n)$ elements;
• for n large enough, $x\not =x'\Rightarrow \Psi _{b,p,n}(x)\cap \Psi _{b,p,n}(x')=\emptyset$.

What we have established so far is the following: to term $t\in \Lambda _{g}\cap \Gamma _{f}$ we assosiate injectively the 4-uple $(b,p,n,B,T)$; then, if u is the first element of $\Psi _{b,p,n}(B)$ in some arbitrary (but fixed) order, we assotiate to $(b,p,n,B,T)$ the term $\phi (t)=T(u)$. By hypothesis on function $\Psi _{b,p,n}$ defined above, the function $\phi :t\mapsto \phi (t)$ is injective for n large enough. Moreover, we have $\left|\phi (\Gamma _{f}\cap \Lambda _{g}\cap L_{n})\right|\leq {\frac {|\Gamma _{f}\cap L_{n}|}{\rho (n)}}$ so the image set of $\phi$ has density 0 and the theorem follows.

Head lambdas bind "many" occurrences of the corresponding variables

Theorem. \label{th:biding_lambdas} Let g and h be two functions belonging to $o\left({\frac {n}{\log(n)}}\right)$ and let $\Lambda _{g,h}$ be the set of terms t where the total number of occurrences of variables bound to one of the $g(size(t))$ head lambdas is less than $h(size(t))$. Then $\Lambda _{g,h}$ has density 0.

Remark. The proof of this theorem uses arguments similar to those used in proof of theorem 'starting lambdas'. But is this theorem useful ?

Yes, since it is used in the next theorem. However, it is enough to show that for fixed integers k and k' each of k head lambdas binds at least k' variables.

pdf

tex

every fixed closed term (including the identity !) does not appear in a random term (in fact we have much more than that)

Let $\Lambda ^{t_{0}}$ denote the set of lambda terms which have $t_{0}$ as a subterm and let $T_{k}$ be the set of those lambda trees in which the number of unbounded leaves (occurrences of free variables) is equal to $k$.

Theorem

For any integers $k$ and $k'\geq k+1$ and for any term $t_{0}\in T_{k}$ of length $k'$ the following holds:

$\lim _{n\to \infty }{\frac {\#(\Lambda _{n}\cap \Lambda ^{t_{0}})}{\#\Lambda _{n}}}=0.$

Proof

Fix $k$ and $k'\geq k+1$. Let $t_{0}$ be a lambda tree of size $k'$ with exactly $k$ occurrences of free variables, denoted $x_{1},\ldots ,x_{k}$ (not necessarily distinct). Since there are at most $k'-k+1$ occurrences of lambdas and at most $k'+1$ leaves in $t_{0}$, there are at most

$K=M(k')(k'+1)^{k'+1}$

such trees and we can enumerate them in a fixed way. Let $m$ be the number of $t_{0}$. The tree $t_{0}$ contains at least one occurrence of lambda, otherwise it would either contain more free variables or would be of a bigger size.

Let $n$ be an integer satisfying ${\sqrt {\frac {n}{\ln(n)}}}\geq K$.

We will construct an injective function $f\colon \Lambda _{n}\cap \Lambda ^{t_{0}}\to \Lambda _{n}$ such that its image is of density 0 in $\Lambda _{n}$.

Let $t$ be a term of size $n$ with $t_{0}$ as its subterm. Let us consider the tree $T$ which is built from the tree $t$ by adding an additional unary node (labelled with $\lambda x$) at depth $m$. Next, let $T'$ be the tree obtained by replacing the subtree $t_{0}$ in $T$ by the tree $t_{1}=UB$, where $U$ is a binary tree of size $k'-k-1$ such that $U=x(x(\ldots (xx)\ldots ))$ and $B=x_{1}(x_{2}(\ldots (x_{k-1}x_{k})\ldots ))$, so the size of $B$ is equal to $k-1$. Thus, the size of $T'$ is equal to $n$. The variable $x$ is bound by the $m$-th lambda in the tree $T'$. Let us take $f(t)=T'$. Since $m$ is the number of the tree $t_{0}$, the function $f$ is injective.

By Theorem \ref{?}, each of $K$ head lambdas in a random tree of size $n$ binds more than $k'$ variables. Trees from the image $f(\Lambda _{n}\cap \Lambda ^{t_{0}})$ do not have this property, since the $m$-th lmabda binds only $k'$ variables. Thus, those trees are negligible among all trees of size $n$.

Corollary

Let $t_{0}$ be a closed lambda term. Then the density of $\Lambda ^{t_{0}}$ is equal to $0$.

Corollary

Let $t_{0}$ be a lambda term in which there are at least two occurrences of lambdas. Then the density of $\Lambda ^{t_{0}}$ is equal to $0$.

comment : so different situation in combinatory logic and lambda calculus ; the coding uses a big size so need to count variables in a different way

Random lambda terms are strongly normalizable

Sketch of the proof pdf tex

Jakub says: I think that it might be possible to simplify the proof, by using other argument for the proof that the density of the image of encoding equals 0.

Chambéry says: we checked the proof and we are convinced by the result. Since Jakub made an important step for the second time, we suggest to explicitely acknowledge his contribution in the paper (for instance, by naming some key lemma/theorems "Jakub's lemma/theorem"). Here are the points to fix in the proof:

• as René said, the definition of "dangerous redex" must be changed to allow a single occurrence of x in A (and a proof sketch of why "no dangerous redex" implies SN must be added)
• version 1 of encoding is sufficient
• in the encoding, there is some substituion of variable to do in C (to have a closed term at the end, and also to ensure that the decoding is unambiguous)
• to complete the proof with the new definition of "dangerous redex" we need the result saying that terms containing identity have density 0 (as said by Jakub by e-mail). We don't see how to conclude without that. However, we have to further check if there is no shorter proof...

Experiments

results of the experiments we have done

some experiments that have to be done : e.g. density of terms having $\lambda x.y$ or big Omega pattern ...

to be done

Upper and lower bounds for $L_{n}$ with other size for variables especially one, binary with fixed size

Open questions and Future work

.....