EREQ: Regular Expressions with Quantifiers and Incremental Quantifier Elimination
summary
Introduces Extended Regular Expressions with Quantifiers (EREQ) that translate wMSO to a regex-like formalism via a linear-time translation and eliminate quantifiers incrementally by symbolic derivatives that distribute over quantifiers. Core theory proves finite derivative closure and is verified in Lean. Implementation uses multi-terminal BDDs, is implemented in Rust, and competes with MONA on 10,000 random benchmarks while solving all 50 structured instances (MONA solves 30), trading MONA’s BDD-space failures for timeouts on some cases.
AI-written summary · about
chapters (17)
- 0:00EREQ introduction
- 0:22Cloud storage traces example
- 1:48Unified specification formalism
- 2:31Weak MSO logic limits
- 3:35Classical weak MSO decision
- 4:59ERQ and symbolic derivatives
- 6:01Alphabet extension semantics
- 8:56Atomic formulas to regexes
- 10:20Derivative properties
- 11:44Quantifier elimination
- 13:10Decision procedure proof
- 13:52Benchmarks evaluation
- 15:16Structured benchmarks Mona
- 16:43Summary and future work
- 18:09Q&A: Data structures BDD
- 19:13Q&A: Lazy automata vs derivatives
- 20:59Q&A: Complement propagation
related talks
29mVerified and Efficient Matching of Regular Expressions with Lookaround
37mAll About Regular Expressions
15mEquality Saturation Theory Exploration à la Carte
24mSolving String Constraints with Regex-Dependent Functions through Transducers wi
51mRegular Expressions in C++, Present and Future
19meqsat: An Equality Saturation Dialect for Non-destructive Rewriting
29mMechanized monadic equational reasoning for ML references
27mLightweight Semantics Engineering with Redex