论文标题
通过广义参数化共同诱导的弱分配的方程理论
An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction
论文作者
论文摘要
关于诸如溪流之类的无限制结构的共同推理是广泛适用的。但是，用于开发共同证明并找到有助于构建此类证明的推理原则的实用框架仍然是一个挑战，尤其是在机器检查的形式化的背景下。 本文给出了一个方程理论的新颖介绍，用于对结构进行推理，直至弱分成型。该理论既具有组成性，因此适用于定义通用诱饵，也适合逐渐添加，这意味着可以交互性地创建分成型。为了证明该理论的健全性，本文还引入了广义的参数化共同诱导，该共同诱导解决了早期作品的表达问题，并为共同推理提供了实用的框架。该论文介绍了流的产生方程理论，但该技术也适用于其他结构。 本文中的所有结果均已在COQ中证明，并且可以作为COQ库获得广义的参数化共同诱导框架。
Coinductive reasoning about infinitary structures such as streams is widely applicable. However, practical frameworks for developing coinductive proofs and finding reasoning principles that help structure such proofs remain a challenge, especially in the context of machine-checked formalization. This paper gives a novel presentation of an equational theory for reasoning about structures up to weak bisimulation. The theory is both compositional, making it suitable for defining general-purpose lemmas, and also incremental, meaning that the bisimulation can be created interactively. To prove the theory's soundness, this paper also introduces generalized parameterized coinduction, which addresses expressivity problems of earlier works and provides a practical framework for coinductive reasoning. The paper presents the resulting equational theory for streams, but the technique applies to other structures too. All of the results in this paper have been proved in Coq, and the generalized parameterized coinduction framework is available as a Coq library.
