K4-free/TW2 graphs, free algebras, Coq proofs

This page is a web appendix to the following three papers:

1. K4-free Graphs as a Free Algebra, .pdf.
   E. Cosme Llopez, D. Pous, in Proc. MFCS'17.
   
2. Treewidth-Two Graphs as a Free Algebra, .pdf.
   C. Doczkal, D. Pous, in Proc. MFCS'18.
   
3. A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs, .pdf.
   C. Doczkal, G. Combette, D. Pous, in Proc. ITP'18.
   

It is a well-known result that graphs of treewidth at most two (TW2) are the ones excluding the clique with four vertices (K4) as a minor, or equivalently, the graphs whose biconnected components are series-parallel.

• In the first paper above, we turn those graphs into a free algebra, answering positively a question by Courcelle and Engelfriet, in the case of treewidth two.
  First we propose a syntax for denoting them: in addition to parallel composition and series composition, it suffices to consider the neutral elements of those operations and a unary transpose operation. Then we give a finite equational presentation (2p-algebra) and we prove it complete: two terms from the syntax are congruent if and only if they denote the same graph.
  Our proof is based on an precise analysis of the structure of K4-free graphs; it actually requires us to (re)prove that those have treewidth at most two.
• In the second paper, we give a simpler proof of the main result from the first paper, not using minors at all: we use a confluent rewriting system to extract terms from TW2 graphs. This approach is more flexible and allows us to handle variants of 2p-algebras: 2pdom-algebras for connected graphs and 1-free 2p-algebras for graphs with distinct input and output and without self-loops.
• In the third paper we give a formal and constructive proof in Coq/Ssreflect that the graphs of treewidth two are exactly those that do not admit K4 as a minor. This result is no longer required to formally prove that those graphs form a free algebra, thanks to the proof from the second paper; it should however be useful to formalise the characterisation of allegories we obtained with Valeria Vignudelli.

Coq/ssreflect proof of TW2=K4-free

• Browse Coq Development (CoqDocJS with foldable proofs)
• Download Theory Files (requires coq-8.6.1 and mathcomp-1.6.1 or newer, updated 15-05-2018)

Independence of the 2p-algebra axioms

We prove the independence of the axioms by exhibiting finite (partial) models.
We automatically checked those models in the Coq proof assistant, see the proof script here or download it there.
These counter-models have at most four elements; the converse operation is always taken to be the identity, except for the independence of axioms A6 and A7.

When looking for those counter-models, we found that there are 11 2p-algebras with three elements and 236 with four elements (up to isomorphism).