A finite and complete axiomatisation of the algebra of languages over the signature of reversible monoidal lattices, proved in Coq.

What is this repository for?

  • This repository contains the full proof, together with some attempts at extending it. These are in the various branches.
  • The documentation is available on my personal webapge, here.

How do I get set up?

  • This proof was developped using Coq version 8.6.1.
  • For readability reasons, we heavily used utf-8 symbols. To navigate the proof, we recommend using emacs with Proof General and company-coq.
  • We generated a Makefile automatically using the tool coq_makefile. The documentation for this tool can be found here.

Overview of the proof

  • tools Toolbox of simple definitions, lemmas and tactics.

  • language Basics of languages.

  • finite_functions We prove here that there is a finite number of functions between two finite decidable sets.

  • graph We define in this module 2-pointed labelled directed graphs, and some operations on them.

  • sp_terms This module deals with series-parallel terms.

  • sp_terms_graphs This module is devoted to the translation from series-parallel terms to graphs.

  • w_terms This module introduces weak terms, and establishes some of their general properties.

  • w_terms_graphs This module is devoted to the translation of weak terms into graphs.

  • terms 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.

  • terms_w_terms In this module we describe the reductions between terms (type 𝐓), primed weak terms (𝐖') and series-parallel terms (𝐒𝐏).

  • terms_graphs Using the translation of terms into primed weak terms we can reduce the axiomatic containment of 𝐓-terms to the ordering of graphs.

  • expr 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.

  • expr_terms This module is devoted to the reductions between expressions and terms.

  • expr_graphs 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.

  • to_lang_witness 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.

  • completeness We finally arrive to the main result of this development: the proof that our axiomatization is complete for the equational theory of languages.