Guarded and Unguarded Iteration for Generalized Processes

摘要

Models of iterated computation, such as (completely) iterative monads, oftendepend on a notion of guardedness, which guarantees unique solvability ofrecursive equations and requires roughly that recursive calls happen only undercertain guarding operations. On the other hand, many models of iteration doadmit unguarded iteration. Solutions are then no longer unique, and in generalnot even determined as least or greatest fixpoints, being instead governed byquasi-equational axioms. Monads that support unguarded iteration in this senseare called (complete) Elgot monads. Here, we propose to equip (Kleislicategories of) monads with an abstract notion of guardedness and then requiresolvability of abstractly guarded recursive equations; examples of suchabstractly guarded pre-iterative monads include both iterative monads and Elgotmonads, the latter by deeming any recursive definition to be abstractlyguarded. Our main result is then that Elgot monads are precisely theiteration-congruent retracts of abstractly guarded iterative monads, the latterbeing defined as admitting unique solutions of abstractly guarded recursiveequations; in other words, models of unguarded iteration come about byquotienting models of guarded iteration.