Myhill-Nerode
A formalisation of the Myhill-Nerode theorem based on regular expressions. 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.
Keywords for this software
References in zbMATH (referenced in 10 articles , 1 standard article )
Showing results 1 to 10 of 10.
Sorted by year (- Abdulaziz, Mohammad; Norrish, Michael; Gretton, Charles: Formally verified algorithms for upper-bounding state space diameters (2018)
- Doczkal, Christian; Smolka, Gert: Regular language representations in the constructive type theory of Coq (2018)
- Doczkal, Christian; Smolka, Gert: Two-way automata in Coq (2016)
- Foster, Simon; Struth, Georg: On the fine-structure of regular algebra (2015)
- Traytel, Dmitriy; Nipkow, Tobias: Verified decision procedures for MSO on words based on derivatives of regular expressions (2015)
- Wu, Chunhan; Zhang, Xingyuan; Urban, Christian: A formalisation of the Myhill-Nerode theorem based on regular expressions (2014)
- Nipkow, Tobias; Haslbeck, Maximilian: A brief survey of verified decision procedures for equivalence of regular expressions (2013)
- Armstrong, Alasdair; Struth, Georg: Automated reasoning in higher-order regular algebra (2012)
- Coquand, Thierry; Siles, Vincent: A decision procedure for regular expression equivalence in type theory (2011)
- Wu, Chunhan; Zhang, Xingyuan; Urban, Christian: A formalisation of the Myhill-Nerode theorem based on regular expressions (proof pearl) (2011)