Myhill-Nerode (Q40261)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry Myhill-Nerode
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Myhill-Nerode |
AFP entry Myhill-Nerode |
Statements
Chunhan Wu
0 references
Xingyuan Zhang
0 references
Christian Urban
0 references
Manuel Eberl
0 references
There are many proofs of the Myhill-Nerode theorem using automata. In this library we give a proof entirely based on regular expressions, since regularity of languages can be conveniently defined using regular expressions (it is more painful in HOL to define regularity in terms of automata). We prove the first direction of the Myhill-Nerode theorem by solving equational systems that involve regular expressions. For the second direction we give two proofs: one using tagging-functions and another using partial derivatives. We also establish various closure properties of regular languages. Most details of the theories are described in our ITP 2011 paper.
0 references
26 August 2011
0 references
The Myhill-Nerode Theorem Based on Regular Expressions (English)
0 references
