Email Gateway (Aug 19 2022 at 14:33): Email Gateway (Aug 19 2022 at 14:33):From: Tobias Nipkow <nipkow@in.tum.de>
Regular Algebras
Simon Foster and Georg Struth
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.
http://afp.sourceforge.net/entries/Regular_Algebras.shtml
Enjoy!
Last updated: Apr 25 2024 at 12:23 UTC