Nuprl Definition : iterate_functor
iterate_functor(I;x,y.R[x; y];T.F[T];a)==r F[⋂b:{x:I| R[a; x]} . iterate_functor(I;x,y.R[x; y];T.F[T];b)]
iterate_functor(I;x,y.R[x; y];T.F[T];a) == fix((λiterate_functor,a. F[⋂b:{x:I| R[a; x]} . (iterate_functor b)])) a
Definitions occuring in Statement :
set: {x:A| B[x]} ,
apply: f a,
fix: fix(F),
lambda: λx.A[x],
isect: ⋂x:A. B[x]
Definitions occuring in definition :
fix: fix(F),
lambda: λx.A[x],
isect: ⋂x:A. B[x],
set: {x:A| B[x]} ,
apply: f a
FDL editor aliases :
iterate_functor
Latex:
iterate\_functor(I;x,y.R[x; y];T.F[T];a)
==r F[\mcap{}b:\{x:I| R[a; x]\} . iterate\_functor(I;x,y.R[x; y];T.F[T];b)]
Latex:
iterate\_functor(I;x,y.R[x; y];T.F[T];a) ==
fix((\mlambda{}iterate$_{functor}$,a. F[\mcap{}b:\{x:I| R[a; x]\} . (iterate$_{func\000Ctor}$ b)])) a
Date html generated:
2016_05_14-AM-06_11_50
Last ObjectModification:
2015_09_22-PM-05_46_57
Theory : co-recursion
Home
Index