« Lambda counting » : différence entre les versions

De Wiki du LAMA (UMR 5127)
Aller à la navigation Aller à la recherche
Ligne 79 : Ligne 79 :
== Generality on lambda calculus ==
== Generality on lambda calculus ==


what kind of distribution ?


\begin{definition}
we look only for densities,
The set $\lambda$ of lambda terms (or, simply, terms) is defined
by the following grammar


<math>t, u := Var \ \mid \ \lambda x.t \ \mid \ (t \ u)$$
for that we need size.


\end{definition}
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

To be able to define the notion of a {\it random} term we
have to define a distribution law on <math>\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.

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

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

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

- <math>size_1((t \ u))=size_1(t)+size_1(u)+1$
\end{definition}

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

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

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

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

- <math>size_0((t \ u))=size_0(t)+size_0(u)+1$
\end{definition}

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 <math>\lambda$ that occur, on the path
from the variable to the root, between the variable and the
<math>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 <math>n$ simply
is <math>n$ itself

- Use optimal binary notation, i.e. the size of the index <math>n$
is <math>log_2(n)$ i.e. the logarithm of <math>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 ==
== generating functions ==

Version du 20 octobre 2008 à 13:00

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

\begin{definition} The set $\lambda$ of lambda terms (or, simply, terms) is defined by the following grammar

Échec de l’analyse (erreur de syntaxe): {\displaystyle t, u := Var \ \mid \ \lambda x.t \ \mid \ (t \ u)$$ \end{definition} To be able to define the notion of a {\it random} term we have to define a distribution law on <math>\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. \begin{definition} The size (denoted as <math>size_1(t)$) of a term <math>t$ is defined by the following rules. - <math>size_1(t)=1$ if <math>t$ is a variable. - <math>size_1(\lambda x.t)=size_1(t)+1$ - <math>size_1((t \ u))=size_1(t)+size_1(u)+1$ \end{definition} In the rest of the paper we will use another definition (denoted as <math>size_0(t)$) which is similar but gives simpler computations. We believe (but we have not yet checked the details) that, with <math>size_1$ we would have similar results. The computation, with <math>size_1$, of the upper and lower bounds of the number of terms of size <math>n$ will be done in section ?? \begin{definition} The size (denoted as <math>size_0(t)$) of a term <math>t$ is defined by the following rules. - <math>size_0(t)=1$ if <math>t$ is a variable. - <math>size_0(\lambda x.t)=size_0(t)+1$ - <math>size_0((t \ u))=size_0(t)+size_0(u)+1$ \end{definition} 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 <math>\lambda$ that occur, on the path from the variable to the root, between the variable and the <math>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 <math>n$ simply is <math>n$ itself - Use optimal binary notation, i.e. the size of the index <math>n$ is <math>log_2(n)$ i.e. the logarithm of <math>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 <math>L_n} )

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 :

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 lambdas in head position and number of lambdas in one path

Remark: (may be 4) can be done directly without 3))

each of the 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 or big Omega pattern ...

to be done

Upper and lower bounds for with other size for variables especially one, binary with fixed size

Open questions and Future work

.....