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

Add to your list(s) Download to your calendar using vCal

• Christian Urban (University of Cambridge)
• Tuesday 09 November 2010, 13:00-14:00
• Computer Laboratory, William Gates Building, Room SS03.

If you have a question about this talk, please contact Thomas Tuerk.

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 in existing theorem provers. The reason is that automata need to be represented as graphs or matrices, neither of which can be easily defined as algebraic 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. The work was partly inspired by a nice paper of Scott Owens on regular expression matching.

This talk is part of the Computer Laboratory Automated Reasoning Group Lunches series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computer Laboratory Automated Reasoning Group Lunches
• Computer Laboratory, William Gates Building, Room SS03
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.