Nuprl Definition : final-iterate
final-iterate(f;x) == fix((λfinal-iterate,x. if can-apply(f;x) then final-iterate do-apply(f;x) else x fi )) x
Definitions occuring in Statement :
do-apply: do-apply(f;x),
can-apply: can-apply(f;x),
ifthenelse: if b then t else f fi ,
apply: f a,
fix: fix(F),
lambda: λx.A[x]
Definitions occuring in definition :
fix: fix(F),
lambda: λx.A[x],
ifthenelse: if b then t else f fi ,
can-apply: can-apply(f;x),
apply: f a,
do-apply: do-apply(f;x)
FDL editor aliases :
final-iterate
Latex:
final-iterate(f;x) ==
fix((\mlambda{}final-iterate,x. if can-apply(f;x) then final-iterate do-apply(f;x) else x fi )) x
Date html generated:
2016_05_15-PM-04_34_37
Last ObjectModification:
2015_09_23-AM-07_49_20
Theory : general
Home
Index