The Equational Theory of Algebras of Languages

RAMiCS in Lyon, May 2017
(Special session on mechanised reasoning)
We investigate the equational theory of algebras of formal languages with the constants empty language and unit language, the unary mirror image and Kleene star operators, and the binary operations of union, intersection and concatenation. We start by reducing the problem of deciding the validity of an equation over this signature to the equality of certain graph languages. This allows us to derive decidability, and to show that this problem is in fact ExpSpace-complete. Using this graph characterisation, and removing the Kleene star from our signature, we then propose a complete finite axiomatisation of this theory. This development was obtained using the proof assistant Coq.

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
PPLV Seminar in London, April 2017
.
More

Related papers

A Complete Axiomatisation of a Fragment of Language Algebra (in CSL 2020) More
Reversible Kleene lattices (in MFCS 2017) More

Updated: