## Fixpoint and Loop Constructions as Colimits

**C. Barry Jay**
*Abstract:* The constructions of fixpoints and while-loops
in a category of domains can be derived from the colimit,
loop(*f*) of a diagram which consists of a single endomorphism
*f;D->D*. If *f* is increasing then the colimiting map
is the least-fixpoint function *Y* and

loop(*f*) = *fix*(*f*)

the subobject of fixpoints. If

*f* = cond(

*b,g,l*) is the
conditional of a while-program then

loop(*f*) = *D_{\neg b}* +
loop_{\infty}(*g*)\perp

the lifted sum of the terminating values (where

*b* is false)
and the infinite loops.

*LFCS report ECS-LFCS-91-182*

Previous |

Index |

Next