Lax11.CliqueExpr

k-expressions, and the graphs of cliquewidth at most k

concepts/Lax11/CliqueExpr.lean · lax-11

definition

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Definition

A k-expression builds a graph from single vertices, each created with one of k labels, by three operations: disjoint union of two expressions; adding every edge between the vertices of one label class and those of another; and relabelling, which moves one label class into another. Evaluating an expression gives a vertex set, a graph on it, and the k label classes it has arrived at. A graph has cliquewidth at most k when some k-expression evaluates to it — that is the width measure the theorem below is stated for, and an expression for the graph is what the theorem takes as input.

An expression is valid when its leaves create pairwise distinct vertices and every edge-adding operation joins two different classes; it is an expression for a graph $G$ when in addition its leaves create all of $G$ 's vertices and it evaluates to exactly $G$ 's edges.

The operations of an expression are also numbered here, since the numbers are what a machine reading an expression is handed: the disjoint union is $0$ , creating a vertex with label $l$ is $1 + l$ , and the two binary operations occupy two further blocks of $k²$ numbers each, in which a pair of labels is read in base $k$ .

Lean source view on GitHub

1	import Mathlib.Combinatorics.SimpleGraph.Basic
2
3	/-!
4	---
5	title: k-expressions, and the graphs of cliquewidth at most k
6	type: definition
7	---
8	A k-expression builds a graph from single vertices, each created with
9	one of k labels, by three operations: disjoint union of two
10	expressions; adding every edge between the vertices of one label class
11	and those of another; and relabelling, which moves one label class into
12	another. Evaluating an expression gives a vertex set, a graph on it,
13	and the k label classes it has arrived at. A graph has cliquewidth at
14	most k when some k-expression evaluates to it — that is the width
15	measure the theorem below is stated for, and an expression for the
16	graph is what the theorem takes as input.
17
18	An expression is valid when its leaves create pairwise distinct
19	vertices and every edge-adding operation joins two different classes;
20	it is an expression for a graph `G` when in addition its leaves
21	create all of `G`'s vertices and it evaluates to exactly `G`'s edges.
22
23	The operations of an expression are also numbered here, since the
24	numbers are what a machine reading an expression is handed: the
25	disjoint union is `0`, creating a vertex with label `l` is `1 + l`, and
26	the two binary operations occupy two further blocks of `k²` numbers
27	each, in which a pair of labels is read in base `k`.
28
29	# Formalization notes
30
31	Vertices are named globally, by the leaves: a leaf carries a vertex
32	name and the vertex set of a subexpression is the set of names of its
33	leaves. So no node of an expression builds a fresh structure that would
34	then have to be glued along an isomorphism — every subexpression
35	evaluates to a subset of the same fixed vertex set, and disjoint union
36	is literally union. That the two sides of a union really are disjoint
37	is then a consequence of the leaf names being distinct, which is what
38	validity requires; it is not built into the definition of the
39	evaluation, so the evaluation stays a plain structural recursion. What
40	does change from a node to its parent is the graph, since adding edges
41	adds them.
42
43	The label classes are sets of vertices rather than a colouring
44	function. That they are pairwise disjoint and cover the vertex set is a
45	theorem about valid expressions, not a clause of the definition — the
46	fewer conditions the definition imposes, the less there is to check
47	against a paper.
48
49	Everything computes: vertex sets and label classes are finite sets, the
50	well-formedness test is a Boolean, and the evaluated graph has a
51	decidable adjacency relation given by the same recursion, so a
52	hand-written expression can be evaluated and its edges compared with a
53	graph by computation rather than by hand.
54
55	The requirement that edge addition joins two different classes is part
56	of validity rather than of the constructor, so that an expression is
57	plain data with no proof carried inside it. Nothing in the mathematics
58	needs it; it is there because it is part of the standard definition of
59	cliquewidth, and leaving it out would silently claim the theorem for a
60	larger class of graphs than the name denotes. Relabelling tests for the
61	target class before the source class, so that relabelling a class into
62	itself is the identity rather than an operation that empties it.
63	-/
64
65	namespace Lax11.CliqueExpr
66
67	variable {n k : ℕ}
68
69	/-- A `k`-expression over the vertex names `Fin n`: a single labelled
70	vertex, disjoint union, edge addition between two label classes, or
71	relabelling one class into another. -/
72	inductive Expr (n k : ℕ) : Type
73	/-- The vertex `v`, carrying label `l`. -/
74	\| leaf (v : Fin n) (l : Fin k)
75	/-- Disjoint union `⊕`. -/
76	\| union (e₁ e₂ : Expr n k)
77	/-- `η i j`: join every vertex of class `i` to every vertex of class `j`. -/
78	\| addEdges (i j : Fin k) (e : Expr n k)
79	/-- `ρ i j`: move class `i` into class `j`. -/
80	\| relabel (i j : Fin k) (e : Expr n k)
81
82	/-- The vertex names created by the leaves, in order. -/
83	def leafIds : Expr n k → List (Fin n)
84	\| .leaf v _ => [v]
85	\| .union e₁ e₂ => leafIds e₁ ++ leafIds e₂
86	\| .addEdges _ _ e => leafIds e
87	\| .relabel _ _ e => leafIds e
88
89	/-- The vertex set of an expression. -/
90	def verts : Expr n k → Finset (Fin n)
91	\| .leaf v _ => {v}
92	\| .union e₁ e₂ => verts e₁ ∪ verts e₂
93	\| .addEdges _ _ e => verts e
94	\| .relabel _ _ e => verts e
95
96	/-- The label classes of an expression: `cls e i` is the set of vertices
97	of `e` currently carrying label `i`. -/
98	def cls : Expr n k → Fin k → Finset (Fin n)
99	\| .leaf v l, i => if i = l then {v} else ∅
100	\| .union e₁ e₂, i => cls e₁ i ∪ cls e₂ i
101	\| .addEdges _ _ e, i => cls e i
102	\| .relabel i j e, t => if t = j then cls e i ∪ cls e j else if t = i then ∅ else cls e t
103
104	/-- The graph an expression evaluates to. -/
105	def graph : Expr n k → SimpleGraph (Fin n)
106	\| .leaf _ _ => ⊥
107	\| .union e₁ e₂ => graph e₁ ⊔ graph e₂
108	\| .addEdges i j e => graph e ⊔ SimpleGraph.fromRel fun u v => u ∈ cls e i ∧ v ∈ cls e j
109	\| .relabel _ _ e => graph e
110
111	/-- The evaluated graph has a decidable adjacency relation, by the same
112	structural recursion. -/
113	instance decidableAdj : ∀ e : Expr n k, DecidableRel (graph e).Adj
114	\| .leaf _ _ => inferInstanceAs (DecidableRel (⊥ : SimpleGraph (Fin n)).Adj)
115	\| .union e₁ e₂ =>
116	have := decidableAdj e₁
117	have := decidableAdj e₂
118	inferInstanceAs (DecidableRel (graph e₁ ⊔ graph e₂).Adj)
119	\| .addEdges i j e =>
120	have := decidableAdj e
121	inferInstanceAs (DecidableRel
122	(graph e ⊔ SimpleGraph.fromRel fun u v => u ∈ cls e i ∧ v ∈ cls e j).Adj)
123	\| .relabel _ _ e => decidableAdj e
124
125	/-- Well-formedness of the operations: `addEdges` joins two different
126	classes, the standard restriction on `η`. -/
127	def opsOk : Expr n k → Bool
128	\| .leaf _ _ => true
129	\| .union e₁ e₂ => opsOk e₁ && opsOk e₂
130	\| .addEdges i j e => (i != j) && opsOk e
131	\| .relabel _ _ e => opsOk e
132
133	/-- A valid expression: the leaves create pairwise distinct vertices —
134	which is what makes the two sides of every `⊕` disjoint — and the
135	operations are well formed. -/
136	structure Valid (e : Expr n k) : Prop where
137	/-- No vertex name is created twice. -/
138	nodup : (leafIds e).Nodup
139	/-- Every `addEdges` joins two different classes. -/
140	ops : opsOk e = true
141
142	/-- A `k`-expression for `G`: valid, and at the root it has created
143	every vertex and exactly the edges of `G`. -/
144	structure ValidFor (e : Expr n k) (G : SimpleGraph (Fin n)) : Prop extends Valid e where
145	/-- The root creates every vertex. -/
146	verts_eq : verts e = Finset.univ
147	/-- The root evaluates to `G`. -/
148	graph_eq : graph e = G
149
150	/-- The operation performed at a node of a `k`-expression. -/
151	inductive Op (k : ℕ) where
152	/-- Disjoint union. -/
153	\| union
154	/-- Create a vertex with label `l`. -/
155	\| leaf (l : Fin k)
156	/-- `η i j`: join class `i` to class `j`. -/
157	\| eta (i j : Fin k)
158	/-- `ρ i j`: move class `i` into class `j`. -/
159	\| rho (i j : Fin k)
160	deriving DecidableEq
161
162	/-- The number naming an operation. The blocks are `union` (one code),
163	the leaves (`k` codes), the joins and the relabels (`k²` codes each,
164	the pair `(i, j)` read in base `k`). -/
165	def Op.code : Op k → ℕ
166	\| .union => 0
167	\| .leaf l => 1 + (l : ℕ)
168	\| .eta i j => 1 + k + ((i : ℕ) * k + (j : ℕ))
169	\| .rho i j => 1 + k + k * k + ((i : ℕ) * k + (j : ℕ))
170
171	/-- The size of the operation alphabet. -/
172	def opCard (k : ℕ) : ℕ := 1 + k + 2 * (k * k)
173
174	end Lax11.CliqueExpr
175

Formalization notes

Vertices are named globally, by the leaves: a leaf carries a vertex name and the vertex set of a subexpression is the set of names of its leaves. So no node of an expression builds a fresh structure that would then have to be glued along an isomorphism — every subexpression evaluates to a subset of the same fixed vertex set, and disjoint union is literally union. That the two sides of a union really are disjoint is then a consequence of the leaf names being distinct, which is what validity requires; it is not built into the definition of the evaluation, so the evaluation stays a plain structural recursion. What does change from a node to its parent is the graph, since adding edges adds them.

The label classes are sets of vertices rather than a colouring function. That they are pairwise disjoint and cover the vertex set is a theorem about valid expressions, not a clause of the definition — the fewer conditions the definition imposes, the less there is to check against a paper.

Everything computes: vertex sets and label classes are finite sets, the well-formedness test is a Boolean, and the evaluated graph has a decidable adjacency relation given by the same recursion, so a hand-written expression can be evaluated and its edges compared with a graph by computation rather than by hand.

The requirement that edge addition joins two different classes is part of validity rather than of the constructor, so that an expression is plain data with no proof carried inside it. Nothing in the mathematics needs it; it is there because it is part of the standard definition of cliquewidth, and leaving it out would silently claim the theorem for a larger class of graphs than the name denotes. Relabelling tests for the target class before the source class, so that relabelling a class into itself is the identity rather than an operation that empties it.

Builds on

none

Used by

Lax11.InstanceEncoding

From Mathlib

Mathlib.Combinatorics.SimpleGraph.Basic

Community review

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

0 comments

Loading discussion…

Lax Lean Archive

k-expressions, and the graphs of cliquewidth at most k

Flags

Flag this concept