Proof Pearl: Regular Expression Equivalence and Relation Algebra
We describe and verify an elegant equivalence checker for regular
expressions. It works by constructing a bisimulation relation between
(derivatives of) regular expressions. By mapping regular expressions
to binary relations, an automatic and complete proof method for
(in)equalities of binary relations over union, composition and
(reflexive) transitive closure is obtained.
pdf
BibTeX:
@article{Krauss-Nipkow-JAR,author={Alexander Krauss and Tobias Nipkow},
title={Proof Pearl: Regular Expression Equivalence and Relation Algebra},
journal={J. Automated Reasoning},volume=49,pages={95--106},year=2012,note={published online March 2011}}
The corresponding
Isabelle theories.