« Lambda counting » : différence entre les versions

De Wiki du LAMA (UMR 5127)
Aller à la navigation Aller à la recherche
Ligne 82 : Ligne 82 :




⚫
definition The set <math>\lambda</math> of lambda terms (or,

⚫
definition The set <math>\lambda<\math> of lambda terms (or,
simply, terms) is defined by the following grammar
simply, terms) is defined by the following grammar


<math>t, u := Var \ \mid \ \lambda x.t \ \mid \ (t \ u)<\math>
<math>t, u := Var \ \mid \ \lambda x.t \ \mid \ (t \ u)</math>


definition
definition
Ligne 93 : Ligne 92 :


To be able to define the notion of a {\it random} term we
To be able to define the notion of a {\it random} term we
have to define a distribution law on <math>\Lambda<\math>. There are many
have to define a distribution law on <math>\Lambda</math>. There are many
possibilities for that. We choose here the simplest one. Note that this is the one for which, at least at present, we are
possibilities for that. We choose here the simplest one. Note that this is the one for which, at least at present, we are
able to prove some results. It is based on densities. For that we
able to prove some results. It is based on densities. For that we
Ligne 102 : Ligne 101 :


definition
definition
The size (denoted as <math>size_1(t)<\math>) of a term <math>t<\math> is defined by the following
The size (denoted as <math>size_1(t)</math>) of a term <math>t</math> is defined by the following
rules.
rules.


- <math>size_1(t)=1<\math> if <math>t<\math> is a variable.
- <math>size_1(t)=1</math> if <math>t</math> is a variable.


- <math>size_1(\lambda x.t)=size_1(t)+1<\math>
- <math>size_1(\lambda x.t)=size_1(t)+1</math>


- <math>size_1((t \ u))=size_1(t)+size_1(u)+1<\math>
- <math>size_1((t \ u))=size_1(t)+size_1(u)+1</math>




In the rest of the paper we will use another definition (denoted
In the rest of the paper we will use another definition (denoted
as <math>size_0(t)<\math>)
as <math>size_0(t)</math>)
which is similar but gives simpler computations.
which is similar but gives simpler computations.
We believe (but we have not yet checked the details) that, with
We believe (but we have not yet checked the details) that, with
<math>size_1<\math> we would have similar results. The
<math>size_1</math> we would have similar results. The
computation, with <math>size_1<\math>, of the upper and lower
computation, with <math>size_1</math>, of the upper and lower
bounds of the number of terms of size <math>n<\math> will be done
bounds of the number of terms of size <math>n</math> will be done
in section ??
in section ??


definition
definition
The size (denoted as <math>size_0(t)<\math>) of a term <math>t<\math> is defined by the following
The size (denoted as <math>size_0(t)</math>) of a term <math>t</math> is defined by the following
rules.
rules.


- <math>size_0(t)=1<\math> if <math>t<\math> is a variable.
- <math>size_0(t)=1</math> if <math>t</math> is a variable.


- <math>size_0(\lambda x.t)=size_0(t)+1<\math>
- <math>size_0(\lambda x.t)=size_0(t)+1</math>


- <math>size_0((t \ u))=size_0(t)+size_0(u)+1<\math>
- <math>size_0((t \ u))=size_0(t)+size_0(u)+1</math>




Ligne 137 : Ligne 136 :
The usual way to implement this coding is to replace the names of
The usual way to implement this coding is to replace the names of
variables by their so called de Bruijn indices: a variable is
variables by their so called de Bruijn indices: a variable is
replaced by the number of <math>\lambda<\math> that occur, on the
replaced by the number of <math>\lambda</math> that occur, on the
path from the variable to the root, between the variable and the
path from the variable to the root, between the variable and the
<math>lambda<\math> that binds it. Note that, in this case,
<math>lambda</math> that binds it. Note that, in this case,
different occurrences of the same variable may be represented by
different occurrences of the same variable may be represented by
different indices.
different indices.
Ligne 147 : Ligne 146 :
following ways
following ways


- Use unary notation, i.e. the size of the index <math>n<\math>
- Use unary notation, i.e. the size of the index <math>n</math>
simply is <math>n<\math> itself
simply is <math>n</math> itself


- Use optimal binary notation, i.e. the size of the index
- Use optimal binary notation, i.e. the size of the index
<math>n<\math> is <math>log_2(n)<\math> i.e. the logarithm of
<math>n</math> is <math>log_2(n)</math> i.e. the logarithm of
<math>n<\math> in base 2.
<math>n</math> in base 2.


- Use uniform binary notation, i.e. the size of an index is the
- Use uniform binary notation, i.e. the size of an index is the
logarithm, in base 2, of the number of leaves of the term.
logarithm, in base 2, of the number of leaves of the term.





Version du 20 octobre 2008 à 13:11

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: É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

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

É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) = \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 É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 É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 É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 +\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 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 É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(y) = y e^y} , 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'(y)=(1+y)e^y} and therefore, newton's method from 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 , 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 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 É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) + 1 \geq \ln\ln(x)} .

combinatory logic

results on combinatory logic

Generality on lambda calculus

definition The set of lambda terms (or, simply, terms) is defined by the following grammar

É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 t, u := Var \ \mid \ \lambda x.t \ \mid \ (t \ u)}

definition


To be able to define the notion of a {\it random} term we 

have to define a distribution law on É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}
. There are many
possibilities for that. We choose here the simplest one. Note that this is the one for which, at least at present,  we are
able to prove some results. It is based on densities. For that we
first have to define the {\it size} of a term.

The usual
definition is the following.

definition 

The size (denoted as ) of a  term É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 t}
 is defined by the following
rules.

- É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 size_1(t)=1}
 if  is a variable.

- É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 size_1(\lambda x.t)=size_1(t)+1}

- É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 size_1((t \ u))=size_1(t)+size_1(u)+1}


In the rest of the paper we will use another definition (denoted as É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 size_0(t)} ) 

 which is similar but  gives simpler computations.

We believe (but we have not yet checked the details) that, 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 size_1} we would have similar results. The computation, 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 size_1} , of the upper and lower bounds of the number of terms of size will be done in section ?? 

definition
The size (denoted as É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 size_0(t)}
) of a  term É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 t}
 is defined by the following
rules.

- É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 size_0(t)=1}
 if É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 t}
 is a variable.

-

- É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 size_0((t \ u))=size_0(t)+size_0(u)+1}


These definitions of the size are, for the implementation point of view, not realistic because, in case a term has a lot of distinct variables, it is not realistic to use a single bit to code them. The usual way to implement this coding is to replace the names of variables by their so called de Bruijn indices: a variable is replaced by the number 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 \lambda} that occur, on the path from the variable to the root, between the variable and 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 lambda} that binds it. Note that, in this case, different occurrences of the same variable may be represented by different indices.

Choosing the way we code these de Bruijn indices gives different other ways of defining the size of a term. This can be done in the following ways

- Use unary notation, i.e. the size of the index É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} simply is É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} itself

- Use optimal binary notation, i.e. the size of the index É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} is É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 log_2(n)} i.e. the logarithm 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 n} in base 2.

- Use uniform binary notation, i.e. the size of an index is the logarithm, in base 2, of the number of leaves of the term.


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

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 É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)} 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} 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 É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} 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 É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} , 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, É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{n+1}{n\alpha}e^{\frac{n+1}{n\alpha}}\geq 4e(n+1)} . The Lambert function begin increasing this means that 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):

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

.....

Récupérée de « http://os-vps418.infomaniak.ch:1250/mediawiki/index.php?title=Lambda_counting&oldid=2653 »