The Equational Theory of Algebras of Languages
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 | |