Nuprl Definition : pW-rec
let ind(p,a,f,G) = ind[p; a; f; G] in
letrec F(p,w) = let a,f=w in
ind(p,a,f,λb.F(C[p; a; b],f(b)) in
F(par;w)
==r let a,f = w
in ind[par; a; f; λb.let ind(p,a,f,G) = ind[p; a; f; G] in
letrec F(p,w) = let a,f=w in
ind(p,a,f,λb.F(C[p; a; b],f(b)) in
F(C[par; a; b];f b)]
let ind(p,a,f,G) = ind[p; a; f; G] in
letrec F(p,w) = let a,f=w in
ind(p,a,f,λb.F(C[p; a; b],f(b)) in
F(par;w) ==
fix((λpW-rec,par,w. let a,f = w in ind[par; a; f; λb.(pW-rec C[par; a; b] (f b))])) par 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 :
pW-rec
Latex:
let ind(p,a,f,G) = ind[p; a; f; G] in
letrec F(p,w) = let a,f=w in
ind(p,a,f,\mlambda{}b.F(C[p; a; b],f(b)) in
F(par;w)
==r let a,f = w
in ind[par; a; f; \mlambda{}b.let ind(p,a,f,G) = ind[p; a; f; G] in
letrec F(p,w) = let a,f=w in
ind(p,a,f,\mlambda{}b.F(C[p; a; b],f(b)) in
F(C[par; a; b];f b)]
Latex:
let ind(p,a,f,G) = ind[p; a; f; G] in
letrec F(p,w) = let a,f=w in
ind(p,a,f,\mlambda{}b.F(C[p; a; b],f(b)) in
F(par;w) ==
fix((\mlambda{}pW-rec,par,w. let a,f = w in ind[par; a; f; \mlambda{}b.(pW-rec C[par; a; b] (f b))])) par w
Date html generated:
2016_05_14-AM-06_14_08
Last ObjectModification:
2015_09_22-PM-05_47_12
Theory : co-recursion
Home
Index