广义过程的有保护和无保护迭代
摘要：抽象有限态模型中的迭代计算模型通常依赖于一个受保护的概念，它保证递归方程的唯一可解性，并且要求递归调用仅在特定的保护操作下发生。另一方面，许多迭代模型允许非受保护的迭代。在这种情况下，解决方案不再是唯一的，并且通常不是最小或最大不动点，而是受准等公理支配的。支持这种非受保护迭代的单子被称为(完全)Elgot单子。在这里，我们提议为单子(的Kleisli类别)配备一个抽象的受保护概念，然后要求抽象受保护递归方程的可解性; 这种抽象受保护的预迭代单子的例子包括迭代单子和Elgot单子，后者将任何递归定义视为抽象受保护。我们的主要结果是，Elgot单子恰好是抽象受保护迭代单子的迭代同态收缩，后者定义为具有抽象受保护递归方程的唯一解的模型; 换句话说，非受保护迭代的模型是通过对受保护迭代模型进行分类得到的。
作者：Sergey Goncharov, Lutz Schr"oder, Christoph Rauch, Maciej Pir''og
论文ID：1712.09574
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22