English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Tools annual

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Presents the access of premium content as premium feature

Premium Content

Global: Zendy Plus annual

Global: Zendy Free Plan

Milner (1984) defined an operational semantics for regular expressions asfinite-state processes. In order to axiomatize bisimilarity of regularexpressions under this process semantics, he adapted Salomaa's proof systemthat is complete for equality of regular expressions under the languagesemantics. Apart from most equational axioms, Milner's system Mil inherits fromSalomaa's system a non-algebraic rule for solving single fixed-point equations.Recognizing distinctive properties of the process semantics that renderSalomaa's proof strategy inapplicable, Milner posed completeness of the systemMil as an open question.  As a proof-theoretic approach to this problem we characterize thederivational power that the fixed-point rule adds to the purely equational partMil$^-$ of Mil. We do so by means of a coinductive rule that permits cyclicderivations that consist of a finite process graph with empty steps thatsatisfies the layered loop existence and elimination property LLEE, and two ofits Mil$^{-}$-provable solutions. With this rule as replacement for thefixed-point rule in Mil, we define the coinductive reformulation cMil as anextension of Mil$^{-}$. In order to show that cMil and Mil are theoremequivalent we develop effective proof transformations from Mil to cMil, andvice versa. Since it is located half-way in between bisimulations and proofs inMilner's system Mil, cMil may become a beachhead for a completeness proof ofMil.  This article extends our contribution to the CALCO 2022 proceedings. Here werefine the proof transformations by framing them as eliminations of derivableand admissible rules, and we link coinductive proofs to a coalgebraicformulation of solutions of process graphs.

A Coinductive Reformulation of Milner's Proof System for Regular Expressions Modulo Bisimilarity