On Regular Expression Proof Complexity

Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10396)

Abstract

We investigate the proof complexity of Salomaa’s axiom system $$F_1$$ for regular expression equivalence. We show that for two regular expression E and F over the alphabet $$\varSigma$$ with $$L(E)=L(F)$$ an equivalence proof of length $$O\left( |\varSigma |^4\cdot \textsc {Tower}(\max \{h(E),h(F)\}+4)\right)$$ can be derived within $$F_1$$, where h(E) (h(F), respectively) refers to the height of E (F, respectively) and the tower function is defined as $$\textsc {Tower}(1)=2$$ and $$\textsc {Tower}(k+1)=2^{\textsc {Tower}(k)}$$, for $$k\ge 1$$. In other words This is in sharp contrast to the fact, that regular expression equivalence admisses exponential proof length if not restricted to the axiom system $$F_1$$. From the theoretical point of view the exponential proof length seems to be best possible, because we show that regular expression equivalence admits a polynomial bounded proof if and only if $$\textsf {NP}=\textsf {PSPACE}$$.

References

1. 1.
Brzozowski, J.A.: Canonical regular expressions and minimal state graphs for definite events. In: Mathematical Theory of Automata. MRI Symposia Series, vol. 12, pp. 529–561. Polytechnic Press, New York (1962)Google Scholar
2. 2.
Cook, S.A., Reckhow, R.A.: The relative efficiency of propositional proof systems. J. Symb. Logic 44(1), 36–50 (1979)
3. 3.
Ginzburg, A.: A procedure of checking equality of regular expressions. J. ACM 14(2), 355–362 (1967)
4. 4.
Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages and Computation. Addison-Wesley, Boston (1979)
5. 5.
Hunt, H.B., Rosenkrantz, D.J., Szymanski, T.G.: On the equivalence, containment, and covering problems for the regular and context-free languages. J. Comput. System Sci. 12, 222–268 (1976)
6. 6.
Kleene, S.C.: Representation of events in nerve nets and finite automata. In: Shannon, C.E., McCarthy, J. (eds.) Automata Studies, Annals of Mathematics Studies, vol. 34, pp. 2–42. Princeton University Press, Princeton (1956)Google Scholar
7. 7.
McNaughton, R., Yamada, H.: Regular expressions and state graphs for automata. IRE Trans. Electron. Comput. EC–9(1), 39–47 (1960)
8. 8.
Salomaa, A.: Two complete axiom systems for the algebra of regular events. J. ACM 13(1), 158–169 (1966)
9. 9.
Stockmeyer, L.J., Meyer, A.R.: Word problems requiring exponential time. In: Proceedings of the 5th Symposium on Theory of Computing, pp. 1–9 (1973)Google Scholar 