Milner (1984) defined an operational semantics for regular expressions as finite-state processes. In order to axiomatize bisimilarity of regular expressions under this process semantics, he adapted Salomaa's proof system that is complete for equality of regular expressions under the language semantics. Apart from most equational axioms, Milner's system Mil inherits from Salomaa's system a non-algebraic rule for solving single fixed-point equations. Recognizing distinctive properties of the process semantics that render Salomaa's proof strategy inapplicable, Milner posed completeness of the system Mil as an open question. As a proof-theoretic approach to this problem we characterize the derivational power that the fixed-point rule adds to the purely equational part Mil$^-$ of Mil. We do so by means of a coinductive rule that permits cyclic derivations that consist of a finite process graph with empty steps that satisfies the layered loop existence and elimination property LLEE, and two of its Mil$^{-}$-provable solutions. With this rule as replacement for the fixed-point rule in Mil, we define the coinductive reformulation cMil as an extension of Mil$^{-}$. In order to show that cMil and Mil are theorem equivalent we develop effective proof transformations from Mil to cMil, and vice versa. Since it is located half-way in between bisimulations and proofs in Milner's system Mil, cMil may become a beachhead for a completeness proof of Mil. This article extends our contribution to the CALCO 2022 proceedings. Here we refine the proof transformations by framing them as eliminations of derivable and admissible rules, and we link coinductive proofs to a coalgebraic formulation of solutions of process graphs.
翻译:Milner(1984年) 定义了常规表达式的操作语义, 以限定状态进程为常规表达式。 为了在这一过程语义学中将常规表达式的二相似性进行分解, 他调整了Salomaa的校验系统, 在语言语义中完全平等。 除了大多数方程式轴外, Milner的系统继承了Salomaaa的系统, 这是一种非通俗规则, 用来解决单一固定点方程式。 承认使Salomaa的证明战略无法适用的进程语义的特殊性, Milner 将系统Mil (Mil) 的完整作为一个开放的问题。 作为解决这一问题的证明性理论方法, 我们把固定点规则添加到纯方程式的方程式 Mil$- $ 。 我们这样做的方式是, 由一个有限的进程图解出, 包括一个满足分层循环存在和清除属性LLEEE的空步骤, 以及两个我们用来证明的 Mil___ oil- probil 20- probil) 解决方案的精细化。