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

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

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

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+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 )}$ (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 É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 \alpha \leq \frac{1}{W(4en)}} . Therefore, É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 f(\alpha)} reaches a maximum for É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 \alpha = \frac{1}{W(4en)}} .

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

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

Thus, we get the following lowerbound for É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 L_n} :

É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 \#(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)) - 1)}{\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 É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 \lim_{n\to +\infty}\left(\frac{\ln(n)}{\ln(4en)}\right)^n = 0} and taking É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 n} large enough, we have the following lowerbound:

É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 \#(L_n) \geq \frac{1}{\sqrt{n}\ln^2(n)}\left(\frac{4n}{\ln(n)}\right)^{n-\frac{n}{\ln(n)}}}

at least É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 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 É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 \lambda x.y} or big Omega pattern ...

to be done

Upper and lower bounds for É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 L_n} with other size for variables especially one, binary with fixed size

Open questions and Future work

.....