终止的代数概念
Algebraic Notions of Termination
摘要：
对终止的五个代数概念进行了形式化、分析和比较：有理或Noetherity、Löb公式、不存在无限迭代、不存在发散和规范化。研究的基础是模态半环，这是加法幂等半环的前向和后向模态算子。为了模拟无限行为，幂等元半环被推广到发散半环、发散Kleene代数和Ω代数。由此产生的概念和技术用于重写理论的经典定理的计算证明。这些应用表明，模态半环是有力的工具，代数推理的有限和无限的动态程序和过渡系统。
英文摘要：
Five algebraic notions of termination are formalised, analysed and compared: wellfoundedness or Noetherity, Löb's formula, absence of infinite iteration, absence of divergence and normalisation. The study is based on modal semirings, which are additively idempotent semirings with forward and backward modal operators. To model infinite behaviours, idempotent semirings are extended to divergence semirings, divergence Kleene algebras and omega algebras. The resulting notions and techniques are used in calculational proofs of classical theorems of rewriting theory. These applications show that modal semirings are powerful tools for reasoning algebraically about the finite and infinite dynamics of programs and transition systems.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
