Home

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