Lambda counting

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

section 1

results on combinatory logic

section 2 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 $L_{n}$)

our results

(the proof of result number k needs the result number (k-1))

1) upper and lower bounds for L_n

2) upper and lower bounds for number of lambdas in a term of size n

3) Jakub's trik : at least 1 lambda in head position

4) at least o(sqrt(n/Log(n))) lambdas in head position and number of lambdas in one path (may be 4) can be done directly without 3))

5) each of the o(sqrt(n/Log(n))) head lambdas really bind "many" occurrences of the variable

6) 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 /x.y or big Omega pattern ...

to be done

Upper and lower bounds for L_n with other size for variables

Open questions and Future work

.....