Nuprl Definition : count_unrolls

count_unrolls(t;k) ==
  fix((λcount_unrolls,t,k. (if t is stopped at g,f then
                           eval k' = k + 1 in
                           count_unrolls (g (f stop(f))) k'
                           otherwise t.<t, k>))) 
  t 
  k


Definitions occuring in Statement :  callbyvalue: callbyvalue,  apply: f a,  fix: fix(F),  lambda: λx.A[x],  pair: <a, b>,  add: n + m,  natural_number: $n
Definitions occuring in definition :  fix: fix(F),  lambda: λx.A[x],  callbyvalue: callbyvalue,  add: n + m,  natural_number: $n,  apply: f a,  pair: <a, b>
FDL editor aliases :  count_unrolls
Latex:
count\_unrolls(t;k)  ==
    fix((\mlambda{}count$_{unrolls}$,t,k.  (if  t  is  stopped  at  g,f  then
                                                    eval  k'  =  k  +  1  in
                                                    count$_{unrolls}$  (g  (f  stop(f)))  k'
                                                    otherwise  t.<t,  k>))) 
    t 
    k


Date html generated: 2016_05_15-PM-02_15_55
Last ObjectModification: 2015_09_23-AM-07_38_19

Theory : untyped!computation


Home Index