Guarded and Unguarded Iteration for Generalized Processes
Goncharov S, Schröder L, Rauch C, Pirog M (2019)
Publication Type: Journal article
Publication year: 2019
Journal
Book Volume: 15
Journal Issue: 3
DOI: 10.23638/LMCS-15(3:1)2019
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 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 (Kleisli categories of) 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 iterative monads and Elgot monads, the latter by deeming any recursive definition to be abstractly guarded. Our main result is then that Elgot monads are precisely the iteration-congruent retracts of abstractly guarded iterative monads, the latter being defined as admitting unique solutions of abstractly guarded recursive equations; in other words, models of unguarded iteration come about by quotienting models of guarded iteration.
Authors with CRIS profile
Sergey Goncharov
Lehrstuhl für Informatik 8 (Theoretische Informatik)
Lutz Schröder
Lehrstuhl für Informatik 8 (Theoretische Informatik)
Christoph Rauch
Lehrstuhl für Informatik 8 (Theoretische Informatik)
Related research project(s)
Involved external institutions
Poland (PL)How to cite
APA:
Goncharov, S., Schröder, L., Rauch, C., & Pirog, M. (2019). Guarded and Unguarded Iteration for Generalized Processes. Logical Methods in Computer Science, 15(3). https://dx.doi.org/10.23638/LMCS-15(3:1)2019
MLA:
Goncharov, Sergey, et al. "Guarded and Unguarded Iteration for Generalized Processes." Logical Methods in Computer Science 15.3 (2019).
BibTeX: Download