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.
- TRAYTEL, D., & NIPKOW, T. (2015). Verified decision procedures for MSO on words based on derivatives of regular expressions. Journal of Functional Programming, 25. https://doi.org/10.1017/s0956796815000246
- author's copy