正则余归纳的基础
Foundations of regular coinduction
AI总结：
本文提出正则解释作为归纳与余归纳的中间方式，证明其与有理不动点一致，给出归纳刻画及算法，并定义正则余归纳原理与可靠性技术，且可扩展至带共规则的推理系统。
摘要：
推理系统是一种广泛使用的框架，用于通过推理规则定义可能的递归谓词。它们允许归纳和余归纳两种解释，这两种解释都得到了相当充分的研究。在本文中，我们考虑一种中间方式的解释，称为正则解释，它结合了两种方法的优点：它允许非良基推理，同时保持有限性。我们证明了基于正则树的正则解释的自然证明论定义与有理不动点一致。然后，我们提供了一种等价的归纳刻画，这导致了一种寻找判断的正则推导的算法。基于这些结果，我们定义了正则推理的证明技术：正则余归纳原理，用于证明完备性，以及一种基于正则解释的归纳刻画的归纳技术，用于证明可靠性。最后，我们展示了正则方法可以平滑地扩展到带有共规则的推理系统，这是一种最近引入的广义框架，允许细化余归纳解释，证明了这种灵活的正则解释也承认等价的归纳刻画。
英文摘要：
Inference systems are a widespread framework used to define possibly recursive predicates by means of inference rules. They allow both inductive and coinductive interpretations that are fairly well-studied. In this paper, we consider a middle way interpretation, called regular, which combines advantages of both approaches: it allows non-well-founded reasoning while being finite. We show that the natural proof-theoretic definition of the regular interpretation, based on regular trees, coincides with a rational fixed point. Then, we provide an equivalent inductive characterization, which leads to an algorithm which looks for a regular derivation of a judgment. Relying on these results, we define proof techniques for regular reasoning: the regular coinduction principle, to prove completeness, and an inductive technique to prove soundness, based on the inductive characterization of the regular interpretation. Finally, we show the regular approach can be smoothly extended to inference systems with corules, a recently introduced, generalised framework, which allows one to refine the coinductive interpretation, proving that also this flexible regular interpretation admits an equivalent inductive characterisation.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
