Sound and Complete Axiomatizations of Coalgebraic Language Equivalence
Sound and Complete Axiomatizations of Coalgebraic Language Equivalence
复制标题
代数语言等价的合理且完整的公理化
DOI：
--
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
Alexandra Silva
中科院分区：
文献类型：
--
作者：
M. Bonsangue;Stefan Milius;Alexandra Silva
余代数为研究动力系统提供了一个统一的框架，包括几种类型的自动机。在这篇文章中，我们利用系统的coalgebraic视图调查，在一个统一的方式，在何种条件下，是健全的和完整的行为等价的演算可以扩展到一个粗糙的coalgebraic语言等价，它产生于一个广义的powerset建设，确定coalgebra。我们通过证明微积分的模公理表达式形成给定类型函子的有理不动点来证明可靠性和完整性。我们的主要结果是函子FT的有理不动点，其中T是描述系统分支的单子（例如，非确定性、权重、概率等），作为商的有理不动点的确定型函子F，提升F的范畴的T-代数。我们应用我们的框架加权自动机的具体例子，我们提出了一个新的声音和完整的演算加权语言等价。作为一个特殊的情况下，我们得到不确定的自动机，我们恢复Rabinovich的声音和完整的演算语言等价。
Coalgebras provide a uniform framework for studying dynamical systems, including several types of automata. In this article, we make use of the coalgebraic view on systems to investigate, in a uniform way, under which conditions calculi that are sound and complete with respect to behavioral equivalence can be extended to a coarser coalgebraic language equivalence, which arises from a generalized powerset construction that determinizes coalgebras. We show that soundness and completeness are established by proving that expressions modulo axioms of a calculus form the rational fixpoint of the given type functor. Our main result is that the rational fixpoint of the functor FT, where T is a monad describing the branching of the systems (e.g., non-determinism, weights, probability, etc.), has as a quotient the rational fixpoint of the determinized type functor F, a lifting of F to the category of T-algebras. We apply our framework to the concrete example of weighted automata, for which we present a new sound and complete calculus for weighted language equivalence. As a special case, we obtain nondeterministic automata in which we recover Rabinovich’s sound and complete calculus for language equivalence.