Nuprl Definition : corec-family
A family of type parameterized by P is a member of
the type ⌜P ⟶ Type⌝.
The family of types ⌜λp.Top⌝ is the greatest such family
(under the pointwise subtype ordering).
If H maps ⌜P ⟶ Type⌝ to ⌜P ⟶ Type⌝, then the intersection (as a family)
of the iterates of H is the corecursive family defined by H.
If H satisfies the properties ⌜type-family-continuous{i:l}(P;H)⌝
and ⌜family-monotone{i:l}(P;H)⌝, then the ⌜corec-family(H)⌝ is an
extensional fixed point of H.
(See lemma corec-family-ext)⋅
corec-family(H) == ⋂n:ℕ. H^n (λp.Top)
Definitions occuring in Statement :
isect-family: ⋂a:A. F[a],
fun_exp: f^n,
nat: ℕ,
top: Top,
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
isect-family: ⋂a:A. F[a],
nat: ℕ,
apply: f a,
fun_exp: f^n,
lambda: λx.A[x],
top: Top
FDL editor aliases :
corec-family
Latex:
corec-family(H) == \mcap{}n:\mBbbN{}. H\^{}n (\mlambda{}p.Top)
Date html generated:
2016_07_08-PM-04_47_37
Last ObjectModification:
2015_09_22-PM-05_47_00
Theory : co-recursion
Home
Index