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)\perpthe lifted sum of the terminating values (where b is false) and the infinite loops. Previous | Index | Next An error occured whilst processing this directive