« Lambda counting » : différence entre les versions
Aucun résumé des modifications |
Aucun résumé des modifications |
||
Ligne 1 : | Ligne 1 : | ||
==Introduction== |
==Introduction== |
||
The question |
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 proerties : 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 densities, |
|||
for that we need size. different size for varibles: zero, one, debruijn indices in unary, binary, ... |
|||
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 |
Version du 17 octobre 2008 à 12:16
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 proerties : 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 densities,
for that we need size. different size for varibles: zero, one, debruijn indices in unary, binary, ...
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