LIPIcs.CSL.2020.11.pdf
- Filesize: 440 kB
- 15 pages
Document
A Complete Axiomatisation of a Fragment of Language Algebra
Author
Paul Brunet 
-
Part of:
Volume:
28th EACSL Annual Conference on Computer Science Logic (CSL 2020)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Computer Science Logic (CSL) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2020-01-06
File
Document Identifiers
Author Details
Acknowledgements
I want to thank the anonymous referees who provided valuable comments, and Amina Doumane for her kind assistance.
Cite AsGet BibTex
Paul Brunet. A Complete Axiomatisation of a Fragment of Language Algebra. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 11:1-11:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.CSL.2020.11
https://doi.org/10.4230/LIPIcs.CSL.2020.11
Abstract
We consider algebras of languages over the signature of reversible Kleene lattices, that is the regular operations (empty and unit languages, union, concatenation and Kleene star) together with intersection and mirror image. We provide a complete set of axioms for the equational theory of these algebras. This proof was developed in the proof assistant Coq.
Subject Classification
ACM Subject Classification
- Theory of computation → Algebraic language theory
Keywords
- Kleene algebra
- language algebra
- completeness theorem
- axiomatisation
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- Hajnal Andréka, Szabolcs Mikulás, and István Németi. The Equational Theory of Kleene Lattices. Theor. Comput. Sci., 412(52):7099-7108, 2011. URL: https://doi.org/10.1016/j.tcs.2011.09.024.
- S. L. Bloom, Z. Ésik, and Gh. Stefanescu. Notes on Equational Theories of Relations. algebra universalis, 33(1):98-126, March 1995. URL: https://doi.org/10.1007/BF01190768.
- Paul Brunet. Reversible Kleene Lattices. In Kim G. Larsen, Hans L. Bodlaender, and Jean-Francois Raskin, editors, 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017), volume 83 of Leibniz International Proceedings in Informatics (LIPIcs), pages 66:1-66:14, Dagstuhl, Germany, 2017. Schloss DagstuhlendashLeibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.MFCS.2017.66.
-
John H. Conway. Regular algebra and finite machines. Chapman and Hall Mathematics Series, 2012.
- Amina Doumane and Damien Pous. Completeness for Identity-Free Kleene Lattices. In Sven Schewe and Lijun Zhang, editors, 29th International Conference on Concurrency Theory (CONCUR 2018), volume 118 of Leibniz International Proceedings in Informatics (LIPIcs), pages 18:1-18:17, Dagstuhl, Germany, 2018. Schloss DagstuhlendashLeibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2018.18.
- D. Kozen. A Completeness Theorem for Kleene Algebras and the Algebra of Regular Events. Information and Computation, 110(2):366-390, May 1994. URL: https://doi.org/10.1006/inco.1994.1037.
- Dexter Kozen. Kleene Algebra with Tests. ACM Trans. Program. Lang. Syst., 19(3):427-443, 1997. URL: https://doi.org/10.1145/256167.256195.
- Daniel Krob. Complete Systems of B-Rational Identities. Theoretical Computer Science, 89(2):207-343, October 1991. URL: https://doi.org/10.1016/0304-3975(91)90395-I.
-
Frank W. Levi. On semigroups. Bull. Calcutta Math. Soc, 36(141-146):82, 1944.