« Lambda counting » : différence entre les versions

De Wiki du LAMA (UMR 5127)
Aller à la navigation Aller à la recherche
Ligne 129 : Ligne 129 :
<center><math>UB(n,k) = M(n,n-k+1) k^{n-k+1}</math></center>
<center><math>UB(n,k) = M(n,n-k+1) k^{n-k+1}</math></center>


If we sum this for all possible <math>k</math>, we get the following upper bound for <math>L_n</math>:
If we sum this for all possible <math>k</math> and get an upper bound of <math>k^{n-k+1}</math> using Lambert function as for the lower bound, we get the following upper bound for <math>L_n</math>:


<center><math>\#(L_n) \leq M(n) \left(\frac{n+1}{W(e(n+1))}\right)^{n-\frac{n+1}{W(e(n+1))} + 1}</math></center>
<center><math>\#(L_n) \leq M(n) \left(\frac{n+1}{W(e(n+1))}\right)^{n-\frac{n+1}{W(e(n+1))} + 1}</math></center>

Version du 20 octobre 2008 à 12:01

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: which is obtained using Strirling formula. However, using stirling series: , we get that for we have

Thus, using this and , we have:

for all but also for .

Motzkin numbers

Let us define the number of unary-binary trees with inner nodes and leafs. We get

Then, by summing we define the number of unary-binary trees with inner nodes and give an equivalent:

Lambert W function

The Lambert function is defined by the equation which has a unique solution in .

For , we have 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:

Indeed, if we define , we have and therefore, newton's method from gives a point at position:

Finally, we show that for , we have:

Indeed, for , we have , which implies and therefore .

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:

with

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 and taking large enough, we have the following lowerbound:

We now compute an upper bound for the number of lambda-terms of size with exactly lambdas (that is with leaves using the Motzkin numbers and allowing any lambda to bind any variable (regardless of the real scope):

If we sum this for all possible and get an upper bound of 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) \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 (NEED FURTHER CHECKING) 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 \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}}

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

.....