« Lambda counting » : différence entre les versions

De Wiki du LAMA (UMR 5127)
Aller à la navigation Aller à la recherche
Aucun résumé des modifications
Aucun résumé des modifications
Ligne 1 : Ligne 1 :
==Introduction==
==Introduction==


The question of our interest is the following: among programs, what is the probability of having a fixed property.
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