Abstract
This is a library of constructions on regular expressions and languages. It provides the operations of concatenation, Kleene star and derivative on languages. Regular expressions and their meaning are defined. An executable equivalence checker for regular expressions is verified; it does not need automata but works directly on regular expressions. By mapping regular expressions to binary relations, an automatic and complete proof method for (in)equalities of binary relations over union, concatenation and (reflexive) transitive closure is obtained.
Extended regular expressions with complement and intersection are also defined and an equivalence checker is provided.
License
History
- May 10, 2012
- Tobias Nipkow added equivalence checking with partial derivatives
- August 26, 2011
- Christian Urban added a theory about derivatives and partial derivatives of regular expressions
Topics
Related publications
- Krauss, A., & Nipkow, T. (2011). Proof Pearl: Regular Expression Equivalence and Relation Algebra. Journal of Automated Reasoning, 49(1), 95–106. https://doi.org/10.1007/s10817-011-9223-4
- author's copy
Session Regular-Sets
- Regular_Set
- Regular_Exp
- NDerivative
- Equivalence_Checking
- Relation_Interpretation
- Regexp_Method
- Regexp_Constructions
- Derivatives
- pEquivalence_Checking
- Regular_Exp2
- Equivalence_Checking2
Used by
- Isabelle/DOF
- The number of comparisons in QuickSort
- Formalization of Knuth–Bendix Orders for Lambda-Free Higher-Order Terms
- POSIX Lexing with Derivatives of Regular Expressions
- Analysis of List Update Algorithms
- Finite Automata in Hereditarily Finite Set Theory
- Unified Decision Procedures for Regular Expression Equivalence
- A Codatatype of Formal Languages
- Light-weight Containers
- Executable Transitive Closures
- The Myhill-Nerode Theorem Based on Regular Expressions
- Abstract Rewriting
- Functional Automata