Related documents |
Papers |
[-] |
We consider algebras of languages over the signature of reversible Kleene lattices, that is the regular operations (empty and unit languages, union, concatenation and Kleene star) together with intersection and mirror image. We provide a complete set of axioms for the equational theory of these algebras. This proof was developed in the proof assistant Coq.
@inproceedings{brunet20-2020, title="A Complete Axiomatisation of a Fragment of Language Algebra", author={Brunet, Paul}, year={2020}, booktitle={CSL}, doi={"10.4230/LIPIcs.CSL.2020.11"}, }
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.
@inproceedings{brunet12-2017, title="Reversible Kleene lattices", author={Brunet, Paul}, year={2017}, booktitle={MFCS}, doi={"10.4230/LIPIcs.MFCS.2017.66"}, }
Talks |
[-] |
Documents |
[-] |
Axiomatisation |
A finite and complete axiomatisation of the algebra of languages over the signature of reversible monoidal lattices was proved in Coq.
Toolbox of simple definitions, lemmas and tactics.
Basics of languages.
We prove here that there is a finite number of functions between two finite decidable sets.
We define in this module 2-pointed labelled directed graphs, and some operations on them.
This module deals with series-parallel terms.
This module is devoted to the translation from series-parallel terms to graphs.
This module introduces weak terms, and establishes some of their general properties.
This module is devoted to the translation of weak terms into graphs.
In this module we define and study an algebra of terms with sequential composition and its unit, intersection, and a mirror operation restricted to variables.
In this module we describe the reductions between terms (type 𝐓), primed weak terms (𝐖') and series-parallel terms (𝐒𝐏).
Using the translation of terms into primed weak terms we can reduce the axiomatic containment of 𝐓-terms to the ordering of graphs.
This module defines the full signature of language algebra we consider here, and its finite complete axiomatization. We also define here some normalisation functions, and list some of their properties.
This module is devoted to the reductions between expressions and terms.
Stringing together the various translations we've defined so far, we may associate with every expression a set of weak graphs. This implies decidability of the axiomatic equivalence for expressions.
In most this module, we establish the following lemma: for every series-parallel term u, there exists a word w and an interpretation σ such that for every other 𝐒𝐏 term v, the graph of v is larger than the graph of u if and only if w belongs to the σ-interpretation of v. This lemma will allow us to prove completeness of our axiomatization with respect to language interpretations.
In the second part of the module, we generalise the result to weak terms and primed weak terms.
We finally arrive to the main result of this development: the proof that our axiomatization is complete for the equational theory of languages.