On Regular Expression Proof Complexity

  • Simon Beier
  • Markus HolzerEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10396)


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}\).


  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)MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    Ginzburg, A.: A procedure of checking equality of regular expressions. J. ACM 14(2), 355–362 (1967)CrossRefzbMATHGoogle Scholar
  4. 4.
    Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages and Computation. Addison-Wesley, Boston (1979)zbMATHGoogle Scholar
  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)MathSciNetCrossRefzbMATHGoogle Scholar
  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)CrossRefzbMATHGoogle Scholar
  8. 8.
    Salomaa, A.: Two complete axiom systems for the algebra of regular events. J. ACM 13(1), 158–169 (1966)MathSciNetCrossRefzbMATHGoogle Scholar
  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

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  1. 1.Institut für InformatikUniversität GiessenGiessenGermany

Personalised recommendations