This page is a web appendix to the following papers:
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 [1], 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 [2], 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 [3] we give the first formal and constructive proof in Coq/Ssreflect that the graphs of treewidth two are exactly those that do not admit K4 as a minor. It is extended in [4], where:
In [5] we formalise the completeness theorem for 2pdom algebras, following the proof in the MFCS'18 paper [2].
This formalisation effort is rather orthogonal to the one above: we are not concerned at all with minors and treewidth here.
We reprove that graphs form a 2pdom algebra here because we need a slight generalisation, but this is the only overlap with [4].
This requires us to use two representations for graphs, the one from the previous papers, which is dependently typed, and a more classical one.
We only maintain and develop a single library for the aforementioned formalisations.
It is available on github/coq-community and opam (package coq-graph-theory
).
Since version 0.8, the library also contains a module dom
containing a proof of Cockayne-Hedetniemi domination chain (with weighted parameters).
The code can be browsed online (CoqDocJS with foldable proofs). Its modules dependencies are given on the right, where:
edone
: small extension of the [done] tactic
bounded
: fixpoint operator for bounded recursion
preliminaries
: miscellaneous basic lemmas missing from the standard libraries
finmap_plus
: additions to the mathcomp-finmap library
set_tac
: a simple tactic for reasoning about finite sets
bij
: computationally relevant bijections between sets
finite_quotient
: abstraction layer for mathcomp quotients
equiv
: lemmas about equivalence closure
digraph
: directed graphs, paths
sgraph
: simple graphs, trees and forests
helly
: Helly property for trees
treewidth
: tree decompositions, treewidth
minor
: minors, links with treewidth
menger
: Menger's theorem and corollaries
separators
: separators, proof of TW2 = K4-free via Menger's theorem
checkpoint
: checkpoints
dom
: Cockayne-Hedetniemi domination chain theorem
ptt
: 2p-algebras, initial algebra of terms, tests (reworked along [5])
mgraph
: labelled multigraphs (reworked along [5])
mgraph2
: pointed multigraphs, 2p algebra of such graphs (reworked along [5])
skeleton
: skeletons of multigraphs
mgraph2_tw2
: subalgebra of treewidth at most two multigraphs
cp_minor
: links between checkpoints and minors, for extraction
extraction_def
: definition of the extraction function in the connected case
extraction_iso
: correctness of the extraction function (connected case)
extraction_top
: extension to the general case, TW2 = K4-free as a corollary
structures
: setoids, bisetoids, monoids
pttdom
: 2pdom-algebras, initial algebra of terms, tests
mgraph
: labelled multigraphs
mgraph2
: pointed multigraphs, 2pdom algebra of such graphs
rewriting
: definition of the rewriting system
reduction
: rewriting system powerful enough to reach normal forms
open_confluence
: open graphs, open local confluence proof
transfer
: transfer lemmas between the open and packed representations of 2p-graphs
completeness
: wrapping up everything into a completeness proof
For reference, we also provide the code as it was at submission/publication time for the three formalisation papers
(This code completely subsumes the one just above.)
(Rather orthogonal to the one just above: only soundness is repeated since it had to be generalised.)
In the MFCS'17 paper [1], we claim 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).