A Decision Procedure for Regular Expression Equivalence in Type Theory

  • Thierry Coquand
  • Vincent Siles
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7086)


We describe and formally verify a procedure to decide regular expressions equivalence: two regular expressions are equivalent if and only if they recognize the same language. Our approach to this problem is inspired by Brzozowski’s algorithm using derivatives of regular expressions, with a new definition of finite sets. In this paper, we detail a complete formalization of Brzozowki’s derivatives, a new definition of finite sets along with its basic meta-theory, and a decidable equivalence procedure correctly proved using Coq and Ssreflect.


Boolean Function Decision Procedure Regular Expression Type Theory Relation Algebra 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Almeida, J.B., Moreira, N., Pereira, D., de Sousa, S.M.: Partial Derivative Automata Formalized in Coq. In: Domaratzki, M., Salomaa, K. (eds.) CIAA 2010. LNCS, vol. 6482, pp. 59–68. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  2. 2.
    Bezem, M., Nakata, K., Uustalu, T.: On streams that are finitely red (submitted, 2011)Google Scholar
  3. 3.
    Braibant, T., Pous, D.: A tactic for deciding Kleene algebras. In: First Coq Workshop (August 2009)Google Scholar
  4. 4.
    Braibant, T., Pous, D.: An Efficient Coq Tactic for Deciding Kleene Algebras. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 163–178. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  5. 5.
    Brzozowski, J.A.: Derivatives of regular expressions. JACM 11(4), 481–494 (1964)MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Büchi, J.R.: Weak second order arithmetica and finite automata. Zeitscrift Fur Mathematische Logic und Grundlagen Der Mathematik 6, 66–92 (1960)CrossRefzbMATHGoogle Scholar
  7. 7.
    The Coq Development Team,
  8. 8.
    Coquand, T., Gonthier, G., Siles, V.: Source code of the formalization,
  9. 9.
    Coquand, T., Spiwack, A.: Constructively finite? In: Laureano Lambán, L., Romero, A., Rubio, J. (eds.) Scientific Contributions in Honor of Mirian Andrés Gómez Servicio de Publicaciones, Universidad de La rioja, Spain (2010)Google Scholar
  10. 10.
    Johnstone, P.: Topos theory. Academic Press (1977)Google Scholar
  11. 11.
    Krauss, A., Nipkow, T.: Proof Pearl: Regular Expression Equivalence and Relation Algebra. Journal of Automated Reasoning (March 2011) (published online)Google Scholar
  12. 12.
    Martin-Löf, P.: An intuitionistic type theory: predicative part. In: Logic Colloquium 1973, pp. 73–118. North-Holland, Amsterdam (1973)Google Scholar
  13. 13.
    Mirkin, B.G.: An algorithm for constructing a base in a language of regular expressions. Engineering Cybernetics 5, 51–57 (1996)Google Scholar
  14. 14.
    Nordström, B.: Terminating general recursion BIT, vol. 28, pp. 605–619 (1988)Google Scholar
  15. 15.
    Owens, S., Reppy, J., Turon, A.: Regular-expression Derivatives Re-examined. Journal of Functional Programming 19(2), 173–190Google Scholar
  16. 16.
    Richman, F., Stolzenberg, G.: Well-Quasi-Ordered sets. Advances in Mathematics 97, 145–153 (1993)MathSciNetCrossRefzbMATHGoogle Scholar
  17. 17.
    Russell, B., Whitehead, A.N.: Principia Mathematica. Cambridge University Press (1910)Google Scholar
  18. 18.
    Gonthier, G., Mahboubi, A.: An introduction to small scale reflection in Coq. Journal of Formalized Reasoning 3(2), 95–152 (2010)MathSciNetzbMATHGoogle Scholar
  19. 19.
    Tarski, A.: Sur les ensembles finis. Fundamenta Mathematicae 6, 45–95 (1924)zbMATHGoogle Scholar
  20. 20.
    Thiemann, R., Sternagel, C.: Certification of Termination Proofs Using CeTA. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 452–468. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  21. 21.
    Wu, C., Zhang, X., Urban, C.: A Formalisation of the Myhill-Nerode Theorem Based on Regular Expressions (Proof Pearl). In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol. 6898, pp. 341–356. Springer, Heidelberg (2011)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Thierry Coquand
    • 1
  • Vincent Siles
    • 1
  1. 1.University of GothenburgSweden

Personalised recommendations