Algebras and axioms for graphs of bounded treewidth

This is a web appendix to the following paper, to be presented at ICALP 2024:

A finite presentation of graphs of treewidth at most three, by Amina Doumane, Damien Pous and Samuel Humeau.

Below you can enter a term to see its graph (the syntax is explained at the bottom of this page)

You may move elements using the mouse, or zoom using control-scroll. You may also type commands in the box below to add/remove elements, etc (press 'h' for a list)


To prove our classification of hard graphs of treewidth at most three, use the left and right arrows to access to the three other graphs (considered as shapes), in each of them, you can use 's' on one of their edges in order to do a case analysis on this edge; this will generate more graphs, and you can navigate between those graphs using the left and right arrows; some of these graphs are not hard, or the initial separation pairs are not minimal, and you can discard them with 'k'. Eventually, you obtain only the domino and cross graphs (DG, XG). (To optimise the process, you may also use the key 'o' on edges to perform slightly smarter case analyses---the first graph initially loaded should not be considered and can be discarded with 'K'.)





Syntax

== terms (u,v) ==
0 empty graph
a a-labeled edge
u | v parallel composition
fu forget u
lu lift u
pu permute p u
ru swap last two sources of u
iu u located according to injection i
s(u1,...,uk) series composition (without the forget)
*(u1,...,uk) star operation
u.v binary sequential composition
u' swap last two sources
== sourced terms (at top level only) ==
#k u set arity to k
== labels (a) ==
s when s does not start with f/l/s/r, which are reserved for forgets/lifts/series/swaplast
-s when s does so, or when s is empty
== permutations (p) ==
[231] explicit permutation of size <=9
(234) cyclic permutation (here, [1342]), of size <=9
[1,..,8,10,9] explicit permutation of possibly greater size
(9,10) cyclic permutation of possible greater size
(note: the identity permutations cannot be written)
== injections (i) ==
{264} injection mapping 1 to 2, 2 to 6, 3 to 4
{2,6,11} injection with potentially bigger values
{011} injection mapping 1 to 11

Code

The source code for this applet (as well as a standalone GTK program) is available on Github.