| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
The Myhill-Nerode Theorem Based on Regular Expressions
| Title: | The Myhill-Nerode Theorem Based on Regular Expressions |
| Authors: | Chunhan Wu, Xingyuan Zhang and Christian Urban |
| Submission date: | 2011-08-26 |
| Abstract: | 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. |
| BibTeX: |
@article{Myhill-Nerode-AFP,
author = {Chunhan Wu and Xingyuan Zhang and Christian Urban},
title = {The Myhill-Nerode Theorem Based on Regular Expressions},
journal = {Archive of Formal Proofs},
month = aug,
year = 2011,
note = {\url{http://isa-afp.org/entries/Myhill-Nerode.shtml},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
| Depends on: | Regular-Sets, Well_Quasi_Orders |
| Status: [skipped] | This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |
Older releases:
|