The Equational Theory of Algebras of Languages

BLAST in Nashville, August 2017

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 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
Related papers
	A Complete Axiomatisation of a Fragment of Language Algebra (in CSL 2020)	More
	Reversible Kleene lattices (in MFCS 2017)	More