Lean Formalization of Extended Regular Expression Matching with Lookarounds
summary
Formalizes an extended regular‑expression matcher in Lean 4 formalization that models predicates with an effective Boolean algebra, represents positions as locations and spans, and implements a derivative‑based engine mirroring the .NET NonBacktracking approach. Proves correctness and completeness of a leftmost‑longest matching algorithm, gives a custom termination metric (lookaround depth, remaining string, regex size), handles intersection, complement and lookarounds, and notes linear-time guarantees only hold when lookaround length is bounded.
AI-written summary · about
chapters (22)
- 0:00Introduction
- 0:26Formalizing extended regex
- 1:29Anchors in regex rules
- 2:53Derivatives and lookarounds
- 3:58Symbolic regex and Boolean algebra
- 5:42Extended symbolic regular expressions with lookarounds
- 6:44Reversal operation on regular expressions
- 7:28Lookaround context
- 8:09String traversal with zippers
- 9:13Match boundaries with spans
- 10:39Match semantics
- 13:18Classical regex derivatives
- 14:43Derivative in Lean
- 16:29Nullability and termination
- 17:56Nullable points
- 19:01Leftmost longest match
- 20:06Match helper functions
- 21:35Algorithm correctness
- 22:36Future work
- 24:06Questions and answers on algorithm complexity
- 25:34Lookaround restrictions
- 26:18Functional vs imperative
related talks
23mSpecifying and Verifying Future Conditions
26mUnfolding Expressions for Gradual Verification
21mExact Loop Bound Analysis
20mOn Extending Incorrectness Logic with Backwards Reasoning
13mEncode the $\forall\exists$ Relational Hoare Logic into Standard Hoare Logic
26mTowards Efficient Model Comparison Using Automated Program Rewriting
46mKeynote: Formal Verification? No, Formal Reasoning!
20mFormal framework for reasoning about the precision of dynamic analysis