Nuprl Definition : corec

For any function F: Type -> Type, the iterates  F^n(Top), n ∈ ℕ form family
of types and ⋂n:ℕF^n(Top) is type. 
If 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

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