文章基本信息

标题：Precongruences and Parametrized Coinduction for Logics for Behavioral Equivalence
本地全文：下载
作者：David Sprunger ; Lawrence S. Moss
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2017
卷号：72
页码：23:1-23:15
DOI：10.4230/LIPIcs.CALCO.2017.23
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：We present a new proof system for equality of terms which present elements of the final coalgebra of a finitary set functor. This is most important when the functor is finitary, and we improve on logical systems which have already been proposed in several papers. Our contributions here are (1) a new logical rule which makes for proofs which are somewhat easier to find, and (2) a soundness/completeness theorem which works for all finitary functors, in particular removing a weak pullback preservation requirement that had been used previously. Our work is based on properties of precongruence relations and also on a new parametrized coinduction principle.
关键词：precongruence; kernel bisimulation; finitary functor; coalgebra; behavioural equivalence