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

Lambert function, Catalan and Motzkin 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 (É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}}} ).
• É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)} : Motzkin 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 W(\alpha)} : Lambert W function.

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 É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 $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 $n$ starting with $k$ lambdas and having no other lambda below. This means that the lower part of the term is a binary tree of size $n-k$ with $k$ possibility for each leaf. Therefore we have:

$LB(n,k)=C(n-k)k^{n-k}$

From the equivalent, we have for $n$ big enough:

$C(n)\geq 4^{n}$

And therefore

$LB(n,k)\geq 4^{n}k^{n-k}$

Now, for $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) = 4^n (\alpha n)^{n(1-\alpha)}} and look for the maximum of this function.

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

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

.....