A general account of coinduction up-to
A general account of coinduction up-to
复制标题
共归纳的一般说明
DOI：
10.1007/s00236-016-0271-4
复制
发表时间：
2016
期刊：
影响因子：
0.6
通讯作者：
J. Rot
中科院分区：
文献类型：
--
作者：
F. Bonchi;Daniela Petrisan;D. Pous;J. Rot
互模拟增强了互相似的余归纳证明方法，为检验不同类型系统的性质提供了有效的证明技术。我们在赫米达和雅各布斯的开创性工作的基础上，证明了这些技术在纤维环境中的可靠性。这使我们不仅可以系统地获得最新的技术，不仅可以用于互相似，而且可以用于建模为余代数的一大类余归纳谓词。根据Turi和Plotkin的著名观察，根据上下文的互模拟可以安全地在GSOS规则指定的任何语言中使用这一事实也可以被视为我们框架的一个实例，即这些语言形成双代数。在本文的第二部分中，我们给出了一种新的标签转移系统弱互相似的范畴处理方法，并证明了Bloom定义的冷规则格式所指定的系统的弱互模拟的上至上下文的可靠性，以确保弱互相似的相合性。由这种冷规则得到的弱过渡系统产生了松弛的双代数，而不是双代数。因此，为了达到我们的目标，我们将第一部分中发展的范畴框架扩展到一个有序的环境中。
Bisimulation up-to enhances the coinductive proof method for bisimilarity, providing efficient proof techniques for checking properties of different kinds of systems. We prove the soundness of such techniques in a fibrational setting, building on the seminal work of Hermida and Jacobs. This allows us to systematically obtain up-to techniques not only for bisimilarity but for a large class of coinductive predicates modeled as coalgebras. The fact that bisimulations up to context can be safely used in any language specified by GSOS rules can also be seen as an instance of our framework, using the well-known observation by Turi and Plotkin that such languages form bialgebras. In the second part of the paper, we provide a new categorical treatment of weak bisimilarity on labeled transition systems and we prove the soundness of up-to context for weak bisimulations of systems specified by cool rule formats, as defined by Bloom to ensure congruence of weak bisimilarity. The weak transition systems obtained from such cool rules give rise to lax bialgebras, rather than to bialgebras. Hence, to reach our goal, we extend the categorical framework developed in the first part to an ordered setting.