Document Open Access Logo

Completeness Theorems for Kleene Algebra with Top

Authors Damien Pous, Jana Wagemaker

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2022.26.pdf
  • Filesize: 0.64 MB
  • 18 pages

Document Identifiers

Author Details

Damien Pous
  • Plume, LIP, CNRS, ENS de Lyon, France
Jana Wagemaker
  • University of Nijmegen, The Netherlands

Funding

This work was supported by the LABEX MILYON (ANR-10-LABX-0070) of Université de Lyon, within the program "Investissements d'Avenir" (ANR-11-IDEX- 0007) operated by the French National Research Agency (ANR).

Acknowledgements

The authors would like to thank Paul Brunet, Amina Doumane, and Jurriaan Rot for the discussions that eventually led to this work, and the CONCUR reviewers for all their comments.

Cite AsGet BibTex

Damien Pous and Jana Wagemaker. Completeness Theorems for Kleene Algebra with Top. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 26:1-26:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.CONCUR.2022.26

Abstract

We prove two completeness results for Kleene algebra with a top element, with respect to languages and binary relations. While the equational theories of those two classes of models coincide over the signature of Kleene algebra, this is no longer the case when we consider an additional constant "top" for the full element. Indeed, the full relation satisfies more laws than the full language, and we show that those additional laws can all be derived from a single additional axiom. We recover that the two equational theories coincide if we slightly generalise the notion of relational model, allowing sub-algebras of relations where top is a greatest element but not necessarily the full relation. We use models of closed languages and reductions in order to prove our completeness results, which are relative to any axiomatisation of the algebra of regular events.

Subject Classification

ACM Subject Classification
  • Theory of computation → Equational logic and rewriting
  • Theory of computation → Logic and verification
  • Theory of computation → Regular languages
Keywords
  • Kleene algebra
  • Hypotheses
  • Completeness
  • Closed languages

Metrics

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

References

  1. H. Andréka and S. Mikulás. Axiomatizability of positive algebras of binary relations. Algebra Universalis, 66(1):7-34, 2011. URL: https://doi.org/10.1007/s00012-011-0142-3.
  2. H. Andréka, S. Mikulás, and I. Németi. The equational theory of Kleene lattices. Theoretical Computer Science, 412(52):7099-7108, 2011. URL: https://doi.org/10.1016/j.tcs.2011.09.024.
  3. H. Andréka and D.A. Bredikhin. The equational theory of union-free algebras of relations. Algebra Universalis, 33(4):516-532, 1995. URL: https://doi.org/10.1007/BF01225472.
  4. Stephen L. Bloom, Zoltán Ésik, and Gheorghe Stefanescu. Notes on equational theories of relations. Algebra Universalis, 33(1):98-126, 1995. URL: https://doi.org/10.1007/BF01190768.
  5. Maurice Boffa. Une remarque sur les systèmes complets d'identités rationnelles. Informatique Théorique et Applications, 24:419-428, 1990. URL: http://archive.numdam.org/article/ITA_1990__24_4_419_0.pdf.
  6. Maurice Boffa. Une condition impliquant toutes les identités rationnelles. Informatique Théorique et Applications, 29(6):515-518, 1995. URL: http://www.numdam.org/article/ITA_1995__29_6_515_0.pdf.
  7. Paul Brunet and Damien Pous. Petri automata for Kleene allegories. In LICS, pages 68-79. ACM, 2015. URL: https://doi.org/10.1109/LICS.2015.17.
  8. Paul Brunet and Damien Pous. Algorithms for Kleene algebra with converse. Journal of Logical and Algebraic Methods in Programming, 85(4):574-594, 2016. URL: https://doi.org/10.1016/j.jlamp.2015.07.005.
  9. J.H. Conway. Regular Algebra and Finite Machines. Chapman and Hall mathematics series. Chapman and Hall, 1971. URL: https://books.google.nl/books?id=1KAXc5TpEV8C.
  10. Anupam Das, Amina Doumane, and Damien Pous. Left-handed completeness for Kleene algebra, via cyclic proofs. In LPAR, volume 57 of EPiC Series in Computing, pages 271-289. Easychair, 2018. URL: https://doi.org/10.29007/hzq3.
  11. Amina Doumane, Denis Kuperberg, Pierre Pradic, and Damien Pous. Kleene algebra with hypotheses. In FoSSaCS, volume 11425 of LNCS, pages 207-223. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-17127-8_12.
  12. Amina Doumane and Damien Pous. Completeness for identity-free Kleene lattices. In CONCUR, volume 118 of LIPIcs, pages 18:1-18:17. Schloss Dagstuhl, 2018. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2018.18.
  13. Zoltán Ésik and Laszlo Bernátsky. Equational properties of Kleene algebras of relations with conversion. Theoretical Computer Science, 137(2):237-251, 1995. URL: https://doi.org/10.1016/0304-3975(94)00041-G.
  14. P. Freyd and A. Scedrov. Categories, Allegories. North Holland, 1990. Google Scholar
  15. Tobias Kappé, Paul Brunet, Alexandra Silva, Jana Wagemaker, and Fabio Zanasi. Concurrent Kleene algebra with observations: from hypotheses to completeness. In FoSSaCS, volume 12077 of LNCS, pages 381-400. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-45231-5_20.
  16. S. C. Kleene. Representation of events in nerve nets and finite automata. In Automata Studies, pages 3-41. Princeton University Press, 1956. URL: http://www.rand.org/pubs/research_memoranda/2008/RM704.pdf.
  17. D. Kozen. Kleene algebra with tests. ACM Transactions on Programming Languages and Systems, 19(3):427-443, May 1997. URL: https://doi.org/10.1145/256167.256195.
  18. D. Kozen. On Hoare logic and Kleene algebra with tests. ACM Transactions on Computational Logic, 1(1):60-76, 2000. URL: https://doi.org/10.1145/343369.343378.
  19. D. Kozen and M.-C. Patron. Certification of compiler optimizations using Kleene algebra with tests. In CL2000, volume 1861 of LNAI, pages 568-582. Springer, 2000. URL: https://doi.org/10.1007/3-540-44957-4_38.
  20. D. Kozen and F. Smith. Kleene algebra with tests: Completeness and decidability. In CSL, volume 1258 of LNCS, pages 244-259. Springer, September 1996. URL: https://doi.org/10.1007/3-540-63172-0_43.
  21. Dexter Kozen. A completeness theorem for Kleene Algebras and the algebra of regular events. In LICS, pages 214-225. IEEE Computer Society, 1991. URL: https://doi.org/10.1109/LICS.1991.151646.
  22. Dexter Kozen and Alexandra Silva. Left-handed completeness. In RAMiCS, volume 7560 of LNCS, pages 162-178. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-33314-9_11.
  23. A. Krauss and T. Nipkow. Proof pearl: Regular expression equivalence and relation algebra. Journal of Automated Reasoning, 49(1):95-106, 2012. URL: https://doi.org/10.1007/s10817-011-9223-4.
  24. D. Krob. Complete systems of B-rational identities. Theoretical Computer Science, 89(2):207-343, 1991. URL: https://doi.org/10.1016/0304-3975(91)90395-I.
  25. Konstantinos Mamouras. Equational theories of abnormal termination based on Kleene algebra. In FoSSaCS, volume 10203 of LNCS, pages 88-105. Springer, 2017. URL: https://doi.org/10.1007/978-3-662-54458-7_6.
  26. Yoshiki Nakamura. Partial derivatives on graphs for Kleene allegories. In LICS, pages 1-12. IEEE, 2017. URL: https://doi.org/10.1109/LICS.2017.8005132.
  27. Peter W. O'Hearn. Incorrectness logic. Proc. ACM Program. Lang., 4(POPL):10:1-10:32, 2020. URL: https://doi.org/10.1145/3371078.
  28. Damien Pous. Kleene Algebra with Tests and Coq tools for while programs. In ITP, volume 7998 of LNCS, pages 180-196. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39634-2_15.
  29. Damien Pous. On the positive calculus of relations with transitive closure. In STACS, volume 96 of LIPIcs, pages 3:1-3:16. Schloss Dagstuhl, 2018. URL: https://doi.org/10.4230/LIPIcs.STACS.2018.3.
  30. Damien Pous, Jurriaan Rot, and Jana Wagemaker. On tools for completeness of Kleene algebra with hypotheses. In RAMiCS, volume 13027 of LNCS, pages 378-395. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-88701-8_23.
  31. V. R. Pratt. Dynamic algebras and the nature of induction. In ACM Symposium on Theory of Computing, STOC '80, pages 22-28, New York, NY, USA, 1980. Association for Computing Machinery. URL: https://doi.org/10.1145/800141.804649.
  32. V.N. Redko. On the algebra of commutative events. Ukrainian Math. Zh., 16:185-195, 1964. Google Scholar
  33. Cheng Zhang, Arthur Azevedo de Amorim, and Marco Gaboardi. On incorrectness logic and Kleene algebra with top and tests. Proc. ACM Program. Lang., 6(POPL):1-30, 2022. URL: https://doi.org/10.1145/3498690.
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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact