Lambda counting

Introduction

The question is: among programs, what is the probability of having a fixed property.

what kind of program : turing machines, cellular automata, combinatory logic, lambda calculus

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

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

• $M(n,k)$

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:

Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle \begin{array}{lcl} A - \frac{f(A) - x}{f'(A)} &=& A + x \frac{\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} \end{array}}

combinatory logic

results on combinatory logic

Generality on lambda calculus

what kind of distribution ?

we look only for densities,

for that we need size.

different size for variables: zero, one, binary with optimal size, binary with fixed size, debruijn indices in unary...

we concentrate on the simple one : variable of size zero (probably similar for size one ) more later for other size

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

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}}{(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 )}$ (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 )=nf(\alpha )\left(-\ln(4n\alpha )+{\frac {1-\alpha }{\alpha }}\right)$. Thus, $f'(\alpha )\geq 0$ is equivalent to ${\frac {1}{\alpha }}e^{\frac {1}{\alpha }}\geq 4en$. The Lambert function begin increasing this means that $f'(\alpha )\geq 0$ is equivalent to $\alpha \leq {\frac {1}{W(4en)}}$. Therefore, $f(\alpha )$ reaches a maximum for $\alpha ={\frac {1}{W(4en)}}$.

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

NOT TRUE : NEEDS FIXING !!! ${\frac {n}{W(4en)}}-{\frac {n}{\ln(4en)}}={\frac {n(\ln(4en)-W(4en))}{W(4en)\ln(4en)}}\geq {\frac {n\ln(\ln(4en))}{\ln ^{2}(4en)}}$

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}{\ln(4en)}}\rceil }^{\lfloor {\frac {n}{W(4en)}}\rfloor }K{\frac {(4k)^{n-k}}{(n+1)^{\frac {3}{2}}}}\geq K\left\lfloor {\frac {n\ln(\ln(4en))}{\ln ^{2}(4en)}}\right\rfloor {\frac {\left({\frac {4n}{\ln(4en)}}\right)^{n-{\frac {n}{\ln(4en)}}}}{(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 {1}{{\sqrt {n}}\ln ^{2}(n)}}\left({\frac {4n}{\ln(n)}}\right)^{n-{\frac {n}{\ln(n)}}}$

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

.....