广义进程的受保护与不受保护迭代
Guarded and Unguarded Iteration for Generalized Processes
AI总结：
本文为单子引入抽象受保护性概念，证明埃尔戈特单子恰为抽象受保护迭代单子的迭代同余收缩，从而统一了受保护与不受保护迭代模型。
摘要：
迭代计算模型，如（完全）迭代单子，通常依赖于受保护性（guardedness）的概念，该概念保证递归方程的唯一可解性，并大致要求递归调用仅在特定的保护操作下发生。另一方面，许多迭代模型确实允许不受保护的迭代。此时解不再唯一，且通常甚至不能确定为最小或最大不动点，而是由拟等式公理支配。支持这种意义上不受保护迭代的单子称为（完全）埃尔戈特单子（Elgot monads）。在此，我们提议为单子的（Kleisli范畴）配备一个抽象的受保护性概念，然后要求抽象受保护的递归方程具有可解性；此类抽象受保护的前迭代单子的例子既包括迭代单子，也包括埃尔戈特单子，后者通过将任何递归定义视为抽象受保护来实现。我们的主要结果是：埃尔戈特单子恰好是抽象受保护迭代单子的迭代同余收缩（iteration-congruent retracts），后者被定义为允许抽象受保护递归方程具有唯一解；换言之，不受保护迭代的模型通过对受保护迭代模型进行商化而得到。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
