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