一句话：提出抽象守卫性统一守卫迭代与 Elgot 单子，并证明 Elgot 单子恰为抽象守卫迭代单子的迭代同余收缩。
本文研究迭代计算的语义模型。传统迭代单子依赖守卫性来保证递归方程有唯一解，而许多模型允许非守卫迭代，此时解不唯一，也未必是最小或最大不动点，而由拟等式公理刻画，这类单子称为 Elgot 单子。作者为（单子的 Kleisli 范畴）引入抽象守卫性概念，并要求抽象守卫递归方程可解。迭代单子和 Elgot 单子都是其例子：前者按通常守卫性，后者把所有递归定义都视为抽象守卫。主要结果是 Elgot 单子恰好是抽象守卫迭代单子的迭代同余收缩；换言之，非守卫迭代模型可由守卫迭代模型取商得到。
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.
@article{paperbot784,
title = {Guarded and Unguarded Iteration for Generalized Processes},
author = {Sergey Goncharov and Lutz Schröder and Christoph Rauch and Maciej Piróg},
journal = {Logical Methods in Computer Science},
volume = {Volume 15, Issue 3},
year = {2019},
doi = {10.23638/lmcs-15(3:1)2019}
}