Document Open Access Logo

A Complete Axiomatisation of a Fragment of Language Algebra

Author Paul Brunet

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2020.11.pdf
  • Filesize: 440 kB
  • 15 pages

Document Identifiers

Related Versions

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)
    0
    PDF Downloads
    0
    Metadata Views

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.

Cite As Get 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

Author Details

Paul Brunet
  • University College London, United Kingdom

Funding

This work was funded by the EPSRC grant IRIS (reference EP/R006865/1).

Acknowledgements

I want to thank the anonymous referees who provided valuable comments, and Amina Doumane for her kind assistance.

Supplementary Materials

References

  1. 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.
  2. 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.
  3. 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.
  4. John H. Conway. Regular algebra and finite machines. Chapman and Hall Mathematics Series, 2012. Google Scholar
  5. 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.
  6. 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.
  7. Dexter Kozen. Kleene Algebra with Tests. ACM Trans. Program. Lang. Syst., 19(3):427-443, 1997. URL: https://doi.org/10.1145/256167.256195.
  8. 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.
  9. Frank W. Levi. On semigroups. Bull. Calcutta Math. Soc, 36(141-146):82, 1944. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact