Algebras of languages
We investigate the equational theory of reversible Kleene lattices, that is algebras of languages with the regular operations (union, composition and Kleene star), together with the intersection and mirror image. Building on results by Andréka, Mikulás and Németi from 2011, we construct the free representation of this algebra. We then provide an automaton model to compare representations. These automata are adapted from Petri automata, which we introduced with Pous in 2015 to tackle a similar problem for algebras of binary relations. This allows us to show that testing the validity of equations in this algebra is decidable, and in fact ExpSpace-complete. We also provide a complete set of axioms for the equational theory of these algebras, which was developed in the proof assistant Coq.
Related documents
Coq proof | ||
| Sources on Bitbucket | ||
| Documentation | ||
Related papers | ||
| A Complete Axiomatisation of a Fragment of Language Algebra (in CSL 2020) | More | |
| Reversible Kleene lattices (in MFCS 2017) | More | |
Related talks | ||
|
A complete axiomatisation of a fragment of language algebra
CSL
in Barcelona,
January 2020
.
|
More | |
|
The theory of languages
Highlights
in London,
September 2017
.
|
More | |
|
The Equational Theory of Algebras of Languages
BLAST
in Nashville,
August 2017
.
|
More | |
|
The Equational Theory of Algebras of Languages
RAMiCS
in Lyon,
May 2017
(Special session on mechanised reasoning)
.
|
More | |
|
The Equational Theory of Algebras of Languages
PPLV Seminar
in London,
April 2017
.
|
More | |