Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Journal of Automated Reasoning
Erschienen in: Journal of Automated Reasoning 1-4/2018

10.03.2018

Regular Language Representations in the Constructive Type Theory of Coq

verfasst von: Christian Doczkal, Gert Smolka

Erschienen in: Journal of Automated Reasoning | Ausgabe 1-4/2018

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

We explore the theory of regular language representations in the constructive type theory of Coq. We cover various forms of automata (deterministic, nondeterministic, one-way, two-way), regular expressions, and the logic WS1S. We give translations between all representations, show decidability results, and provide operations for various closure properties. Our results include a constructive decidability proof for the logic WS1S, a constructive refinement of the Myhill-Nerode characterization of regularity, and translations from two-way automata to one-way automata with verified upper bounds for the increase in size. All results are verified with an accompanying Coq development of about 3000 lines.
Vorheriger Artikel Formally Verified Algorithms for Upper-Bounding State Space Diameters

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren
Anhänge
Nur mit Berechtigung zugänglich
Fußnoten
1
Here, abstract means that no witness can be extracted from the existence proof. The function \(\mathsf {xchoose}_X\) computes a witness by enumerating elements of X. The proof argument is only used to guarantee termination.
 
2
The language \(L := \{\,a^nb^m\,\big |\,\text {The} n-\text {th Turing machine holds within m steps on input} \varepsilon \,\}\) is decidable, but the image of L under the homomorphism mapping a to a and b to \(\varepsilon \) is undecidable.
 
3
In [24], \({\hat{\delta }}\,\) is defined recursively starting from the right end of the word. In Coq, structural recursion is more natural and the impact on the proofs appears to be minimal.
 
4
Wu et al. [42] derive the closure of regular expressions under complement by proving the Myhill–Nerode theorem using regular expressions. The proof is significantly more complex than the automata constructions.
 
5
That the transitive closure of a decidable relation is decidable is established in the Ssreflect libraries using depth-first search.
 
Literatur
1.
2.
Berghofer, S., Reiter, M.: Formalizing the logic-automaton connection. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) Theorem Proving in Higher Order Logics (TPHOLs 2009). LNCS, vol. 5674, pp. 147–163. Springer (2009)
3.
Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.): Interactive Theorem Proving—4th International Conference, ITP 2013, Rennes, France, July 22–26, 2013. Proceedings, LNCS, vol. 7998. Springer (2013)
4.
Braibant, T., Pous, D.: Deciding kleene algebras in Coq. Log. Methods. Comput. Sci. 8(1:16), 1–42 (2012)MathSciNetMATH
5.
6.
Büchi, J.R.: Weak second-order arithmetic and finite automata. Zeitschr. f. math. Logic und Grundladen d. Math. 6, 66–92 (1960)MathSciNetCrossRefMATH
7.
Cohen, C.: Pragmatic quotient types in Coq. In: Blazy et al. [3], pp. 213–228
8.
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, Cambridge (2000)
9.
Coquand, T., Siles, V.: A decision procedure for regular expression equivalence in type theory. In: Jouannaud, J.P., Shao, Z. (eds.) Certified Programs and Proofs (CPP 2011). LNCS, vol. 7086, pp. 119–134. Springer (2011)
10.
11.
Doczkal, C., Kaiser, J., Smolka, G.: A constructive theory of regular languages in Coq. In: Gonthier, G., Norrish, M. (eds.) Certified Programs and Proofs (CPP 2013). LNCS, vol. 8307, pp. 82–97. Springer (2013)
12.
Doczkal, C., Smolka, G.: Two-way automata in Coq. In: Blanchette, J.C., Merz, S. (eds.) Interactive Theorem Proving (ITP 2016). LNCS, vol. 9807, pp. 151–166. Springer (2016)
13.
14.
Filliâtre, J.C.: Finite automata theory in Coq: A constructive proof of kleene’s theorem. Tech. Rep. 97-04, LIP - ENS Lyon (1997)
15.
Gelade, W., Neven, F.: Succinctness of the complement and intersection of regular expressions. ACM Trans. Comput. Logic 13(1), 4:1–4:19 (2012)MathSciNetCrossRefMATH
16.
Gonthier, G., Mahboubi, A., Rideau, L., Tassi, E., Théry, L.: A modular formalisation of finite group theory. In: Schneider, K., Brandt, J. (eds.) Theorem Proving in Higher Order Logics (TPHOLs 2007). LNCS, vol. 4732, pp. 86–101. Springer (2007)
17.
Grädel, E., Thomas, W., Wilke, T. (eds.): Automata, logics, and infinite games: a guide to current research [outcome of a Dagstuhl seminar, February 2001], LNCS, vol. 2500. Springer (2002)
18.
19.
Hofmann, M., Lange, M.: Automatentheorie und Logik. eXamen.press, Springer, Berlin (2011)CrossRefMATH
20.
Hopcroft, J.E., Motwani, R., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation - international edition (2. ed). Addison-Wesley, Boston (2001)MATH
21.
Johnsonbaugh, R., Miller, D.P.: Converses of pumping lemmas. In: Austing, R.H., Cassel, L.N., Miller, J.E., Joyce, D.T. (eds.) Proceedings of the 21st SIGCSE Technical Symposium on Computer Science Education, 1990, Washington, DC, USA, 1990. pp. 27–30. ACM (1990)
22.
Khoussainov, B., Nerode, A.: Automata Theory and its Applications. Springer, Berlin (2012)MATH
23.
Kleene, S.C.: Representation of events in nerve nets and finite automata. In: Shannon, C.E., McCarthy, J. (eds.) Automata Studies, pp. 3–42. Princeton University Press, Princeton (1956)
24.
Kozen, D.: Automata and computability. Undergraduate texts in computer science. Springer, Berlin (1997)
25.
Krauss, A., Nipkow, T.: Proof pearl: Regular expression equivalence and relation algebra. J. Autom. Reason. 49(1), 95–106 (2012)MathSciNetCrossRefMATH
26.
Moreira, N., Pereira, D., de Sousa, S.M.: Deciding kleene algebra terms equivalence in Coq. J. Log. Algebr. Methods Program. 84(3), 377–401 (2015)MathSciNetCrossRefMATH
27.
Nipkow, T.: Verified lexical analysis. In: Grundy, J., Newey, M.C. (eds.) Theorem Proving in Higher Order Logics (TPHOLs ’98). LNCS, vol. 1479, pp. 1–15. Springer (1998)
28.
Paulson, L.C.: A formalisation of finite automata using hereditarily finite sets. In: Felty, A.P., Middeldorp, A. (eds.) Automated deduction (CADE-25). LNCS, vol. 9195, pp. 231–245. Springer (2015)
29.
Pighizzini, G.: Two-way finite automata: old and recent results. Fundam. Inform. 126(2–3), 225–246 (2013)MathSciNetMATH
30.
Pous, D.: Kleene algebra with tests and coq tools for while programs. In: Blazy et al. [3], pp. 180–196
31.
32.
Reinhardt, K.: The complexity of translating logic to finite automata. In: Grädel et al. [17], pp. 231–238
33.
Rosenberg, A.L.: State. In: Goldreich, O., Rosenberg, A.L., Selman, A.L. (eds.) Theoretical computer science, essays in memory of Shimon even. LNCS, vol. 3895, pp. 375–398. Springer (2006)
34.
35.
36.
37.
Trakhtenbrot, B.A.: Finite automata and the logic of monadic predicates. Dokl. Akad. Nauk SSSR 140, 326–329 (1961)
38.
Traytel, D., Nipkow, T.: Verified decision procedures for MSO on words based on derivatives of regular expressions. J. Funct. Program. 25, 1–30 (2015)MathSciNetCrossRefMATH
39.
40.
41.
Wu, C., Zhang, X., Urban, C.: A formalisation of the Myhill-Nerode theorem based on regular expressions (proof pearl). In: van Eekelen, M.C.J.D., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) Interactive Theorem Proving (ITP 2011). LNCS, vol. 6898, pp. 341–356. Springer (2011)
42.
Wu, C., Zhang, X., Urban, C.: A formalisation of the Myhill-Nerode theorem based on regular expressions. J. Autom. Reason. 52(4), 451–480 (2014)MathSciNetCrossRefMATH
Metadaten
Titel
Regular Language Representations in the Constructive Type Theory of Coq
verfasst von
Christian Doczkal
Gert Smolka
Publikationsdatum
10.03.2018
Verlag
Springer Netherlands
Erschienen in
Journal of Automated Reasoning / Ausgabe 1-4/2018
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670
DOI
https://doi.org/10.1007/s10817-018-9460-x

Weitere Artikel der Ausgabe 1-4/2018

Journal of Automated Reasoning 1-4/2018 Zur Ausgabe

OriginalPaper

Toward Compositional Verification of Interruptible OS Kernels and Device Drivers

OriginalPaper

Verified iptables Firewall Analysis and Verification

OriginalPaper

The Role of the Mizar Mathematical Library for Interactive Proof Development in Mizar

OriginalPaper

A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality

OriginalPaper

Mechanising a Type-Safe Model of Multithreaded Java with a Verified Compiler

EditorialNotes

Introduction to Milestones in Interactive Theorem Proving