Unified Decision Procedures for Regular Expression Equivalence
We formalize a unified framework for verified decision procedures for regular
expression equivalence. Five recently published formalizations of such
decision procedures (three based on derivatives, two on marked regular
expressions) can be obtained as instances of the framework. We discover that
the two approaches based on marked regular expressions, which were previously
thought to be the same, are different, and one seems to produce uniformly
smaller automata. The common framework makes it possible to compare the
performance of the different decision procedures in a meaningful way.
pdf
BibTeX:
@inproceedings{NipkowT-ITP14,
author={Tobias Nipkow and Dmitriy Traytel},
title={Unified Decision Procedures for Regular Expression Equivalence},
booktitle={Interactive Theorem Proving (ITP 2014)},
editor={R. Gamboa and G. Klein},
publisher=Springer,series=LNCS,volume={8558},pages={450-466},year=2014}
Isabelle theories in the
Archive of Formal Proofs