×
Wu, Chunhan; Zhang, Xingyuan; Urban, Christian

A formalisation of the Myhill-Nerode theorem based on regular expressions. (English) Zbl 1314.68179

J. Autom. Reasoning 52, No. 4, 451-480 (2014).
Summary: There are numerous textbooks on regular languages. Many of them focus on finite automata for proving properties. Unfortunately, automata are not so straightforward to formalise in theorem provers. The reason is that natural representations for automata are graphs, matrices or functions, none of which are inductive datatypes. Regular expressions can be defined straightforwardly as a datatype and a corresponding reasoning infrastructure comes for free in theorem provers. We show in this paper that a central result from formal language theory – the Myhill-Nerode Theorem – can be recreated using only regular expressions. From this theorem many closure properties of regular languages follow.

Cited in 6 Documents

MSC:

68Q45 Formal languages and automata
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)

Keywords:

regular languages; theorem provers; Myhill-Nerode theorem

Software:

Myhill-Nerode; Presburger Automata; Archive Formal Proofs; Gauss Jordan Elimination; Regular Sets
Cite Review PDF
Full Text: DOI

References:

[1] Almeida, J.B., Moriera, N., Pereira, D., de Sousa, S.M.: Partial derivative automata formalized in Coq. In: Proceedings of the 15th International Conference on Implementation and Application of Automata, vol. 6482, pp. 59-68. LNCS (2010) · Zbl 1297.68214
[2] Antimirov, V.: Partial derivatives of regular expressions and finite automata constructions. Theor. Comput. Sci. 155, 291-319 (1995) · Zbl 0872.68120 · doi:10.1016/0304-3975(95)00182-4
[3] Asperti, A.: A compact proof of decidability for regular expression equivalence. In: Proceedings of the 3rd International Conference on Interactive Theorem Proving, vol. 7406, pp. 283-298. LNCS (2012) · Zbl 1360.68738
[4] Berghofer, S., Nipkow, T.: Executing higher order logic. In: Proceedings of the International Workshop on Types for Proofs and Programs, vol. 2277, pp. 24-40. LNCS (2002) · Zbl 1054.68133
[5] Berghofer, S., Reiter, M.: Formalizing the logic-automaton connection. In: Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, vol. 5674, pp. 147-163. LNCS (2009) · Zbl 1252.68250
[6] Braibant, T.: Kleene Algebras, Rewriting Modulo AC, and and Circuits in Coq. Ph.D. thesis, University of Grenoble (2012) · Zbl 0225.94044
[7] Brzozowski, J.A.: Derivatives of regular expressions. J. ACM 11(4), 481-494 (1964) · Zbl 0225.94044 · doi:10.1145/321239.321249
[8] Church, A.: A formulation of the simple theory of types. J. Symb. Log. 5(2), 56-68 (1940) · JFM 66.1192.06 · doi:10.2307/2266170
[9] Constable, R.L., Jackson, P.B., Naumov, P., Uribe, J.C.: Constructively formalizing automata theory. In: Proof, Language, and Interaction, pp. 213-238. MIT Press (2000) · JFM 66.1192.06
[10] Coquand, T., Siles, V.: A decision procedure for regular expression equivalence in type theory. In: Proceedings of the 1st Conference on Certified Programs and Proofs, vol. 7086, pp. 119-134. LNCS (2011) · Zbl 1350.68228
[11] Doczkal, C., Kaiser, J.O., Smolka, G.: A Constructive Theory of Regular Languages in Coq. Accepted for publication. In: Proceedings of the 3rd International Conference on Certified Programs and Proofs. (2013) · Zbl 1426.68143
[12] Fenner, S.A., Gasarch, W.I., Postow, B.: The complexity of finding SUBSEQ(A). Theor. Comput. Syst. 45(3), 577-612 (2009) · Zbl 1187.68295 · doi:10.1007/s00224-008-9111-4
[13] Filliâtre, J.-C.: Finite automata theory in Coq: a constructive proof of Kleene’s Theorem. Research Report 97-04, LIP - ENS Lyon (1997) · Zbl 1187.68295
[14] Fortnow, L., Gasarch, W.I.: Proving DFA-Langs Closed Under Concat and * Without Using Equiv to NDFA’s. Retrieved today, from http://blog.computationalcomplexity.org (2013) · Zbl 1163.68317
[15] Gelade, W., Neven, F.: Succinctness of the complement and intersection of regular expressions. ACM Trans. Comput. Log. 13(1), 4:1-4:21 (2012) · Zbl 1351.68139 · doi:10.1145/2071368.2071372
[16] Haftmann, F.: Code Generation from Specifications in Higher-Order Logic. Ph.D. thesis, Technical University of Munich (2009) · Zbl 1107.68427
[17] Haines, L.H.: On free monoids partially ordered by embedding. J. Comb. Theor. 6, 94-98 (1969) · Zbl 0224.20065 · doi:10.1016/S0021-9800(69)80111-0
[18] Harper, R.: Proof-directed debugging. J. Funct. Program. 9(4), 463-469 (1999) · Zbl 0948.68038 · doi:10.1017/S0956796899003378
[19] Hopcroft, J.E., Ullman, J.D.: Formal Languages and Their Relation to Automata. Addison-Wesley, Reading (1969) · Zbl 0196.01701
[20] Kozen, D.: Automata and Computability. Springer, New York (1997) · Zbl 0883.68055 · doi:10.1007/978-1-4612-1844-9
[21] Krauss, A., Nipkow, T.: Proof pearl: regular expression equivalence and relation algebra. J. Autom. Reason. 49(1), 95-106 (2012) · Zbl 1269.68090 · doi:10.1007/s10817-011-9223-4
[22] Lammich, P., Tuerk, T.: Applying data refinement for monadic programs to Hopcroft’s Algorithm. In: Proceedings of the 3rd International Conference on Interactive Theorem Proving, vol. 7406, pp. 166-182. LNCS (2012) · Zbl 1360.68757
[23] Nipkow, T.: Verified lexical analysis. In: Proceedings of the 11th International Conference on Theorem Proving in Higher Order Logics, vol. 1479, pp. 1-15. LNCS (1998)
[24] Nipkow, T.: Gauss-Jordan elimination for matrices represented as functions. In: Klein, G., Nipkow, T., Paulson, L. (eds.) The Archive of Formal Proofs, http://afp.sourceforge.net/entries/Gauss-Jordan-Elim-Fun.shtml. Formal proof development, 2011
[25] Owens, S., Reppy, J., Turon, A.: Regular-expression derivatives re-examined. J. Funct. Program. 19(2), 173-190 (2009) · Zbl 1163.68317 · doi:10.1017/S0956796808007090
[26] Owens, S., Slind, K.: Adapting functional programs to higher order logic. Higher-Order Symb. Comput. 21(4), 377-409 (2008) · Zbl 1175.68103 · doi:10.1007/s10990-008-9038-0
[27] Rosenberg, A.L.: A Big Ideas Approach to the Theory of Computation. Course notes for CMPSCI 401 at the University of Massachusetts (2006)
[28] Sakarovitch, J.: Elements of Automata Theory. Cambridge University Press, Cambridge (2009) · Zbl 1188.68177 · doi:10.1017/CBO9781139195218
[29] Shallit, J.: A Second Course in Formal Languages and Automata Theory. Cambridge University Press, Cambridge (2008) · Zbl 1163.68025 · doi:10.1017/CBO9780511808876
[30] Sternagel, C.: Certified kruskals tree theorem. Accepted for publication In: Proceedings of the 3rd International Conference on Certified Programs and Proofs. (2013) · Zbl 1426.68288
[31] Sulzmann, M., Lu, K.Z.M.: Regular expression sub-matching using partial derivatives. In: Proceedings of the 14th Symposium on Principles and Practice of Declarative Programming (PPDP), pp. 79-90. ACM (2012)
[32] Wu, C., Zhang, X., Urban, C.: A formalisation of the Myhill-Nerode theorem based on regular expressions (Proof Pearl). In: Proceedings of the 2nd International Conference on Interactive Theorem Proving, vol. 6898, pp. 341-356. LNCS (2011) · Zbl 1342.68306
[33] Wu, C., Zhang, X., Urban, C.: The Myhill-Nerode theorem based on regular expressions. In: Klein, G., Nipkow, T., Paulson, L. (eds) The Archive of Formal Proofs, http://afp.sourceforge.net/entries/Myhill-Nerode.shtml. Formal proof development, 2011 · Zbl 1342.68306
[34] Yi, K.: Educational pearl: Proof-Directed Debugging revisited for a first-order version. J. Funct. Program. 16(6), 663-670 (2006) · Zbl 1107.68427 · doi:10.1017/S0956796806006149
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.