Abstract
We present a formal constructive theory of regular languages consisting of about 1400 lines of Coq/Ssreflect. As representations we consider regular expressions, deterministic and nondeterministic automata, and Myhill and Nerode partitions. We construct computable functions translating between these representations and show that equivalence of representations is decidable. We also establish the usual closure properties, give a minimization algorithm for DFAs, and prove that minimal DFAs are unique up to state renaming. Our development profits much from Ssreflect’s support for finite types and graphs.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Asperti, A.: A compact proof of decidability for regular expression equivalence. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 283–298. Springer, Heidelberg (2012)
Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.): TPHOLs 2009. LNCS, vol. 5674. Springer, Heidelberg (2009)
Berghofer, S., Reiter, M.: Formalizing the logic-automaton connection. In: Berghofer, et al. (eds.) [2], pp. 147–163
Braibant, T., Pous, D.: Deciding kleene algebras in coq. Logical Methods in Computer Science 8(1) (2012)
Constable, R.L., Jackson, P.B., Naumov, P., Uribe, J.C.: Constructively formalizing automata theory. In: Plotkin, G.D., Stirling, C., Tofte, M. (eds.) Proof, Language, and Interaction, pp. 213–238. The MIT Press (2000)
Coquand, T., Siles, V.: A decision procedure for regular expression equivalence in type theory. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol. 7086, pp. 119–134. Springer, Heidelberg (2011)
Doczkal, C., Kaiser, J.O., Smolka, G.: Formalization accompanying this paper, http://www.ps.uni-saarland.de/extras/cpp13/
Garillot, F., Gonthier, G., Mahboubi, A., Rideau, L.: Packaging mathematical structures. In: Berghofer, et al. (eds.) [2], pp. 327–342
Gonthier, G., Mahboubi, A., Tassi, E.: A Small Scale Reflection Extension for the Coq system. Rapport de recherche RR-6455, INRIA (2008), http://hal.inria.fr/inria-00258384
Hopcroft, J.E., Motwani, R., Ullman, J.D.: Introduction to automata theory, languages, and computation - international edition, 2nd edn. Addison-Wesley (2001)
Huffman, D.: The synthesis of sequential switching circuits. Journal of the Franklin Institute 257(3), 161–190 (1954)
Kleene, S.C.: Representation of events in nerve nets and finite automata. In: Shannon, McCarthy (eds.) [19], pp. 3–42
Kozen, D.: Automata and computability. Undergraduate texts in computer science. Springer (1997)
Krauss, A., Nipkow, T.: Proof pearl: Regular expression equivalence and relation algebra. J. Autom. Reasoning 49(1), 95–106 (2012)
Moore, E.F.: Gedanken-experiments on sequential machines. In: Shannon, McCarthy (eds.) [19], pp. 129–153
Myhill, J.R.: Finite Automata and the Representation of Events. Tech. Rep. WADC TR-57-624, Wright-Paterson Air Force Base (1957)
Nerode, A.: Linear automaton transformations. Proceedings of the American Mathematical Society 9(4), 541–544 (1958)
Rabin, M.O., Scott, D.: Finite automata and their decision problems. IBM J. Res. Dev. 3(2), 114–125 (1959)
Shannon, C., McCarthy, J. (eds.): Automata Studies. Princeton University Press (1956)
The Coq Development Team: http://coq.inria.fr
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer International Publishing Switzerland
About this paper
Cite this paper
Doczkal, C., Kaiser, JO., Smolka, G. (2013). A Constructive Theory of Regular Languages in Coq. In: Gonthier, G., Norrish, M. (eds) Certified Programs and Proofs. CPP 2013. Lecture Notes in Computer Science, vol 8307. Springer, Cham. https://doi.org/10.1007/978-3-319-03545-1_6
Download citation
DOI: https://doi.org/10.1007/978-3-319-03545-1_6
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-03544-4
Online ISBN: 978-3-319-03545-1
eBook Packages: Computer ScienceComputer Science (R0)