Partial graphs

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

definition

Loading review…

Natural Language Statement

Definition

A partial graph H consists of a finite vertex set V = V(H), two disjoint sets E(H), N(H) ⊆ (V choose 2) of edges and non-edges, and a partition of V whose parts are treated as colors. The pairs in R(H) = E(H) ∪ N(H) are resolved, and all other pairs are unresolved. H is viewed as a logical structure with binary relations E and N and a unary predicate for every color. Distances dist^H and balls Ball^H_r(v) are measured in the Gaifman graph (V, R(H)), the graph of resolved pairs.

For the model-checking algorithm, the parts are given names, to track them over time. Fix a countably infinite set of unary symbols, called colors. A partial graph G is regarded as a relational structure with the two symmetric binary relations E and N and a unary relation Y for every color Y. The vertices of color Y form its color class Y^G, and the nonempty color classes are the parts of G. The size of the representation of G is given by |G| = |V(G)| and ‖G‖ = |V(G)| + |R(G)|.

Concept map

7 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.GaifmanGraph
2	import Lax185574.Encodings
3	import Mathlib.Combinatorics.SimpleGraph.Basic
4	import Mathlib.Data.Set.Card
5
6	/-!
7	---
8	title: Partial graphs
9	type: definition
10	---
11	A partial graph H consists of a finite vertex set V = V(H), two
12	disjoint sets E(H), N(H) ⊆ (V choose 2) of edges and non-edges, and
13	a partition of V whose parts are treated as colors. The pairs in
14	R(H) = E(H) ∪ N(H) are resolved, and all other pairs are
15	unresolved. H is viewed as a logical structure with binary relations E
16	and N and a unary predicate for every color. Distances dist^H and balls
17	Ball^H_r(v) are measured in the Gaifman graph (V, R(H)), the graph of
18	resolved pairs.
19
20	For the model-checking algorithm, the parts are given names, to track
21	them over time. Fix a countably infinite set of unary symbols, called
22	colors. A partial graph G is regarded as a relational structure with
23	the two symmetric binary relations E and N and a unary relation Y for
24	every color Y. The vertices of color Y form its color class Y^G, and
25	the nonempty color classes are the parts of G. The size of the
26	representation of G is given by \|G\| = \|V(G)\| and
27	‖G‖ = \|V(G)\| + \|R(G)\|.
28
29	# Formalization notes
30
31	The paper introduces partial graphs in the technical overview and
32	extends the notion in the preliminaries of the model-checking part. Both
33	passages describe the same objects. All metric notions count resolved
34	pairs, edges and non-edges alike.
35
36	Colors are natural numbers. Edges and non-edges are simple graphs on the
37	vertex type, so they are symmetric and irreflexive by construction, and
38	a resolved pair is an edge of their supremum. The language of partial
39	graphs has the two binary symbols and one unary symbol per natural
40	number. Its Gaifman graph is exactly the graph of resolved pairs. That
41	graph is what `ball` uses, so `ball` agrees with
42	`Lax185574.GaifmanGraph.ball` on the structure of a partial graph.
43
44	The induced partial graph G[X], defined in the paper together with
45	`Lax185574.ConstructionWidth`, is the induced substructure of
46	`Lax185574.GaifmanGraph`, applied to the structure of G. Statements
47	about G[X] do not use this substructure. They are stated through the
48	partial graph G and the set X, see `Lax185574.LocalDefinability`, and
49	need no separate definition.
50
51	For a partial graph on `Fin n`, \|G\| is `n`. The size ‖G‖ =
52	\|V(G)\| + \|R(G)\|, used in running-time bounds, is `PartialGraph.size`.
53
54	The distance matrix D_G of a partial graph, with entries
55	D_G(u, v) = dist^G(u, v) ∈ ℕ ∪ {∞}, is `Lax185574.DistanceMatrix`. It is
56	∞ for vertices in different components of the graph of resolved pairs.
57	The algorithms of the model-checking procedure receive it as an
58	additional input, and maintain it along the construction sequence.
59	-/
60
61	namespace Lax185574.PartialGraphs
62
63	open FirstOrder FirstOrder.Language
64	open Lax185574.GaifmanGraph
65
66	universe z
67
68	/-- A partial graph on the vertex type `V`: disjoint edges and
69	non-edges, and one color per vertex. -/
70	structure PartialGraph (V : Type z) where
71	/-- The edges `E(G)`. -/
72	edge : SimpleGraph V
73	/-- The non-edges `N(G)`. -/
74	nonEdge : SimpleGraph V
75	/-- No pair is both an edge and a non-edge. -/
76	disjoint : Disjoint edge nonEdge
77	/-- The color of each vertex. -/
78	color : V → ℕ
79
80	variable {V : Type z}
81
82	namespace PartialGraph
83
84	/-- The resolved pairs `R(G) = E(G) ∪ N(G)`, the Gaifman graph of the
85	partial graph. -/
86	def resolved (G : PartialGraph V) : SimpleGraph V := G.edge ⊔ G.nonEdge
87
88	/-- `Ball^G_r(v)`: the vertices within distance `r` of `v` along
89	resolved pairs. -/
90	def ball (G : PartialGraph V) (r : ℕ) (v : V) : Set V :=
91	{u \| WithinDist G.resolved r v u}
92
93	/-- The color class `Y^G`. -/
94	def colorClass (G : PartialGraph V) (Y : ℕ) : Set V := {v \| G.color v = Y}
95
96	/-- The size `‖G‖ = \|V(G)\| + \|R(G)\|` of a partial graph on `Fin n`. -/
97	noncomputable def size {n : ℕ} (G : PartialGraph (Fin n)) : ℕ :=
98	n + Set.ncard G.resolved.edgeSet
99
100	end PartialGraph
101
102	/-- The relation symbols of partial graphs: edges, non-edges and one
103	unary symbol per color. -/
104	inductive Rel : ℕ → Type
105	\| edge : Rel 2
106	\| nonEdge : Rel 2
107	\| color (Y : ℕ) : Rel 1
108
109	/-- The language of partial graphs. -/
110	def language : Language :=
111	⟨fun _ => Empty, Rel⟩
112	deriving Language.IsRelational
113
114	/-- A partial graph as a relational structure. -/
115	@[implicit_reducible]
116	def PartialGraph.structure (G : PartialGraph V) : language.Structure V where
117	funMap f := isEmptyElim f
118	RelMap
119	\| .edge => fun x => G.edge.Adj (x 0) (x 1)
120	\| .nonEdge => fun x => G.nonEdge.Adj (x 0) (x 1)
121	\| .color Y => fun x => G.color (x 0) = Y
122
123	open Lax185574.Encoding in
124	/-- A partial graph on `Fin n` is encoded by the family of its colors,
125	then its edges and then its non-edges, each graph as in
126	`Lax185574.Encodings`. So the encoding is `n` and the `n` colors, then
127	`n` and for every vertex in order the set of its neighbors along edges,
128	then `n` and for every vertex the set of its neighbors along non-edges.
129	It is determined by the partial graph and has length O(‖G‖). Running
130	times are stated in terms of ‖G‖, which is only meaningful for an
131	encoding without padding. The edges and non-edges are relations, so the
132	encoding is not derived. -/
133	noncomputable instance {n : ℕ} : Encode (PartialGraph (Fin n)) where
134	encode G := encode (G.color, G.edge, G.nonEdge)
135
136	end Lax185574.PartialGraphs
137

Formalization notes

The paper introduces partial graphs in the technical overview and extends the notion in the preliminaries of the model-checking part. Both passages describe the same objects. All metric notions count resolved pairs, edges and non-edges alike.

Colors are natural numbers. Edges and non-edges are simple graphs on the vertex type, so they are symmetric and irreflexive by construction, and a resolved pair is an edge of their supremum. The language of partial graphs has the two binary symbols and one unary symbol per natural number. Its Gaifman graph is exactly the graph of resolved pairs. That graph is what $ball$ uses, so $ball$ agrees with $Lax185574.GaifmanGraph.ball$ on the structure of a partial graph.

The induced partial graph G[X], defined in the paper together with $Lax185574.ConstructionWidth$ , is the induced substructure of $Lax185574.GaifmanGraph$ , applied to the structure of G. Statements about G[X] do not use this substructure. They are stated through the partial graph G and the set X, see $Lax185574.LocalDefinability$ , and need no separate definition.

For a partial graph on $Fin n$ , |G| is $n$ . The size ‖G‖ = |V(G)| + |R(G)|, used in running-time bounds, is $PartialGraph.size$ .

The distance matrix D_G of a partial graph, with entries D_G(u, v) = dist^G(u, v) ∈ ℕ ∪ {∞}, is $Lax185574.DistanceMatrix$ . It is ∞ for vertices in different components of the graph of resolved pairs. The algorithms of the model-checking procedure receive it as an additional input, and maintain it along the construction sequence.

Builds on

Used by

From Mathlib

Discussion

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

Loading discussion…

Lax Lean Archive

Partial graphs

Flags

Flag this concept

Natural Language Statement

Definition

In the paper

Lean source view on GitHub

Discussion

Settings

Your comments