Author here - I don't think this is an issue. If you don't use submatching, you can just compute the minimal DFAs and compare them to test for equivalence, and

Author here - I don't think this is an issue. If you don't use submatching, you can just compute the minimal DFAs and compare them to test for equivalence, and you don't even need negation. Thus, introducing negation can't do any harm there. But as I generate Mealy machines for submatching, which can't be minimised, we need another approach. Knowing that A - B = A ∧ ¬B, one can produce a DFA for (A - B) ∨ (B - A), and if it has no accepting states, then A and B must be equivalent, as nothing can match one but not both. But DFA construction is O(2ⁿ), even if one takes the RE → NFA → DFA route, so this is nothing new complexity-wise. Such a decision procedure is never used in a derivative-based regex implementation, anyway. The equivalence of regular expressions only needs to be approximated, and the approximation consists of some structural rules (see Definition 4.1 of [1]). Relatively few rules are needed to guarantee that a _finite_ machine can be generated, and only a dozen rules are required to get very close to a minimal DFA (table 1, page 14 of [1]). So having the possibility of writing a precise regex equivalence function is completely irrelevant to producing an efficient regex engine. A decision procedure is handy, but you can write one for submatch-less regexes without negation, the complexity of such a procedure is typical for DFA construction, and the problem of deciding if two regular expressions are equivalent is irrelevant. [1] Regular-expression derivatives reexamined https://www.ccs.neu.edu/home/turon/re-deriv.pdf https://www.ccs.neu.edu/home/turon/re-deriv.pdf