Document Open Access Logo

Finiteness of Symbolic Derivatives in Lean

Authors Ekaterina Zhuchko , Hendrik Maarand , Margus Veanes , Gabriel Ebner

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.ITP.2025.16.pdf
  • Filesize: 0.9 MB
  • 19 pages
HTML5 Logo HTML (experimental)
LIPIcs.ITP.2025.16.html

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Formal languages and automata theory
Keywords
  • Lean
  • regular languages
  • lookarounds
  • derivatives
  • finiteness

Metrics

Abstract

Brzozowski proved that the set of derivatives of any regular expression is finite modulo associativity, idempotence and, notably, commutativity of the union operator. We extend this result to the case of symbolic location based derivatives, for which we prove finiteness of the state space by quotienting only by associativity, deduplication and idempotence (ADI); the fact that we don't use commutativity allows for this result to carry over to the derivative based backtracking (PCRE) match semantics, where the union operator is noncommutative. Furthermore, we consider regular expressions extended with lookarounds, intersection, and negation. We also show that our method for proving finiteness allows us to include certain simplification rules in the derivative operation while preserving finiteness. The finiteness proof is constructive: given an expression R, we construct a finite set that is an overapproximation (modulo ADI) of the set of derivatives of R. We reuse some of the infrastructure provided in previous formalization efforts for regular expressions in Lean 4, showing the flexibility and reusability of the framework.

Cite As Get BibTex

Ekaterina Zhuchko, Hendrik Maarand, Margus Veanes, and Gabriel Ebner. Finiteness of Symbolic Derivatives in Lean. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 16:1-16:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.ITP.2025.16

Author Details

Ekaterina Zhuchko
  • Tallinn University of Technology, Estonia
Hendrik Maarand
  • Tallinn University of Technology, Estonia
Margus Veanes
  • Microsoft Research, Redmond, WA, USA
Gabriel Ebner
  • Microsoft Research, Redmond, WA, USA

Funding

E. Zhuchko and H. Maarand were supported by the Estonian Research Council grant PRG1210 (Automata in Learning, Interaction and Concurrency).

Supplementary Materials

References

  1. Stål Aanderaa. On the algebra of regular expressions. Technical Report, Applied Mathematics, Harvard University, 1965. Google Scholar
  2. Valentin Antimirov. Partial derivatives of regular expressions and finite automata constructions. Theoretical Computer Science, 155:291-319, 1996. URL: https://doi.org/10.1007/3-540-59042-0_96.
  3. Fahad Ausaf, Roy Dyckhoff, and Christian Urban. POSIX lexing with derivatives of regular expressions. In Archive of Formal Proofs, 2016. URL: http://www.isa-afp.org/entries/Posix-Lexing.shtml.
  4. Aurèle Barrière and Clément Pit-Claudel. Linear matching of javascript regular expressions. Proc. ACM Program. Lang., 8(PLDI), June 2024. URL: https://doi.org/10.1145/3656431.
  5. Martin Berglund, Brink van der Merwe, and Steyn van Litsenborgh. Regular expressions with lookahead. Journal of Universal Computer Science, 27(4):324-340, 2021. URL: https://doi.org/10.3897/jucs.66330.
  6. Janusz A. Brzozowski. Derivatives of regular expressions. J. ACM, 11(4):481-494, 1964. URL: https://doi.org/10.1145/321239.321249.
  7. Pascal Caron, Jean-Marc Champarnaud, and Ludovic Mignot. Partial derivatives of an extended regular expression. In Language and Automata Theory and Applications, LATA 2011, volume 6638 of LNCS, pages 179-191. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-21254-3_13.
  8. Jean-Marc Champarnaud and Djelloul Ziadi. From Mirkin’s prebases to Antimirov’s word partial derivatives. Fundam. Inf., 45(3):195-205, January 2001. URL: http://content.iospress.com/articles/fundamenta-informaticae/fi45-3-03.
  9. Thierry Coquand and Vincent Siles. A decision procedure for regular expression equivalence in type theory. In Certified Programs and Proofs, pages 119-134. Springer Berlin Heidelberg, 2011. URL: https://doi.org/10.1007/978-3-642-25379-9_11.
  10. Loris D'Antoni and Margus Veanes. Automata modulo theories. Communications of the ACM, 64(5):86-95, May 2021. URL: https://doi.org/10.1145/3419404.
  11. Derek Egolf, Sam Lasser, and Kathleen Fisher. Verbatim: A verified lexer generator. In 2021 IEEE Security and Privacy Workshops (SPW), pages 92-100, 2021. URL: https://doi.org/10.1109/SPW53761.2021.00022.
  12. Derek Egolf, Sam Lasser, and Kathleen Fisher. Verbatim++: Verified, optimized, and semantically rich lexing with derivatives. In Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2022), pages 27-39. ACM, 2022. URL: https://doi.org/10.1145/3497775.3503694.
  13. Gérard Huet. The zipper. Journal of Functional Programming, 7(5):549-554, 1997. URL: https://doi.org/10.1017/S0956796897002864.
  14. Vladimir Komendantsky. Reflexive toolbox for regular expression matching: verification of functional programs in Coq+Ssreflect. In Proceedings of the Sixth Workshop on Programming Languages Meets Program Verification, PLPV '12, pages 61-70, New York, NY, USA, 2012. Association for Computing Machinery. URL: https://doi.org/10.1145/2103776.2103784.
  15. Konstantinos Mamouras and Agnishom Chattopadhyay. Efficient matching of regular expressions with lookaround assertions. Proc. ACM Program. Lang., 8(POPL), January 2024. URL: https://doi.org/10.1145/3632934.
  16. B. G. Mirkin. An algorithm for constructing a base in a language of regular expressions. Journal of Symbolic Logic, 36(4):694-694, 1971. URL: https://doi.org/10.2307/2272532.
  17. Takayuki Miyazaki and Yasuhiko Minamide. Derivatives of regular expressions with lookahead. J. Inf. Process., 27:422-430, 2019. URL: https://doi.org/10.2197/ipsjjip.27.422.
  18. Nelma Moreira, David Pereira, and Simão Melo de Sousa. Deciding regular expressions (in-)equivalence in Coq. In Wolfram Kahl and Timothy G. Griffin, editors, Relational and Algebraic Methods in Computer Science, pages 98-113, Berlin, Heidelberg, 2012. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-33314-9_7.
  19. Dan Moseley, Mario Nishio, Jose Perez Rodriguez, Olli Saarikivi, Stephen Toub, Margus Veanes, Tiki Wan, and Eric Xu. Derivative based nonbacktracking real-world regex matching with backtracking semantics. In Nate Foster et al., editor, PLDI '23: 44th ACM SIGPLAN International Conference on Programming Language Design and Implementation, Florida, USA, June 17-21, 2023, pages 1-2. ACM, 2023. URL: https://doi.org/10.1145/3591262.
  20. Tobias Nipkow and Dmitriy Traytel. Unified decision procedures for regular expression equivalence. In Gerwin Klein and Ruben Gamboa, editors, Interactive Theorem Proving, pages 450-466, Cham, 2014. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-08970-6_29.
  21. POSIX. IEEE standard for information technology - portable operating system interface (POSIX(R)). IEEE Std 1003.1-2008 (Revision of IEEE Std 1003.1-2004), pages 1-3874, 2008. URL: https://doi.org/10.1109/IEEESTD.2008.4694976.
  22. Olli Saarikivi, Margus Veanes, Tiki Wan, and Eric Xu. Symbolic regex matcher. In Tomáš Vojnar and Lijun Zhang, editors, Tools and Algorithms for the Construction and Analysis of Systems, volume 11427 of LNCS, pages 372-378. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-17462-0_24.
  23. Arto Salomaa. Two complete axiom systems for the algebra of regular events. J. ACM, 13(1):158-169, January 1966. URL: https://doi.org/10.1145/321312.321326.
  24. Caleb Stanford, Margus Veanes, and Nikolaj Bjørner. Symbolic boolean derivatives for efficiently solving extended regular expression constraints. In PLDI'21, pages 620-635. ACM, 2021. URL: https://doi.org/10.1145/3453483.3454066.
  25. Martin Sulzmann and Kenny Zhuo Ming Lu. Regular expression sub-matching using partial derivatives. In Proceedings of the 14th Symposium on Principles and Practice of Declarative Programming (PPDP'12), pages 79-90, New York, NY, USA, 2012. ACM. URL: https://doi.org/10.1145/2370776.2370788.
  26. Martin Sulzmann and Kenny Zhuo Ming Lu. Posix regular expression parsing with derivatives. In M. Codish and E. Sumii, editors, FLOPS 2014, volume 8475 of LNCS, pages 203-220. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-43144-4_5.
  27. Chengsong Tan and Christian Urban. POSIX lexing with bitcoded derivatives. In A. Naumowicz and R. Thiemann, editors, 14th International Conference on Interactive Theorem Proving, number 26 in LIPICS, pages 26:1-26:18. Dagstuhl Publishing, 2023. URL: https://doi.org/10.4230/LIPICS.ITP.2023.27.
  28. Christian Urban. POSIX lexing with derivatives of regular expressions. Journal of Automated Reasoning, 67:1-24, July 2023. URL: https://doi.org/10.1007/s10817-023-09667-1.
  29. Ian Erik Varatalu, Margus Veanes, and Juhan Ernits. RE#: High performance derivative-based regex matching with intersection, complement, and restricted lookarounds. Proc. ACM Program. Lang., 9(POPL), January 2025. URL: https://doi.org/10.1145/3704837.
  30. Margus Veanes, Thomas Ball, Gabriel Ebner, and Ekaterina Zhuchko. Symbolic automata: Omega-regularity modulo theories. Proc. ACM Program. Lang., 9(POPL), January 2025. URL: https://doi.org/10.1145/3704838.
  31. Ekaterina Zhuchko. Lean sources for this paper, 2025. URL: https://github.com/ezhuchko/finiteness-derivatives.
  32. Ekaterina Zhuchko, Margus Veanes, and Gabriel Ebner. Lean formalization of extended regular expression matching with lookarounds. In Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP '24), pages 279-292. ACM, 2024. URL: https://doi.org/10.1145/3636501.3636959.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact