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: É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 C(n) \sim \frac{4^n}{n^{3/2}\sqrt{\pi}}} which is obtained using Strirling formula. However, using stirling series: É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!=\sqrt{2\pi n}\left({n\over e}\right)^n \left( 1 +{1\over12n} +{1\over288n^2} -{139\over51840n^3} -{571\over2488320n^4} + \cdots \right) } , we get that 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\geq1} we have É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 \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 É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(\frac{n}{n+1}\right)^{n} > e^{-1}} , we have:

É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 C(n) = \frac{(2n)!}{(n+1)!n!} \geq \frac{36}{49\sqrt{\pi}} \frac{4^n}{(n+1)^\frac{3}{2}}} for all É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\geq1} but also 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=0} .

Motzkin numbers

Let us define É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 M(n,k)} the number of unary-binary trees with $n$ inner nodes 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 k} leafs. We get

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

Then, by summing we define É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 M(n)} the number of unary-binary trees with É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} inner nodes and give an equivalent:

É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 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 É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 W(x)} is defined by the equation É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 x = W(x) e ^ {W(x)} } which has a unique solution in $\mathbb {R}$.

For $x\geq e$, we have É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 \ln(x) - \ln(\ln(x)) \leq W(x) \leq \ln(x)} which implies 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 W(x) \sim \ln(x)} near $+\infty$. To prove this, it is enough to remark 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 (\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 É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 \ln(x) - \ln(\ln(x))} , we can find a better upper bound 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 W(x)} because É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 y \mapsto y e^y} is increasing and convex. This gives:

É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 \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 É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 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 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 É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 x\geq e} , we have:

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

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

É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 LB(n,k) = C(n-k) k^{n-k+1}}

And therefore, for $n>k$, using our lower bound 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 C(n)} 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 n + 1 \geq n - k + 1} , we get:

É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 LB(n,k) \geq K \frac{(4k)^{n-k+1}}{(n+1)^\frac{3}{2}}} with É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=\frac{36}{49\sqrt{\pi}}}

Now, 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, we define É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) = \left(4n\alpha\right)^{n(1-\alpha) + 1}} (so É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 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 É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) = f(\alpha) \left(-n\ln(4n\alpha) +\frac{n(1-\alpha) + 1}{\alpha}\right)} . Thus, $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 \frac{n+1}{n\alpha}e^{\frac{n+1}{n\alpha}}\geq 4e(n+1)} . The Lambert function begin increasing 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 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{n+1}{nW(4e(n+1))}} . 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{n+1}{nW(4e(n+1))}} .

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+1}{W(4e(n+1))}} 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+1}{W(4e(n+1))}} 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+1}{\ln(4e(n+1))}} . Indeed, using our inequalities on Lambert W function, we have:

É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+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 É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+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 É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{\sqrt{n}}{\ln^3(n)}\left(\frac{4n}{\ln(n)}\right)^{n-\frac{n}{\ln(n)}}}

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

É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 UB(n,k) = M(n,n-k+1) k^{n-k+1}}

If we sum this for all possible É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} and get an upper bound of É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^{n-k+1}} using Lambert function as for the lower bound, we get the following upper bound 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) \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):

É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(\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 É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

.....