K4-free/TW2 graphs, free algebras, Coq proofs
This page is a web appendix to the following three papers:
-
K4-free Graphs as a Free Algebra,
.pdf.
E. Cosme Llopez, D. Pous, in Proc. MFCS'17.
-
Treewidth-Two Graphs as a Free Algebra,
.pdf.
C. Doczkal, D. Pous, in Proc. MFCS'18.
-
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
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).