Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

As stated in the title, I need a decision procedure for the problem of regular expression equivalence with not. Wikipedia states the problem is in the NONELEMENTARY complexity class. All I really need is link to the paper that describes the problem and its solution. This is NOT a homework problem. I need the procedure for a program static analysis tool.


share|cite|improve this question
The fact that it is in NONELEMENTARY should discourage any attempts to implement the decision procedure... – Aryabhata Mar 16 '11 at 16:42
Crossposted to stackoverflow. – Chris Eagle Mar 16 '11 at 16:51
FOL is semi-decidable but people still write theorem provers. – Tony Johnson Mar 16 '11 at 17:56
But if you're expecting to use nested 'not's, as one might expect if you need to implement this, the stack of two's goes up by the nesting depth. By depth 5 or $2^{65536}$, you're already well beyond the number of particles in the universe. – Mitch Mar 17 '11 at 1:59
The hope is that the nested not's will be avoided, but if they are there, a worst case time will be displayed that will encourage the user to fiddle around with the expression. – Tony Johnson Mar 17 '11 at 12:53
up vote 2 down vote accepted

Stockmeyer and Meyer, "Word problems requiring exponential time", Proc. 5th ACM Symposium on the Theory of Computing, pp 1-9, 1973.

The derivation is fairly intuitive: every negation in the regular expression 'somehow' requires conversion to a DFA, and a lower bound of $\Theta(2^n)$ states guaranteed for conversion. Nest your $\neg$'s and you get a stack of exponentials.

share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.