LIPIcs.CALCO.2021.16.pdf
- Filesize: 0.85 MB
- 23 pages
Document
A Coinductive Version of Milner’s Proof System for Regular Expressions Modulo Bisimilarity
Author
-
Part of:
Volume:
9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Conference on Algebra and Coalgebra in Computer Science (CALCO) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2021-11-08
File
Document Identifiers
Acknowledgements
I want to thank Luca Aceto for his comments on the introduction. I am also very grateful to the anonymous reviewers for their careful reading, for spotting distracting oversights, and for asking for additional clarifications, such as concerning the motivation of coinductive proofs.
Cite AsGet BibTex
Clemens Grabmayer. A Coinductive Version of Milner’s Proof System for Regular Expressions Modulo Bisimilarity. In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 16:1-16:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.CALCO.2021.16
https://doi.org/10.4230/LIPIcs.CALCO.2021.16
Abstract
By adapting Salomaa’s complete proof system for equality of regular expressions under the language semantics, Milner (1984) formulated a sound proof system for bisimilarity of regular expressions under the process interpretation he introduced. He asked whether this system is complete. Proof-theoretic arguments attempting to show completeness of this equational system are complicated by the presence of a non-algebraic rule for solving fixed-point equations by using star iteration.
We characterize the derivational power that the fixed-point rule adds to the purely equational part Mil- of Milner’s system Mil: it corresponds to the power of coinductive proofs over Mil- that have the form of finite process graphs with the loop existence and elimination property LEE. We define a variant system cMil by replacing the fixed-point rule in Mil with a rule that permits LEE-shaped circular derivations in Mil- from previously derived equations as a premise. With this rule alone we also define the variant system CLC for combining LEE-shaped coinductive proofs over Mil-. We show that both cMil and CLC have proof interpretations in Mil, and vice versa. As this correspondence links, in both directions, derivability in Mil with derivation trees of process graphs, it widens the space for graph-based approaches to finding a completeness proof of Milner’s system.
Subject Classification
ACM Subject Classification
- Theory of computation → Process calculi
Keywords
- regular expressions
- process theory
- bisimilarity
- coinduction
- proof theory
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- Roberto M. Amadio and Luca Cardelli. Subtyping Recursive Types. ACM Trans. Program. Lang. Syst., 15(4):575-631, September 1993. URL: https://doi.org/10.1145/155183.155231.
- Valentin Antimirov. Partial Derivatives of Regular Expressions and Finite Automaton Constructions. Theoretical Computer Science, 155(2):291-319, 1996. URL: https://doi.org/10.1016/0304-3975(95)00182-4.
- Michael Brandt and Fritz Henglein. Coinductive Axiomatization of Recursive Type Equality and Subtyping. Fundamenta Informaticae, 33(4):309-338, December 1998. URL: https://doi.org/10.1007/3-540-62688-3_29.
- Clemens Grabmayer. Relating Proof Systems for Recursive Types. PhD thesis, Vrije Universiteit Amsterdam, March 2005. URL: http://www.phil.uu.nl/~clemens/linkedfiles/proefschrift.pdf.
-
Clemens Grabmayer. Using Proofs by Coinduction to Find "Traditional" Proofs. In José Luiz Fiadeiro, Neal Harman, Markus Roggenbach, and Jan Rutten, editors, Proceedings of CALCO 2005, volume 3629 of LNCS, pages 175-193. Springer, 2005.
-
Clemens Grabmayer. A Coinductive Axiomatisation of Regular Expressions under Bisimulation. Technical report, University of Nottingham, 2006. Short Contribution to CMCS 2006, March 25-27, 2006, Vienna Institute of Technology, Austria.
- Clemens Grabmayer. Modeling Terms by Graphs with Structure Constraints (Two Illustrations). In Proc. TERMGRAPH@FSCD'18, volume 288, pages 1-13, http://www.eptcs.org/, 2019. EPTCS. URL: https://doi.org/10.4204/EPTCS.288.1.
- Clemens Grabmayer. Structure-Constrained Process Graphs for the Process Semantics of Regular Expressions. Technical report, http://arxiv.org, December 2020. URL: http://arxiv.org/abs/2012.10869.
- Clemens Grabmayer. A Coinductive Version of Milner’s Proof System for Regular Expressions Modulo Bisimilarity. Technical report, http://arxiv.org, August 2021. Extended version of this paper. URL: http://arxiv.org/abs/2108.13104.
- Clemens Grabmayer. Structure-Constrained Process Graphs for the Process Semantics of Regular Expressions. In Patrick Bahr, editor, Proceedings 11th International Workshop on Computing with Terms and Graphs, Online, 5th July 2020, volume 334 of Electronic Proceedings in Theoretical Computer Science, pages 29-45. Open Publishing Association, 2021. URL: https://doi.org/10.4204/EPTCS.334.3.
-
Clemens Grabmayer and Wan Fokkink. A Complete Proof System for 1-Free Regular Expressions Modulo Bisimilarity. In Proceedings of LICS 2020, New York, NY, 2020. ACM. Extended report see [Clemens Grabmayer and Wan Fokkink, 2020].
- Clemens Grabmayer and Wan Fokkink. A Complete Proof System for 1-Free Regular Expressions Modulo Bisimilarity. Technical report, http://arxiv.org, April 2020. URL: http://arxiv.org/abs/2004.12740.
-
Robin Milner. A Complete Inference System for a Class of Regular Behaviours. Journal of Computer and System Sciences, 28(3):439-466, 1984.
- Arto Salomaa. Two Complete Axiom Systems for the Algebra of Regular Events. Journal of the ACM, 13(1):158-169, 1966. URL: https://doi.org/10.1145/321312.321326.