A Complete Axiomatisation of a Fragment of Language Algebra

Author Paul Brunet

Thumbnail PDF


  • Filesize: 440 kB
  • 15 pages

Document Identifiers

Author Details

Paul Brunet
  • University College London, United Kingdom


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)


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
  • Kleene algebra
  • language algebra
  • completeness theorem
  • axiomatisation


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  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

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail