SGER: Axiomatizing Fixed Points

SGER：不动点公理化

• 批准号: 0119916
• 负责人: Stephen Bloom
• 金额: $ 2.34万
• 依托单位: Stevens Institute of Technology
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2001
• 资助国家: 美国
• 起止时间: 2001-08-01 至 2002-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0119916&HistoricalAwards=false
• 关键词: SGER; Axiomatizing; Fixed; Points

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.

史蒂芬·L·布鲁姆：《不动点公理化》史蒂文斯出版社。技术的目的拟议工作的目的是获得对计算中的“不动点”或“迭代”运算的性质的完整而简单的描述。更简单的公理可能导致自由结构的具体离散，我们打算使用这些公理和/或这些具体描述来发现和改进决策算法。Bloom，Esik等人以前的工作已经得到了迭代运算所满足的方程定律的完整描述。这种描述采用迭代理论的公理的形式，它捕捉了计算理论中许多感兴趣的结构的重要特征。迭代理论的原始公理化包含了一个复杂的方程方案。最近，这一方案已被“组身份”所取代。然而，进一步的简化似乎是可能的。另一个目标是找到迭代理论的相对有限公理，这些公理由额外的运算和/或关系丰富。如果成功，就会有一些主要的有益推论。例如，有限状态过程的并发行为(包括互相似等价和迹等价)、有转换和无转换的Kleene关系代数的并发行为、递归程序模式或递归数据类型定义的行为等价等的一组相对简单的公理。最后，研究者和其他人的一些先前的工作表明迭代理论的定律在2-范畴的极端一般的背景下成立，我们打算详细地研究这一现象。