Nuprl Definition : corec
For any function F: Type -> Type, the iterates F^n(Top), n ∈ ℕ form a family
of types and ⋂n:ℕ. F^n(Top) is a type.
If F is monotone and continuous (preserves omega limits) then the intersection
is the greatest fixpoint for F (see corec-ext)⋅
corec(T.F[T]) == ⋂n:ℕ. primrec(n;Top;λ,T. F[T])
Definitions occuring in Statement :
primrec: primrec(n;b;c),
nat: ℕ,
top: Top,
lambda: λx.A[x],
isect: ⋂x:A. B[x]
Definitions occuring in definition :
isect: ⋂x:A. B[x],
nat: ℕ,
primrec: primrec(n;b;c),
top: Top,
lambda: λx.A[x]
FDL editor aliases :
corec
Latex:
corec(T.F[T]) == \mcap{}n:\mBbbN{}. primrec(n;Top;\mlambda{},T. F[T])
Date html generated:
2016_07_08-PM-04_47_36
Last ObjectModification:
2015_09_22-PM-05_46_57
Theory : co-recursion
Home
Index