Talk "Guarded vs. Unguarded Iteration"

by Lutz Schröder

Thu, 12 January 2017 at 09:30 am in Binz (Rügen), Germany

Joint work with: Sergey Goncharov, Maciej Pirog, Christoph Rauch

Abstract: Models of iterated computation, such as completely iterative monads, often depend on a notion of guardedness, which guarantees unique solvability of recursive equations and requires roughly that recursive calls happen only under certain guarding operations. On the other hand, many models of iteration do admit unguarded iteration. Solutions are then no longer unique, and in general (i.e.\ outside domain-theoretic models) not even determined as least or greatest fixpoints, being instead governed by quasi-equational axioms. Monads that support unguarded iteration in this sense are called complete Elgot monads. Here, we propose to equip monads with an abstract notion of guardedness and then require solvability of abstractly guarded recursive equations; examples of such abstractly guarded pre-iterative monads include both completely iterative monads and complete Elgot monads, the latter by deeming any recursive definition to be abstractly guarded. Our main result is then that complete Elgot monads are precisely the iteration-congruent retracts of abstractly guarded iterative monads, the latter being defined as admitting \emph{unique} solutions of abstractly guarded recursive equations. In consequence, we identify complete Elgot monads as certain algebras for a monad on the category of monads.