King's College London

Research portal

A formalisation of the myhill-nerode theorem based on regular expressions

Research output: Contribution to journalArticle

Chunhan Wu, Xingyuan Zhang, Christian Urban

Original languageEnglish
Pages (from-to)451-480
Number of pages30
JournalJOURNAL OF AUTOMATED REASONING
Volume52
Issue number4
DOIs
Publication statusPublished - 25 Jan 2014

King's Authors

Abstract

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. 

View graph of relations

© 2018 King's College London | Strand | London WC2R 2LS | England | United Kingdom | Tel +44 (0)20 7836 5454