Decision procedures for regular expression equivalence have been formalized before, usually based on Brzozowski derivatives. Yet, for a straightforward embedding of MSO formulas into regular expressions an extension of regular expressions with a projection operation is required. We prove total correctness and completeness of an equivalence checker for regular expressions extended in that way. We also define a language-preserving translation of formulas into regular expressions with respect to two different semantics of MSO. Our results have been formalized and verified in the theorem prover Isabelle. Using Isabelle's code generation facility, this yields purely functional, formally verified programs that decide equivalence of MSO formulas.
BibTeX:
@article{TraytelN-JFP15, author={Dmitriy Traytel and Tobias Nipkow}, title={Verified Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions}, journal={Journal of Functional Programming}, volume=25,year=2015}Isabelle theories in the Archive of Formal Proofs
This is an extended version of this conference paper.