Lean Formalization of Extended Regular Expression Matching with Lookarounds
Ekaterina Zhuchko, Margus Veanes, Gabriel Ebner
Abstract
We present a formalization of a matching algorithm for extended regular expression matching based on locations and symbolic derivatives which supports intersection, complement and lookarounds and whose implementation mirrors an extension of the recent .NET NonBacktracking regular expression engine. The formalization of the algorithm and its semantics uses the Lean 4 proof assistant. The proof of its correctness is with respect to standard matching semantics.
Topics & Concepts
CorrectnessRegular expressionComputer scienceExpression (computer science)Complement (music)Semantics (computer science)Intersection (aeronautics)Programming languageMatching (statistics)Pattern matchingExtension (predicate logic)Theoretical computer scienceOperational semanticsMathematicsGeneBiochemistryPhenotypeComplementationStatisticsChemistryAerospace engineeringEngineeringLogic, programming, and type systemsService-Oriented Architecture and Web ServicesNatural Language Processing Techniques