The marriage of bisimulations and Kripke logical relations
The marriage of bisimulations and Kripke logical relations
复制标题
互模拟与克里普克逻辑关系的结合
DOI：
10.1145/2103656.2103666
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
Viktor Vafeiadis
中科院分区：
文献类型：
--
作者：
C. Hur;Derek Dreyer;Georg Neis;Viktor Vafeiadis
近年来，在开发有效的技术来推理ML类语言中的程序等价性方面取得了很大进展，ML类语言是指结合了高阶函数、递归类型、抽象类型和通用可变引用等联合收割机功能的语言。出现的两种最突出的技术类型是 * 互模拟 * 和 *Kripke逻辑关系（KLR）*。虽然这两种方法都很强大，但它们的互补优势使我们和其他研究人员想知道它们之间是否存在必要的权衡。此外，这两种方法似乎都受到基本的限制，如果一个人有兴趣将它们扩展到跨语言推理。在本文中，我们提出了 * 关系转换系统（RTS）*，它结合了KLR和互模拟的一些最吸引人的方面。特别是，RTS显示如何互模拟的支持推理递归功能通过 *coinduction* 可以合成与KLR的支持推理本地状态通过 * 状态转换系统 *。此外，我们设计了RTS，以避免KLR和互模拟的限制，排除他们的泛化到跨语言推理。值得注意的是，与KLR不同，RTS是可传递组合的。
There has been great progress in recent years on developing effective techniques for reasoning about program equivalence in ML-like languages---that is, languages that combine features like higher-order functions, recursive types, abstract types, and general mutable references. Two of the most prominent types of techniques to have emerged are *bisimulations* and *Kripke logical relations (KLRs)*. While both approaches are powerful, their complementary advantages have led us and other researchers to wonder whether there is an essential tradeoff between them. Furthermore, both approaches seem to suffer from fundamental limitations if one is interested in scaling them to inter-language reasoning. In this paper, we propose *relation transition systems (RTSs)*, which marry together some of the most appealing aspects of KLRs and bisimulations. In particular, RTSs show how bisimulations' support for reasoning about recursive features via *coinduction* can be synthesized with KLRs' support for reasoning about local state via *state transition systems*. Moreover, we have designed RTSs to avoid the limitations of KLRs and bisimulations that preclude their generalization to inter-language reasoning. Notably, unlike KLRs, RTSs are transitively composable.