Lambda counting

Introduction

what kind of properties : structural (for functional programs), behaviour (SN, weakly normalizable, ...

references to known results on : turing machines, cellular automata

we concentrate on combinatory logic, lambda calculus)

This paper adresses the following question. Having a (theoritical) programming language and a property of programs in that language. What is the probability that a random program satisfies the given property ? In particular, is it the case that almost every random program satisfies the desired property i.e. the probability is 1 ? This question has some known results for Turing machines and cellular automata. Some of them will be given in section ??.

In this introduction we consider that this notion of probabilty is, at least intuitively, sufficiently clear but, of course, this will have to be made precise.

We will consider this question for functional programming languages. For this kind of languages we can consider various properties. Some concern the structural of the program, some concern its behaviour.

The simplest such language is the lambda calculus. Some experiments have been done for it (see for example ...) which clearly indicates that, for example, almost every closed lambda term begins with a $\lambda$ but, as far as we know, there is no proved result of this form.

This paper proves some highly non trivial results of this form. In particular we show that almost every closed lambda term begins with "many" $\lambda$ (the precise meaning of this is given in theorem ??), that these $\lambda$ bound "many" occurences of the corresponding variables theorem ??) and that, given any fixed closed term, almost no $\lambda$-term has this term as a sub-term.

Our original motivation was to consider the property of being terminating. Is a random term strongly normalizable (SN for short)? This question is, at present, unsolved and the experiments we have done do not even give an idea of what the result should be. It is known that being SN is an undecidable question and it is thus not easy to count the number of SN terms of big size. It is clear that having $(\delta \ \delta )$ as a sub-term is a sufficient (but not necessary) condition for being non SN but as the experiments have shown (and as we have proved) almost no terms contains $(\delta \ \delta )$ and this is thus useless to have a rsult for non SN. On the opposite direction, it is known that, if a term t is not SN, then a pattern "looking like" $(\delta \ \delta )$ (the precise meaning will be given in sectioon ??) must appear in t but the experiments seem to show that almost every term possesses this pattern (actually, we have not bee

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 series: $n!={\sqrt {2\pi n}}\left({n \over e}\right)^{n}\left(1+{1 \over 12n}+{1 \over 288n^{2}}-{139 \over 51840n^{3}}-{571 \over 2488320n^{4}}+\cdots \right)$, we get that for $n\geq 1$ we have ${\sqrt {2\pi n}}\left({n \over e}\right)^{n}\leq n!\leq {\frac {7}{6}}{\sqrt {2\pi n}}\left({n \over e}\right)^{n}$

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

$C(n)={\frac {(2n)!}{(n+1)!n!}}\geq {\frac {36}{49{\sqrt {\pi }}}}{\frac {4^{n}}{(n+1)^{\frac {3}{2}}}}$ for all $n\geq 1$ but also for $n=0$.

Motzkin numbers

Let us define $M(n,k)$ the number of unary-binary trees with $n$ inner nodes and $k$ leafs. We get

$M(n,k)={\frac {(n+k-1)!}{(n-k+1)!(k-1)!k!}}$

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=0}^{n}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. This gives:

$\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

+ 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 T' in the other direction is not linear. As far as we know, there is no known bound on the size of T'(t) but it is not difficult to find exemples where size(T'(t)) is of order $size(t)^{3}$.

The point is that T' has to code the binding in some way and this takes place. It will be interesting to compare the size of T'(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 of size $n-k$ 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 {36}{49{\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(\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, using the fact that $\lim _{n\to +\infty }\left({\frac {\ln(n)}{\ln(4en)}}\right)^{n}=0$ and taking $n$ large enough, we have the following lowerbound:

$\#(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):

$\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}}}$

at least $o({\sqrt {n/\ln(n)}})$ lambdas in head position and number of lambdas in one path

Remark: (may be 4) can be done directly without 3))

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

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

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

.....