Regular Algebras

Title:	Regular Algebras
Authors:	Simon Foster and Georg Struth
Submission date:	2014-05-21
Abstract:	Regular algebras axiomatise the equational theory of regular expressions as induced by regular language identity. We use Isabelle/HOL for a detailed systematic study of regular algebras given by Boffa, Conway, Kozen and Salomaa. We investigate the relationships between these classes, formalise a soundness proof for the smallest class (Salomaa's) and obtain completeness of the largest one (Boffa's) relative to a deep result by Krob. In addition we provide a large collection of regular identities in the general setting of Boffa's axiom. Our regular algebra hierarchy is orthogonal to the Kleene algebra hierarchy in the Archive of Formal Proofs; we have not aimed at an integration for pragmatic reasons.
BibTeX:	@article{Regular_Algebras-AFP, author = {Simon Foster and Georg Struth}, title = {Regular Algebras}, journal = {Archive of Formal Proofs}, month = may, year = 2014, note = {\url{http://isa-afp.org/entries/Regular_Algebras.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	Kleene_Algebra
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.