Nuprl Definition : restart-function

restart-function(f) ==  fix((λR,n. if 0 <z n then <R (n - 1), {n}> else f 0 fi ))


Definitions occuring in Statement :  single-bag: {x},  ifthenelse: if b then t else f fi ,  lt_int: i <z j,  apply: f a,  fix: fix(F),  lambda: λx.A[x],  pair: <a, b>,  subtract: n - m,  natural_number: $n
Definitions occuring in definition :  fix: fix(F),  lambda: λx.A[x],  ifthenelse: if b then t else f fi ,  lt_int: i <z j,  pair: <a, b>,  subtract: n - m,  single-bag: {x},  apply: f a,  natural_number: $n
FDL editor aliases :  restart-function
Latex:
restart-function(f)  ==    fix((\mlambda{}R,n.  if  0  <z  n  then  <R  (n  -  1),  \{n\}>  else  f  0  fi  ))


Date html generated: 2016_05_15-PM-10_11_52
Last ObjectModification: 2015_09_23-AM-08_22_38

Theory : eval!all


Home Index