Document Open Access Logo

Certified Intersection of Commutative Regular Expressions as Solutions of Systems of Linear Diophantine Equations

Authors Ricardo Almeida , Blair Archibald , Basile Pesin , Michele Sevegnani

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITP.2026.7.pdf
  • Filesize: 1.37 MB
  • 20 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Regular languages
  • Software and its engineering → Formal software verification
Keywords
  • commutative regular expressions
  • linear Diophantine equations
  • interactive theorem provers
  • Rocq

Metrics

Abstract

Commutative regular expressions describe sets of unordered words, and are used, for example, when building type systems for process calculi. In these applications, an important operation is finding the intersection of two expressions, but no algorithm currently exists. We remedy this by proposing an algorithm for computing intersections of commutative regular expressions, which we implement and prove correct in the Rocq prover. The algorithm encodes the intersection of two expressions as systems of linear Diophantine equations, and extracts from their solution an intersection expression. To solve these systems we implement and verify the algorithm proposed by Contejean and Devie. We detail the implementation of the intersection algorithm, highlight essential aspects of the proofs (including the complex proof of termination of the equation system solver), and evaluate the OCaml-extracted solver on random and real-world commutative regular expressions.

Cite As Get BibTex

Ricardo Almeida, Blair Archibald, Basile Pesin, and Michele Sevegnani. Certified Intersection of Commutative Regular Expressions as Solutions of Systems of Linear Diophantine Equations. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 7:1-7:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.ITP.2026.7

Author Details

Ricardo Almeida
  • School of Computing Science, University of Glasgow, UK
Blair Archibald
  • School of Computing Science, University of Glasgow, UK
Basile Pesin
  • Fédération ENAC ISAE-SUPAERO ONERA, Université de Toulouse, France
Michele Sevegnani
  • School of Computing Science, University of Glasgow, UK

Funding

This work is partially supported by the British Council through the Alliance Hubert Curien Programme under grant 49780UL and an Amazon Research Award on Automated Reasoning.

Acknowledgements

We thank A. Logan for pointing us in the direction of the Contejean-Devie algorithm for solving systems of linear Diophantine equations, and Rocq-discourse users (A. Trieu, D. Larchey-Wendling, Y. Zakowski and J-M. Mariot) for their help with the proof of Lemma 8.

Supplementary Materials

References

  1. Farid Ajili and Evelyne Contejean. Avoiding slack variables in the solving of linear diophantine equations and inequations. Theoretical Computer Science, 173(1):183-208, 1997. URL: https://doi.org/10.1016/S0304-3975(96)00195-8.
  2. André Almeida, Marco Almeida, José Alves, Nelma Moreira, and Rogério Reis. FAdo and GUItar: Tools for automata manipulation and visualization. In Sebastian Maneth, editor, Implementation and Application of Automata, pages 65-74, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-02979-0_10.
  3. Ricardo Almeida, Blair Archibald, Basile Pesin, and Michele Sevegnani. Certified intersection of commutative regular expressions as solutions of systems of linear diophantine equations, May 2026. URL: https://doi.org/10.5281/zenodo.20265929.
  4. Blair Archibald and Michele Sevegnani. A Bigraphs Paper of Sorts. In Russ Harmer and Jens Kosiol, editors, Graph Transformation, pages 21-38. Springer Nature Switzerland, 2024. URL: https://doi.org/10.1007/978-3-031-64285-2_2.
  5. Iovka Boneva, Radu Ciucanu, and Sławek Staworko. Schemas for unordered xml on a dime. Theory of Computing Systems, 57(2):337-376, 2015. URL: https://doi.org/10.1007/s00224-014-9593-1.
  6. Michael Clausen and Albrecht Fortenbacher. Efficient solution of linear diophantine equations. Journal of Symbolic Computation, 8(1):201-216, 1989. URL: https://doi.org/10.1016/S0747-7171(89)80025-2.
  7. Manuel Clavel, Francisco Durán, Steven Eker, Santiago Escobar, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, and Carolyn Talcott. Unification and narrowing in maude 2.4. In Ralf Treinen, editor, Rewriting Techniques and Applications, pages 380-390, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-02348-4_27.
  8. Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, and Carolyn Talcott. All about maude-a high-performance logical framework: how to specify, program, and verify systems in rewriting logic, volume 4350. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-71999-1.
  9. Evelyne Contejean. Solving *-problems modulo distributivity by a reduction to ac1-unification. Journal of Symbolic Computation, 16(5):493-521, 1993. URL: https://doi.org/10.1006/jsco.1993.1060.
  10. Evelyne Contejean and Hervé Devie. An Efficient Incremental Algorithm for Solving Systems of Linear Diophantine Equations. Information and Computation, 113(1):143-172, 1994. URL: https://doi.org/10.1006/inco.1994.1067.
  11. John H. Conway. Regular Algebra and Finite Machines. Chapman and Hall, 1971. URL: https://doi.org/10.2307/3616008.
  12. Justin DeBenedetto and David Chiang. Algorithms and training for weighted multiset automata and regular expressions. In Cezar Câmpeanu, editor, Implementation and Application of Automata, pages 146-158, Cham, 2018. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-94812-6_13.
  13. Ugo de'Liguoro and Luca Padovani. Mailbox Types for Unordered Interactions. In Todd Millstein, editor, 32nd European Conference on Object-Oriented Programming (ECOOP 2018), volume 109 of Leibniz International Proceedings in Informatics (LIPIcs), pages 15:1-15:28, Dagstuhl, Germany, 2018. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2018.15.
  14. Simon Fowler. MBCheck: A typechecker for the Pat language. URL: https://github.com/SimonJF/mbcheck.
  15. Simon Fowler, Duncan Paul Attard, Franciszek Sowul, Simon J. Gay, and Phil Trinder. Special Delivery: Programming with Mailbox Types. In Proceedings of the ACM on Programming Languages, volume 7, pages 78-107, 2023. URL: https://doi.org/10.1145/3607832.
  16. Miriam Franchella. On the origins of dénes könig’s infinity lemma. Archive for History of Exact Sciences, 51(1):3-27, March 1997. URL: https://doi.org/10.1007/BF00376449.
  17. Alexander Herold and Jörg H Siekmann. Unification in abelian semigroups. Journal of Automated Reasoning, 3(3):247-283, 1987. URL: https://doi.org/10.1007/BF00243791.
  18. John E. Hopcroft, Rajeev Motwani, and Jeffrey D. Ullman. Introduction to automata theory, languages, and computation, 2nd edition. SIGACT News, 32(1):60-65, March 2001. URL: https://doi.org/10.1145/568438.568455.
  19. Eryk Kopczynski. Complexity of problems of commutative grammars. Logical Methods in Computer Science, Volume 11, Issue 1, March 2015. URL: https://doi.org/10.2168/LMCS-11(1:9)2015.
  20. Xavier Leroy. Well-founded recursion done right. In CoqPL 2024: The Tenth International Workshop on Coq for Programming Languages, London, United Kingdom, January 2024. ACM. URL: https://inria.hal.science/hal-04356563.
  21. GS Makanin. Algorithmic decidability of the rank of constant free equations in a free semigroup. In Dokl. Akad. Nauk, SSSR, volume 243, 1978. Google Scholar
  22. Florian Meßner, Julian Parsert, Jonas Schöpf, and Christian Sternagel. A formally verified solver for homogeneous linear diophantine equations. In Jeremy Avigad and Assia Mahboubi, editors, Interactive Theorem Proving, pages 441-458, Cham, 2018. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-94821-8_26.
  23. Robin Milner. The Space and Motion of Communicating Agents. Cambridge University Press, 2009. URL: https://doi.org/10.1017/CBO9780511626661.
  24. Tadao Murata. Petri nets: Properties, analysis and applications. Proceedings of the IEEE, 77(4):541-580, 1989. URL: https://doi.org/10.1109/5.24143.
  25. Dávid Papp and Béla Vizvári. Effective solution of linear diophantine equation systems with an application in chemistry. Journal of Mathematical Chemistry, 39:15-31, January 2006. URL: https://doi.org/10.1007/s10910-005-9001-9.
  26. Donald Pilling. The Algebra of Operators for Regular Events. University of Cambridge, 1970. URL: https://books.google.co.uk/books?id=vPB40AEACAAJ.
  27. Loïc Pottier. Minimal solutions of linear diophantine systems: bounds and algorithms. In Proceedings of the 4th International Conference on Rewriting Techniques and Applications, RTA-91, pages 162-173, Berlin, Heidelberg, 1991. Springer-Verlag. URL: https://doi.org/10.1007/3-540-53904-2_94.
  28. V.N. Redko. On the algebra of commutative events. Ukrainian Math. J., 16(16):185-195, 1964. In Russian. URL: https://www.scopus.com/pages/publications/0000257607.
  29. Rogério Reis and Nelma Moreira. FAdo 2.2.0, 2024. URL: https://fado.dcc.fc.up.pt/.
  30. Arto Salomaa. Theory of automata. Elsevier, 2014. URL: https://doi.org/10.1016/C2013-0-02221-9.
  31. Michele Sevegnani and Muffy Calder. BigraphER: Rewriting and analysis engine for bigraphs. In Swarat Chaudhuri and Azadeh Farzan, editors, Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part II, volume 9780 of Lecture Notes in Computer Science, pages 494-501. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-41540-6_27.
  32. Slawek Staworko, Iovka Boneva, Jose E. Labra Gayo, Samuel Hym, Eric G. Prud'hommeaux, and Harold Solbrig. Complexity and Expressiveness of ShEx for RDF. In Marcelo Arenas and Martín Ugarte, editors, 18th International Conference on Database Theory (ICDT 2015), volume 31 of Leibniz International Proceedings in Informatics (LIPIcs), pages 195-211, Dagstuhl, Germany, 2015. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ICDT.2015.195.
  33. Mark E. Stickel. A unification algorithm for associative-commutative functions. J. ACM, 28(3):423-434, July 1981. URL: https://doi.org/10.1145/322261.322262.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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