Regular Algebras

Simon Foster 🌐 and Georg Struth 🌐

May 21, 2014

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

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.

License

BSD License

Topics

Session Regular_Algebras

Depends on

Cite

× 
@article{Regular_Algebras-AFP,
  author  = {Simon Foster and Georg Struth},
  title   = {Regular Algebras},
  journal = {Archive of Formal Proofs},
  month   = {May},
  year    = {2014},
  note    = {\url{https://isa-afp.org/entries/Regular_Algebras.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: