Lax916827.SnakeGraphs

Snake graphs and their outputs

concepts/Lax916827/SnakeGraphs.lean · lax-916827

definition

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

In the paper

page 100 of the paper of lax-157538, Transducers

Definition

A snake graph with states $Q$ , length $n$ and output alphabet $B$ (Section C.2.4 of Transducers) is a directed graph with edges labelled by $B + 1$ whose vertices are pairs of a row $q \in Q$ and a column $i \in \{0, 1, \ldots, n\}$ , in which edges only go between adjacent columns and all edges lie on a single directed path. The output of a snake graph is the concatenation of the labels along that path, the extra label of $B + 1$ contributing nothing; its width is the largest number of times the path visits one column. Like configuration graphs, snake graphs are represented as strings over a finite alphabet $C$ once the state set is fixed: a letter is a bipartite graph on two copies of $Q$ describing the edges between two adjacent columns. The book's snake lemma (Lemma C.2.12) says that for every $k$ the function mapping a string over $C$ to the output of the snake graph it represents, if it represents one of width at most $k$ , and to $\varepsilon$ otherwise, is regular; this is the induction on the width by which two-way transducers are decomposed into primes.

Lean source view on GitHub

1	import Mathlib.Data.Set.Card
2
3	/-!
4	---
5	title: Snake graphs and their outputs
6	type: definition
7	---
8	A snake graph with states $Q$ , length $n$ and output alphabet $B$ (Section
9	C.2.4 of Transducers) is a directed graph with edges labelled by $B + 1$ whose
10	vertices are pairs of a row $q \in Q$ and a column $i \in \{0, 1, \ldots, n\}$ ,
11	in which edges only go between adjacent columns and all edges lie on a single
12	directed path. The output of a snake graph is the concatenation of the labels
13	along that path, the extra label of $B + 1$ contributing nothing; its width is
14	the largest number of times the path visits one column. Like configuration
15	graphs, snake graphs are represented as strings over a finite alphabet $C$
16	once the state set is fixed: a letter is a bipartite graph on two copies of
17	$Q$ describing the edges between two adjacent columns. The book's *snake
18	lemma* (Lemma C.2.12) says that for every $k$ the function mapping a string
19	over $C$ to the output of the snake graph it represents, if it represents one
20	of width at most $k$ , and to $\varepsilon$ otherwise, is regular; this is the
21	induction on the width by which two-way transducers are decomposed into primes.
22
23	# Formalization notes
24
25	A letter `SnakeLetter Q B` assigns to every vertex of the two copies of `Q` —
26	`(false, q)` in the left column, `(true, q)` in the right one — its outgoing
27	edge to the other copy, with a label in `Option B`, if it has one; the letter
28	at position `i` of a string carries the edges between the columns `i` and
29	`i + 1`, so a string of length `n` describes a graph on `Q × {0, …, n}`. The
30	book's special letter for the empty input is not needed: the empty string
31	represents the one-column graph with no edges. A snake path is a directed path
32	with pairwise distinct vertices covering every edge of the graph; a string
33	represents at most one output, so `snakeOut k` is well defined by a choice.
34	The width of the represented graph is bounded by the number of vertices of a
35	column that carry an edge, and the lemma is stated for every `k`, not only
36	`k ≤ \|Q\|`.
37	-/
38
39	namespace Lax916827.SnakeGraphs
40
41	/-- The alphabet `C` of snake letters for the state set `Q` and output alphabet `B`:
42	a letter gives, for every vertex of the two copies of `Q`, its outgoing edge to
43	the other copy with a label in `B + 1`, if any. -/
44	abbrev SnakeLetter (Q B : Type) := Bool × Q → Option (Q × Option B)
45
46	/-- A vertex of a snake graph: a row `q` and a column `i`. -/
47	abbrev Vtx (Q : Type) := Q × ℕ
48
49	/-- The edge relation of the graph represented by `w`: an edge from `v` to `v'`
50	labelled `o` is recorded by the letter between their columns, read from the left
51	copy when `v'` is in the next column and from the right copy when it is in the
52	previous one. -/
53	def Edge {Q B : Type} (w : List (SnakeLetter Q B)) (v v' : Vtx Q) (o : Option B) : Prop :=
54	(v'.2 = v.2 + 1 ∧ ∃ c, w[v.2]? = some c ∧ c (false, v.1) = some (v'.1, o)) ∨
55	(v.2 = v'.2 + 1 ∧ ∃ c, w[v'.2]? = some c ∧ c (true, v.1) = some (v'.1, o))
56
57	/-- The vertex `v` carries an edge, incoming or outgoing. -/
58	def Incident {Q B : Type} (w : List (SnakeLetter Q B)) (v : Vtx Q) : Prop :=
59	(∃ v' o, Edge w v v' o) ∨ (∃ u o, Edge w u v o)
60
61	/-- All edges of the graph represented by `w` lie on the single directed path
62	`p 0, …, p m` with pairwise distinct vertices and edge labels `lab`: this is
63	what makes the graph a snake graph. -/
64	structure IsSnakePath {Q B : Type} (w : List (SnakeLetter Q B)) (m : ℕ) (p : ℕ → Vtx Q)
65	(lab : ℕ → Option B) : Prop where
66	/-- Consecutive vertices of the path are joined by an edge with the recorded
67	label. -/
68	edge : ∀ t < m, Edge w (p t) (p (t + 1)) (lab t)
69	/-- The vertices of the path are pairwise distinct. -/
70	inj : ∀ s ≤ m, ∀ t ≤ m, p s = p t → s = t
71	/-- Every edge of the graph is an edge of the path. -/
72	covers : ∀ v v' o, Edge w v v' o → ∃ t < m, p t = v ∧ p (t + 1) = v' ∧ lab t = o
73
74	/-- The output along a path: the concatenation of the labels of its edges, the
75	label `none` contributing nothing. -/
76	def pathOut {B : Type} (lab : ℕ → Option B) (m : ℕ) : List B :=
77	((List.range m).map (fun t => (lab t).toList)).flatten
78
79	/-- `v` is the output of the snake graph represented by `w`. -/
80	def SnakeOutIs {Q B : Type} (w : List (SnakeLetter Q B)) (v : List B) : Prop :=
81	∃ m p lab, IsSnakePath w m p lab ∧ v = pathOut lab m
82
83	/-- The number of times the snake visits the column `i`: the number of vertices of
84	that column carrying an edge. -/
85	noncomputable def colVisits {Q B : Type} (w : List (SnakeLetter Q B)) (i : ℕ) : ℕ :=
86	{q : Q \| Incident w (q, i)}.ncard
87
88	/-- The width of the represented graph is at most `k`. -/
89	def SnakeWidthLe {Q B : Type} (w : List (SnakeLetter Q B)) (k : ℕ) : Prop :=
90	∀ i, colVisits w i ≤ k
91
92	open Classical in
93	/-- The function of the snake lemma: the output of the snake graph represented by
94	`w`, if `w` represents one of width at most `k`, and the empty string otherwise.
95	-/
96	noncomputable def snakeOut {Q B : Type} (k : ℕ) (w : List (SnakeLetter Q B)) : List B :=
97	if h : SnakeWidthLe w k ∧ ∃ v, SnakeOutIs w v then h.2.choose else []
98
99	end Lax916827.SnakeGraphs
100

Formalization notes

A letter $SnakeLetter Q B$ assigns to every vertex of the two copies of $Q$ — $(false, q)$ in the left column, $(true, q)$ in the right one — its outgoing edge to the other copy, with a label in $Option B$ , if it has one; the letter at position $i$ of a string carries the edges between the columns $i$ and $i + 1$ , so a string of length $n$ describes a graph on $Q × {0, …, n}$ . The book's special letter for the empty input is not needed: the empty string represents the one-column graph with no edges. A snake path is a directed path with pairwise distinct vertices covering every edge of the graph; a string represents at most one output, so $snakeOut k$ is well defined by a choice. The width of the represented graph is bounded by the number of vertices of a column that carry an edge, and the lemma is stated for every $k$ , not only $k ≤ |Q|$ .

Builds on

none

Used by

Lax916827.SnakeLemma

From Mathlib

Mathlib.Data.Set.Card

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