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
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:
Échec de l’analyse (fonction inconnue « \begin{array} »): {\displaystyle \begin{array}{lcl}A - \frac{f(A) - x}{f'(A)} &=& A + x \frac{\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} \end{array}}
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:
NOT TRUE : NEEDS FIXING !!!
Thus, we get the following lowerbound for :
To simplify, using the fact that and taking 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 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
.....