« Lambda counting » : différence entre les versions

De Wiki du LAMA (UMR 5127)
Aller à la navigation Aller à la recherche
Ligne 61 : Ligne 61 :
== to be done ==
== to be done ==


Upper and lower bounds for L_n with other size for variables especially one, binary with fixed size
Upper and lower bounds for <math>L_n</math> with other size for variables especially one, binary with fixed size


== Open questions and Future work ==
== Open questions and Future work ==

Version du 17 octobre 2008 à 13: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 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

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

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

.....