« Lambda counting » : différence entre les versions
| Ligne 48 : | Ligne 48 : | ||
<center><math>(\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)} </math></center> |
<center><math>(\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)} </math></center> |
||
This is not precise enough for our purpose. Using one step of the Newton method from <math>\ln(x) - \ln(\ln(x))</math>, we can find a better upper bound for <math>W(x)</math> because <math>y \mapsto y e^y</math> is increasing |
This is not precise enough for our purpose. Using one step of the Newton method from <math>\ln(x) - \ln(\ln(x))</math>, we can find a better upper bound for <math>W(x)</math> because <math>y \mapsto y e^y</math> is increasing and convex. This gives: |
||
<center><math>\ln(x) - \ln(\ln(x)) \leq W(x) \leq \ln(x) - \ln(\ln(x)) + \frac{\ln(\ln(x))}{\ln(x) - \ln(\ln(x)) + 1}</math></center> |
<center><math>\ln(x) - \ln(\ln(x)) \leq W(x) \leq \ln(x) - \ln(\ln(x)) + \frac{\ln(\ln(x))}{\ln(x) - \ln(\ln(x)) + 1}</math></center> |
||
Version du 18 octobre 2008 à 17:42
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
- : 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:
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
- É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)}
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 which has a unique solution in É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 \mathbb{R}} .
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)} which implies that near . To prove this, it is enough to remark that
This is not precise enough for our purpose. Using one step of the Newton method from , we can find a better upper bound for because is increasing and convex. This gives:
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 )
our results
(the proof of result of section k needs the result of section (k-1))
Upper and lower bounds for
For the lower bound, we will first count the number of lambda-terms of size starting with lambdas and having no other lambda below. This means that the lower part of the term is a binary tree of size with possibility for each leaf. Therefore we have:
And therefore, for , using our lower bound for and , we get:
Now, for fixed, we define (so ) and look for the maximum of this function. We have . Thus, is equivalent to . The Lambert function begin increasing this means that is equivalent to . Therefore, reaches a maximum for .
This means that reaches its maximum for fixed when is near to which is likely not to be an integer. However, there are at least integer between and . Indeed, using our inequalities on Lambert W function, we have:
Thus, we get the following lowerbound for :
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:
upper and lower bounds for number of lambdas in a term of size n
Jakub's trik : at least 1 lambda in head position
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))
each of the É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)})} head lambdas really bind "many" occurrences of the variable
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
.....