[Club2] Title and abstract for Talk on 17 November

[Christian Urban]

Dear All,

Below is the title and abstract for my Club2 talk on 
regular expressions on Wednesday 17th November.

Best wishes,
Christian


--------------------------------------

A Formalisation of the Myhill-Nerode Theorem based
on Regular Expressions

There are countless textbooks on regular languages. Nearly 100% 
of them introduce the subject by describing finite automata and 
only mentioning on the side a connection with regular expressions. 
Unfortunately, automata are a hassle for formalisations. The 
reason is that in full generality they need to be represented as 
graphs or matrices, neither of which can be easily defined as 
datatype. In contrast, regular expressions can be defined easily 
as datatype and a corresponding reasoning infrastructure comes for 
free. We show in this talk that a central result from formal 
language theory - the Myhill-Nerode theorem - can be recreated 
using only regular expressions. This will involve ideas from term 
rewriting and unification theory. The Myhill-Nerode theorem provides 
necessary and sufficient conditions for a language to be regular.


This is joint work with Chunhan Wu and Xingyuan Zhang
(who I visited over the summer in Nanjing). The work was 
partly inspired by two nice functional pearls by Harper
and by Yi.