An open problem posed by Milner asks for a proof that a certain axiomatisation, which Milner showed is sound with respect to bisimilarity for regular expressions, is also complete. One of the main difficulties of the problem is the lack of a full Kleene theorem, since there are automata that can not be specified, up to bisimilarity, by an expression. Grabmayer and Fokkink (2020) characterise those automata that can be expressed by regular expressions without the constant 1, and use this characterisation to give a positive answer to Milner's question for this subset of expressions. In this paper, we analyse Grabmayer and Fokkink's proof of completeness from the perspective of universal coalgebra, and thereby give an abstract account of their proof method. We then compare this proof method to another approach to completeness proofs from coalgebraic language theory. This culminates in two abstract proof methods for completeness, what we call the local and global approaches, and a description of when one method can be used in place of the other.
翻译:Milner 提出的一个开放问题要求证明, Milner 所显示的对正态表达式的两异性来说是可靠的, 某种异化也是完整的。 问题的主要困难之一是缺乏完整的 Kleene 定理, 因为有无法用表达式指定至两异性的自动模型。 Grabmayer 和 Fokkink (202020年) 将那些可以用普通表达式表达的、 没有常态 1 的表达式表达的自动模型定性为特征, 并使用此特性来对 Milner 的子表达式的问题做出肯定的回答 。 在本文中, 我们从通用的煤层角度分析Grabmayer 和 Fokkink 的完整证据, 从而抽象地描述它们的证据方法。 我们然后将这一证据方法与另一种方法进行比较, 以另一种方法来从煤雕刻语言理论中获取完整性证明。 这最终以两种抽象的证明方法来证明完整性, 我们称之为本地和全球方法, 并描述何时可以使用一种方法取代另一种方法 。