Guarded and Unguarded Iteration for Generalized Processes
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 iterat...
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2019-07-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/4170/pdf |
| _version_ | 1827322765615562752 |
|---|---|
| author | Sergey Goncharov Lutz Schröder Christoph Rauch Maciej Piróg |
| author_facet | Sergey Goncharov Lutz Schröder Christoph Rauch Maciej Piróg |
| author_sort | Sergey Goncharov |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-25T01:34:04Z |
| format | Article |
| id | doaj.art-0341b7ba8945445ab238610f8f96fd70 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:34:04Z |
| publishDate | 2019-07-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-0341b7ba8945445ab238610f8f96fd702024-03-08T10:28:03ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742019-07-01Volume 15, Issue 310.23638/LMCS-15(3:1)20194170Guarded and Unguarded Iteration for Generalized ProcessesSergey GoncharovLutz SchröderChristoph RauchMaciej PirógModels 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.https://lmcs.episciences.org/4170/pdfcomputer science - logic in computer science03d75, 68q55f.4.1 |
| spellingShingle | Sergey Goncharov Lutz Schröder Christoph Rauch Maciej Piróg Guarded and Unguarded Iteration for Generalized Processes Logical Methods in Computer Science computer science - logic in computer science 03d75, 68q55 f.4.1 |
| title | Guarded and Unguarded Iteration for Generalized Processes |
| title_full | Guarded and Unguarded Iteration for Generalized Processes |
| title_fullStr | Guarded and Unguarded Iteration for Generalized Processes |
| title_full_unstemmed | Guarded and Unguarded Iteration for Generalized Processes |
| title_short | Guarded and Unguarded Iteration for Generalized Processes |
| title_sort | guarded and unguarded iteration for generalized processes |
| topic | computer science - logic in computer science 03d75, 68q55 f.4.1 |
| url | https://lmcs.episciences.org/4170/pdf |
| work_keys_str_mv | AT sergeygoncharov guardedandunguardediterationforgeneralizedprocesses AT lutzschroder guardedandunguardediterationforgeneralizedprocesses AT christophrauch guardedandunguardediterationforgeneralizedprocesses AT maciejpirog guardedandunguardediterationforgeneralizedprocesses |