Nuprl Definition : W-rec
W-rec(a,f,r.F[a; f; r];w)==r let a,f = w in F[a; f; λb.W-rec(a,f,r.F[a; f; r];f b)]
W-rec(a,f,r.F[a; f; r];w) == fix((λW-rec,w. let a,f = w in F[a; f; λb.(W-rec (f b))])) w
Definitions occuring in Statement :
apply: f a,
fix: fix(F),
lambda: λx.A[x],
spread: spread def
Definitions occuring in definition :
fix: fix(F),
spread: spread def,
lambda: λx.A[x],
apply: f a
FDL editor aliases :
W-rec
Latex:
W-rec(a,f,r.F[a; f; r];w)==r let a,f = w in F[a; f; \mlambda{}b.W-rec(a,f,r.F[a; f; r];f b)]
Latex:
W-rec(a,f,r.F[a; f; r];w) == fix((\mlambda{}W-rec,w. let a,f = w in F[a; f; \mlambda{}b.(W-rec (f b))])) w
Date html generated:
2016_05_14-AM-06_15_40
Last ObjectModification:
2015_09_22-PM-05_47_18
Theory : co-recursion
Home
Index