SGER: Axiomatizing Fixed Points

Stephen L. Bloom《不动点的公理化》斯蒂文斯技术学院提出的这项工作的目的是获得对计算中“不动点”或“迭代”操作性质的完整而简单的描述。更简单的公理可能导致自由结构的具体离散，我们打算使用公理和/或这些具体描述来发现和改进决策算法。Bloom， Esik和其他人之前的工作已经对迭代操作所满足的方程定律进行了完整的描述。这种描述采用迭代理论公理的形式，它捕捉了计算理论中许多感兴趣的结构类的重要特征。最初的迭代理论公理化包含了一个复杂的方程格式。最近，这种方案已经被“群体身份”所取代。然而，进一步的简化似乎是可能的。另一个目标是找到通过附加运算和/或关系丰富的迭代理论的相对有限公理化。如果成功的话，会有一些主要的有益的推论。例如，一组相对简单的公理，适用于有限状态过程的并发行为（双相似等价和迹等价），适用于有和没有转换的Kleene关系代数，适用于递归程序方案或递归数据类型定义的行为等价等。最后，研究者和其他人的一些先前的工作表明，迭代定律理论在极一般的2类设置中成立，我们打算详细研究这一现象。

Stephen L. Bloom"Axiomatizing Fixed PointsStevens Inst. of TechnologyThe purpose of the proposed work is to obtain complete, but simple, descriptions of the properties of the "fixed point" or "iteration" operation in computation. Simpler axioms may lead to concrete discreptions of free structures and we intend to use the axioms and/or these concrete descriptions to find and improve decision algorithms. Previous work by Bloom, Esik and others has resulted in a complete description of the equational laws satisfied by the iteration operation. This description takes the form of the axioms for Iteration Theories, which capture important features of many classes of structures of interest in the theory of computation. The original axiomatization of iteration theories contained a complicated equational scheme. Recently, this scheme has been replaced by the "group identities". Nevertheless, further simplifications seem to be possible. Another goal is to find relative finite axiomatizations of iteration theories enriched by additional operations and/or relations. If successful, there are major beneficial corollaries. For example, a relatively simple set of axioms for the concurrent behavior of finite state processes (both for bisimilarity equivalence and for trace equivalence), for Kleene relation algebras with and without conversion, for the behavioral equivalence of recursive program schemes or recursive data type definitions and others.Lastly, some previous work of the investigators and others has indicated that the laws of iteration theories hold in the extremely general setting of 2-categories, and we intend to investigate this phenomenon in detail.