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

• É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)}  : 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: $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 É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 $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-{\frac {x\ln(\ln(x))}{x}}\leq x\leq x\ln(x)=\ln(x)e^{\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}$

And therefore, for $n>k$, using our lower bound for $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}}{(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 $f(\alpha )=\left(4n\alpha \right)^{n(1-\alpha )}$ (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) = n f(\alpha) \left(-\ln(4n\alpha) +\frac{1-\alpha}{\alpha}\right)} . Thus, É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 \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 $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))}{\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 ${\frac {n}{\ln(4en)}}$. 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}{W(4en)}-\frac{n}{\ln(4en)} = \frac{n (\ln(4en) - W(4en))}{W(4en)\ln(4en)} \leq \frac{n \ln(\ln(4en))}{\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))}{\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

.....