Construction sequences

Lax185574.ConstructionSequences · concepts/Lax185574/ConstructionSequences.lean · lax-185574

definition

Loading review…

Natural Language Statement

Definition

For colors P, Q and a partial graph G, the partial graphs merge_{P,Q}(G) (for P ≠ Q), resolve⁺{P,Q}(G) and resolve⁻{P,Q}(G) are obtained from G by leaving everything unchanged, apart from the following:

merge_{P,Q}(G): P^H = P^G ∪ Q^G and Q^H = ∅, for P ≠ Q;
resolve⁺_{P,Q}(G): E(H) = E(G) ∪ (P^G Q^G ∖ N(G));
resolve⁻_{P,Q}(G): N(H) = N(G) ∪ (P^G Q^G ∖ E(G)).

Here P^G Q^G is the set of pairs xy of distinct vertices with x ∈ P^G and y ∈ Q^G. After either resolve, every pair in P^G Q^G is resolved.

An initial partial graph has no resolved pairs, and every part is a singleton. A construction sequence of a graph G = (V, E) is a sequence G₁, …, G_λ of partial graphs with vertex set V such that G₁ is initial, every step is one merge or one resolve, and G_λ has a single part, E(G_λ) = E and N(G_λ) = (V choose 2) ∖ E.

Concept map

8 concepts

100%

DefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.

In the paper

page 40 of this submission's paper
page 7 of this submission's paper

Lean source view on GitHub

Show types on hover

1	import Lax185574.PartialGraphs
2
3	/-!
4	---
5	title: Construction sequences
6	type: definition
7	---
8	For colors P, Q and a partial graph G, the partial graphs merge_{P,Q}(G)
9	(for P ≠ Q), resolve⁺_{P,Q}(G) and resolve⁻_{P,Q}(G) are obtained from G
10	by leaving everything unchanged, apart from the following:
11
12	- merge_{P,Q}(G): P^H = P^G ∪ Q^G and Q^H = ∅, for P ≠ Q;
13	- resolve⁺_{P,Q}(G): E(H) = E(G) ∪ (P^G Q^G ∖ N(G));
14	- resolve⁻_{P,Q}(G): N(H) = N(G) ∪ (P^G Q^G ∖ E(G)).
15
16	Here P^G Q^G is the set of pairs xy of distinct vertices with x ∈ P^G and
17	y ∈ Q^G. After either resolve, every pair in P^G Q^G is resolved.
18
19	An initial partial graph has no resolved pairs, and every part is a
20	singleton. A construction sequence of a graph G = (V, E) is a sequence
21	G₁, …, G_λ of partial graphs with vertex set V such that G₁ is initial,
22	every step is one merge or one resolve, and G_λ has a single part,
23	E(G_λ) = E and N(G_λ) = (V choose 2) ∖ E.
24
25	# Formalization notes
26
27	A sequence is a nonempty list of partial graphs. Its first entry is G₁,
28	and the step condition relates consecutive entries `s[t]` and `s[t+1]`.
29	"Every part is a singleton" says that the coloring is injective, and "a
30	single part" says that all vertices have the same color. The colors P
31	and Q of a step are arbitrary natural numbers, as in the paper. A resolve naming a color that no vertex
32	has, or a merge whose second color no vertex has, changes nothing, and
33	is still counted as a step. Such steps only lengthen a sequence. The pairs `P^G Q^G` are built with `SimpleGraph.fromRel`,
34	which symmetrizes the relation and removes the diagonal.
35
36	The paper defines construction sequences twice, in the technical
37	overview through merges and resolves of parts, and in the preliminaries
38	of the model-checking part through the operators on colors above. Both
39	passages describe the same sequences. A merge of two distinct parts is a
40	merge of their colors, and a resolve of two parts is a resolve of their
41	colors.
42
43	Algorithms receive and produce a construction sequence on `Fin n` as a
44	`Script`: the colors of the initial partial graph, which has no resolved
45	pairs, and the list of the steps. `Script.run` is the sequence it
46	produces, the initial partial graph followed by the results of the
47	steps. The derived encoding of `Lax185574.Encoding` writes a script as
48	n, the n colors, the number of steps, and then each step as three
49	numbers, an opcode (0 for a merge, 1 for a positive resolve and 2 for a
50	negative resolve) followed by the colors P and Q. Nothing in a script
51	forces its colors to be distinct, or its sequence to be a construction
52	sequence of a particular graph. Those are properties of the sequence,
53	stated through `IsConstructionSequence` where they are needed.
54	-/
55
56	namespace Lax185574.ConstructionSequences
57
58	open Lax185574.PartialGraphs
59
60	universe z
61
62	variable {V : Type z}
63
64	/-- The pairs `P^G Q^G`: distinct vertices, one of color `P` and the
65	other of color `Q`. -/
66	def between (G : PartialGraph V) (P Q : ℕ) : SimpleGraph V :=
67	SimpleGraph.fromRel fun x y => G.color x = P ∧ G.color y = Q
68
69	/-- `merge_{P,Q}(G)`: the vertices of color `Q` get color `P`. -/
70	def merge (G : PartialGraph V) (P Q : ℕ) : PartialGraph V :=
71	{ G with color := fun v => if G.color v = Q then P else G.color v }
72
73	/-- `resolve⁺_{P,Q}(G)`: the unresolved pairs in `P^G Q^G` become
74	edges. -/
75	def resolvePos (G : PartialGraph V) (P Q : ℕ) : PartialGraph V where
76	edge := G.edge ⊔ (between G P Q \ G.nonEdge)
77	nonEdge := G.nonEdge
78	disjoint := disjoint_sup_left.2 ⟨G.disjoint, disjoint_sdiff_self_left⟩
79	color := G.color
80
81	/-- `resolve⁻_{P,Q}(G)`: the unresolved pairs in `P^G Q^G` become
82	non-edges. -/
83	def resolveNeg (G : PartialGraph V) (P Q : ℕ) : PartialGraph V where
84	edge := G.edge
85	nonEdge := G.nonEdge ⊔ (between G P Q \ G.edge)
86	disjoint := disjoint_sup_right.2 ⟨G.disjoint, disjoint_sdiff_self_right⟩
87	color := G.color
88
89	/-- An initial partial graph: no resolved pairs, and every part is a
90	singleton. -/
91	def IsInitial (G : PartialGraph V) : Prop :=
92	G.edge = ⊥ ∧ G.nonEdge = ⊥ ∧ Function.Injective G.color
93
94	/-- `H` is obtained from `G` by one merge or one resolve. -/
95	def IsStep (G H : PartialGraph V) : Prop :=
96	∃ P Q : ℕ, (P ≠ Q ∧ H = merge G P Q) ∨ H = resolvePos G P Q ∨
97	H = resolveNeg G P Q
98
99	/-- `s` is a construction sequence of the graph `G`: it starts with an
100	initial partial graph, each entry is obtained from the previous one by
101	one merge or one resolve, and the last entry has a single part, the
102	edges of `G` as edges and the non-edges of `G` as non-edges. -/
103	def IsConstructionSequence (G : SimpleGraph V) (s : List (PartialGraph V)) :
104	Prop :=
105	∃ h : s ≠ [],
106	IsInitial (s.head h) ∧
107	(∀ (t : ℕ) (ht : t + 1 < s.length), IsStep s[t] s[t + 1]) ∧
108	(∀ u v : V, (s.getLast h).color u = (s.getLast h).color v) ∧
109	(s.getLast h).edge = G ∧ (s.getLast h).nonEdge = Gᶜ
110
111	open Lax185574.Encoding
112
113	/-- One step of a construction sequence. -/
114	inductive Step
115	/-- `merge_{P,Q}`. -/
116	\| merge (P Q : ℕ)
117	/-- `resolve⁺_{P,Q}`. -/
118	\| resolvePos (P Q : ℕ)
119	/-- `resolve⁻_{P,Q}`. -/
120	\| resolveNeg (P Q : ℕ)
121	deriving Encode
122
123	/-- The partial graph obtained by applying a step. -/
124	def apply (G : PartialGraph V) : Step → PartialGraph V
125	\| .merge P Q => merge G P Q
126	\| .resolvePos P Q => resolvePos G P Q
127	\| .resolveNeg P Q => resolveNeg G P Q
128
129	/-- The partial graph with no resolved pairs and the given colors. -/
130	def unresolved (color : V → ℕ) : PartialGraph V where
131	edge := ⊥
132	nonEdge := ⊥
133	disjoint := disjoint_bot_left
134	color := color
135
136	/-- A construction script on `Fin n`: the colors of the initial partial
137	graph, which has no resolved pairs, and the steps. -/
138	structure Script (n : ℕ) where
139	/-- The colors of the initial partial graph. -/
140	colors : Fin n → ℕ
141	/-- The steps, in order. -/
142	steps : List Step
143	deriving Encode
144
145	/-- The sequence produced by a script: the initial partial graph
146	followed by the results of the steps. -/
147	def Script.run {n : ℕ} (σ : Script n) : List (PartialGraph (Fin n)) :=
148	σ.steps.scanl apply (unresolved σ.colors)
149
150	/-- Every number in the encoding of the script `σ` is at most the
151	length of the encoding plus `n`. This holds when the colors of the
152	initial partial graph and of the steps are vertices. It lets an
153	algorithm pass the script on to another one, whose word length depends
154	on the numbers of its input. -/
155	def Script.HasSmallNumbers {n : ℕ} (σ : Script n) : Prop :=
156	∀ v ∈ encode σ, v ≤ (encode σ).length + n
157
158	/-- The list `y` encodes the sequence `s` of partial graphs on `n`
159	vertices: it is the encoding of a script that produces `s`. -/
160	def EncodesSequence {n : ℕ} (y : List ℕ) (s : List (PartialGraph (Fin n))) :
161	Prop :=
162	∃ σ : Script n, y = encode σ ∧ s = σ.run
163
164	end Lax185574.ConstructionSequences
165

Formalization notes

A sequence is a nonempty list of partial graphs. Its first entry is G₁, and the step condition relates consecutive entries $s[t]$ and $s[t+1]$ . "Every part is a singleton" says that the coloring is injective, and "a single part" says that all vertices have the same color. The colors P and Q of a step are arbitrary natural numbers, as in the paper. A resolve naming a color that no vertex has, or a merge whose second color no vertex has, changes nothing, and is still counted as a step. Such steps only lengthen a sequence. The pairs $P^G Q^G$ are built with $SimpleGraph.fromRel$ , which symmetrizes the relation and removes the diagonal.

The paper defines construction sequences twice, in the technical overview through merges and resolves of parts, and in the preliminaries of the model-checking part through the operators on colors above. Both passages describe the same sequences. A merge of two distinct parts is a merge of their colors, and a resolve of two parts is a resolve of their colors.

Algorithms receive and produce a construction sequence on $Fin n$ as a $Script$ : the colors of the initial partial graph, which has no resolved pairs, and the list of the steps. $Script.run$ is the sequence it produces, the initial partial graph followed by the results of the steps. The derived encoding of $Lax185574.Encoding$ writes a script as n, the n colors, the number of steps, and then each step as three numbers, an opcode (0 for a merge, 1 for a positive resolve and 2 for a negative resolve) followed by the colors P and Q. Nothing in a script forces its colors to be distinct, or its sequence to be a construction sequence of a particular graph. Those are properties of the sequence, stated through $IsConstructionSequence$ where they are needed.

Builds on

Lax185574.PartialGraphs

Used by

From Mathlib

none

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

Loading discussion…

Lax Lean Archive

Construction sequences

Flags

Flag this concept

Natural Language Statement

Definition

In the paper

Lean source view on GitHub

Discussion

Settings

Your comments