Personal tools
You are here: Home Events LFCS Seminars-Folder LFCS Seminar: Christian Urban

LFCS Seminar: Christian Urban

— filed under:

Formalising Regular Language Theory with Regular Expressions

  • LFCS Seminar
When Feb 21, 2012
from 04:00 PM to 05:00 PM
Add event to calendar vCal

There are numerous textbooks on regular languages. Nearly all of them introduce the subject by describing finite automata and only mentioning on the side a connection with regular expressions. Unfortunately, automata are difficult to formalise in theorem provers. The reason is that they need to be represented as graphs, matrices or functions, none of which are inductive datatypes. Also convenient operations for disjoint unions of graphs, matrices and functions are not easily formalisiable. In contrast, regular expressions can be defined conveniently as a datatype and a corresponding reasoning infrastructure comes for free. I will show in this talk 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. We can also derive a simple regular expression matcher.

Document Actions