2026-08-17T10:52:34Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:24614 2025-12-12T15:09:59Z ddc:004 open_access

Finiteness of Symbolic Derivatives in Lean Zhuchko, Ekaterina Maarand, Hendrik Veanes, Margus Ebner, Gabriel Lean regular languages lookarounds derivatives finiteness 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Ekaterina Zhuchko and Hendrik Maarand and Margus Veanes and Gabriel Ebner 2025 Is Part Of LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2025.16 urn:nbn:de:0030-drops-246144 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.16 eng https://creativecommons.org/licenses/by/4.0/legalcode