Lax194892.ChildConfigurationGraphs

Children of a configuration and child configuration graphs

concepts/Lax194892/ChildConfigurationGraphs.lean · lax-194892

definition

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

In the paper

page 169 of the paper of lax-157538, Transducers

Definition

Section D.2 of Transducers organises a run of a pebble transducer as a tree: the children of a configuration of height $\ell$ are the configurations of height $\ell + 1$ that the run visits after it before coming back down to height $\ell$ ; between two consecutive children the run stays above height $\ell + 1$ . The children are described by the child configuration graph: a directed graph whose vertices are pairs of a state and a gap — the position of the moving pebble $\ell + 1$ — with an edge for the run between two consecutive children, annotated with the input string and the positions of the fixed pebbles $1, \ldots, \ell$ . Like a configuration, a child configuration graph is represented as a string over a fixed finite alphabet with one letter per gap of the input, and the output of the graph is the concatenation of the string representations of the children in order of execution. Lemma D.2.5 and Claims D.2.6–D.2.7 say that a for-transducer computes the graph from the configuration and the children from the graph.

Lean source view on GitHub

1	import Mathlib.Data.Nat.Find
2	import Mathlib.Data.Finite.Defs
3	import Lax194892.PebbleConfigurationEncoding
4
5	/-!
6	---
7	title: Children of a configuration and child configuration graphs
8	type: definition
9	---
10	Section D.2 of Transducers organises a run of a pebble transducer as a
11	tree: the children of a configuration of height $\ell$ are the configurations
12	of height $\ell + 1$ that the run visits after it before coming back down to
13	height $\ell$ ; between two consecutive children the run stays above height
14	$\ell + 1$ . The children are described by the child configuration graph: a
15	directed graph whose vertices are pairs of a state and a gap — the position of
16	the moving pebble $\ell + 1$ — with an edge for the run between two consecutive
17	children, annotated with the input string and the positions of the fixed
18	pebbles $1, \ldots, \ell$ . Like a configuration, a child configuration graph is
19	represented as a string over a fixed finite alphabet with one letter per gap of
20	the input, and the output of the graph is the concatenation of the string
21	representations of the children in order of execution. Lemma D.2.5 and Claims
22	D.2.6–D.2.7 say that a for-transducer computes the graph from the configuration
23	and the children from the graph.
24
25	# Formalization notes
26
27	A child is the vertex `(q, p)` standing for the configuration whose stack is
28	the parent's with the gap `p` on top (`cfgOf`); `FirstChild` and `NextChild` are
29	runs that stay strictly above the children's height (`StrictAbove`, a run of at
30	least one step whose intermediate configurations have height at least `h`),
31	and `IsChildSeq M w q st ch m` says that `ch 0, …, ch m` is the list of the
32	children of `(q, st)`. `confEnc` is the string representation of a single
33	configuration (the shape of `PebbleConfigurationEncoding`, for one
34	configuration). A letter of the child configuration graph carries the input
35	letter, the fixed pebbles of the gap, the index of the moving pebble, which
36	states are the first child in this column, and for every state the outgoing
37	and the incoming edge of the vertex, the latter redundant but what makes the
38	representation locally checkable (`Chk`). `cgOfChildren` is the representation
39	of the graph of a configuration with children `ch`, and `CGOutIs u v` says
40	that `v` is the concatenation of the children's representations read off the
41	graph `u` (`CGPath`); a string determines at most one such `v`.
42	-/
43
44	namespace Lax194892.ChildConfigurationGraphs
45
46	open Lax194892.PebbleTransducers Lax194892.PebbleConfigurationEncoding
47
48	-- ## The children of a configuration
49
50	/-- The stack has height at least `h`; the halting vertex has no height. -/
51	def HeightGe {Q : Type} (h : ℕ) : PebbleCfg Q → Prop
52	\| PebbleCfg.conf _ st => h ≤ st.length
53	\| PebbleCfg.halt => False
54
55	/-- A run of at least one step whose intermediate configurations have height at
56	least `h`. -/
57	inductive StrictAbove {A B Q : Type} {k : ℕ} (M : Pebble A B Q k) (w : List A) (h : ℕ) :
58	PebbleCfg Q → PebbleCfg Q → Prop
59	/-- A single step. -/
60	\| one {c c' : PebbleCfg Q} {o : List B} : M.stepCfg w c = some (o, c') → StrictAbove M w h c c'
61	/-- A step to a configuration of height at least `h`, followed by such a run. -/
62	\| cons {c c' c'' : PebbleCfg Q} {o : List B} : M.stepCfg w c = some (o, c') → HeightGe h c' →
63	StrictAbove M w h c' c'' → StrictAbove M w h c c''
64
65	/-- A vertex of a child configuration graph: a state and a gap. -/
66	abbrev Vtx (Q : Type) := Q × ℕ
67
68	/-- The configuration of the child `v` of a configuration with stack `st`: the
69	moving pebble sits on top. -/
70	def cfgOf {Q : Type} (st : List ℕ) (v : Vtx Q) : PebbleCfg Q := PebbleCfg.conf v.1 (st ++ [v.2])
71
72	/-- `v'` is the child following the child `v`: the run from `v` first returns to
73	the children's height at `v'`. -/
74	def NextChild {A B Q : Type} {k : ℕ} (M : Pebble A B Q k) (w : List A) (st : List ℕ)
75	(v v' : Vtx Q) : Prop :=
76	StrictAbove M w (st.length + 2) (cfgOf st v) (cfgOf st v')
77
78	/-- `v` is the first child of the configuration `(q, st)`. -/
79	def FirstChild {A B Q : Type} {k : ℕ} (M : Pebble A B Q k) (w : List A) (q : Q) (st : List ℕ)
80	(v : Vtx Q) : Prop :=
81	StrictAbove M w (st.length + 2) (PebbleCfg.conf q st) (cfgOf st v)
82
83	/-- `ch 0, …, ch m` is the list of the children of `(q, st)`, in order of
84	execution. -/
85	structure IsChildSeq {A B Q : Type} {k : ℕ} (M : Pebble A B Q k) (w : List A) (q : Q)
86	(st : List ℕ) (ch : ℕ → Vtx Q) (m : ℕ) : Prop where
87	/-- The list starts with the first child. -/
88	first : FirstChild M w q st (ch 0)
89	/-- Each child is followed by the next one. -/
90	next : ∀ t < m, NextChild M w st (ch t) (ch (t + 1))
91	/-- The last child has no successor. -/
92	stop : ∀ v, ¬ NextChild M w st (ch m) v
93
94	-- ## String representations
95
96	/-- A letter of the representation of a configuration: the state, the input letter
97	following the gap, and the pebbles in the gap. -/
98	abbrev ConfLetter (A Q : Type) (k : ℕ) := Q × Option A × (Fin k → Bool)
99
100	/-- The string representation of the configuration `(q, st)` of `w`: one letter per
101	gap. -/
102	def confEnc {A Q : Type} {k : ℕ} (q : Q) (st : List ℕ) (w : List A) : List (ConfLetter A Q k) :=
103	(List.range (w.length + 1)).map fun p => (q, w[p]?, ann k st p)
104
105	/-- The direction of an edge: inside the column, one column right, one column left. -/
106	abbrev Dir := Option Bool
107
108	/-- The column that the direction `d` leads to from the column `p`. -/
109	def dest (p : ℕ) : Dir → Option ℕ
110	\| none => some p
111	\| some true => some (p + 1)
112	\| some false => if p = 0 then none else some (p - 1)
113
114	/-- The direction from the column `a` to the adjacent column `b`. -/
115	def dirOf (a b : ℕ) : Dir := if b = a then none else if a < b then some true else some false
116
117	/-- A letter of the representation of a child configuration graph: one gap of the
118	input, with the input letter, the fixed pebbles, the index of the moving pebble,
119	the states that are the first child in this column, and the outgoing and
120	incoming edges of the vertices of this column. -/
121	structure CGLetter (A Q : Type) (k : ℕ) where
122	/-- The input letter following this gap, absent for the last gap. -/
123	lett : Option A
124	/-- The fixed pebbles sitting in this gap. -/
125	peb : Fin k → Bool
126	/-- The index of the moving pebble. -/
127	nid : Fin k
128	/-- The states `q` for which `(q, this column)` is the first child. -/
129	src : Q → Bool
130	/-- The outgoing edge of `(q, this column)`. -/
131	nxt : Q → Option (Q × Dir)
132	/-- The incoming edge of `(q, this column)`. -/
133	prv : Q → Option (Q × Dir)
134
135	open scoped Classical in
136	/-- The index at which `v` occurs among the first `m` children, if any. -/
137	noncomputable def idxAt {Q : Type} (ch : ℕ → Vtx Q) (m : ℕ) (v : Vtx Q) : Option ℕ :=
138	if h : ∃ t, t < m ∧ ch t = v then some (Nat.find h) else none
139
140	open scoped Classical in
141	/-- The index `t < m` such that `v` is the child following `ch t`, if any. -/
142	noncomputable def idxSuccAt {Q : Type} (ch : ℕ → Vtx Q) (m : ℕ) (v : Vtx Q) : Option ℕ :=
143	if h : ∃ t, t < m ∧ ch (t + 1) = v then some (Nat.find h) else none
144
145	open scoped Classical in
146	/-- The representation of the child configuration graph whose children are
147	`ch 0, …, ch m`, over an input with `n + 1` gaps carrying the letters `lett` and
148	the fixed pebbles `peb`, the moving pebble having the index `nid`. -/
149	noncomputable def cgOfPath {A Q : Type} {k : ℕ} (lett : ℕ → Option A) (peb : ℕ → Fin k → Bool)
150	(nid : Fin k) (n : ℕ) (ch : ℕ → Vtx Q) (m : ℕ) : List (CGLetter A Q k) :=
151	(List.range (n + 1)).map fun j =>
152	{ lett := lett j
153	peb := peb j
154	nid := nid
155	src := fun q' => decide ((q', j) = ch 0)
156	nxt := fun q' => (idxAt ch m (q', j)).map fun t => ((ch (t + 1)).1, dirOf j (ch (t + 1)).2)
157	prv := fun q' => (idxSuccAt ch m (q', j)).map fun t => ((ch t).1, dirOf (ch t).2 j) }
158
159	/-- The representation of the child configuration graph of a configuration of `w`
160	with stack `st`, moving pebble `nid` and children `ch 0, …, ch m`. -/
161	noncomputable def cgOfChildren {A Q : Type} {k : ℕ} (w : List A) (st : List ℕ) (nid : Fin k)
162	(ch : ℕ → Vtx Q) (m : ℕ) : List (CGLetter A Q k) :=
163	cgOfPath (fun j => w[j]?) (fun j => ann k st j) nid w.length ch m
164
165	-- ## Reading the children off a represented graph
166
167	/-- The vertex that the edge out of `v` leads to, if any. -/
168	def succOf {A Q : Type} {k : ℕ} (u : List (CGLetter A Q k)) (v : Vtx Q) : Option (Vtx Q) :=
169	(u[v.2]?).bind fun c => (c.nxt v.1).bind fun x => (dest v.2 x.2).map fun p' => (x.1, p')
170
171	/-- `v` is marked as the first child. -/
172	def IsSrc {A Q : Type} {k : ℕ} (u : List (CGLetter A Q k)) (v : Vtx Q) : Prop :=
173	∃ c, u[v.2]? = some c ∧ c.src v.1 = true
174
175	/-- The representation of the child that the vertex `v` stands for: the state of
176	`v`, the input letters and the fixed pebbles of the graph, and the moving pebble
177	in the column of `v`. -/
178	def confAt {A Q : Type} {k : ℕ} (u : List (CGLetter A Q k)) (v : Vtx Q) :
179	List (ConfLetter A Q k) :=
180	u.mapIdx fun j c => (v.1, c.lett, fun i => c.peb i \|\| (decide (i = c.nid) && decide (v.2 = j)))
181
182	/-- The letter to the left of the gap `i`. -/
183	def leftLet {A Q : Type} {k : ℕ} (u : List (CGLetter A Q k)) (i : ℕ) : Option (CGLetter A Q k) :=
184	if i = 0 then none else u[i - 1]?
185
186	open Classical in
187	/-- The local consistency test on two adjacent letters: every edge recorded by
188	`nxt` between or inside their columns is recorded by `prv` at its target, and a
189	vertex marked as the first child has no incoming edge. -/
190	noncomputable def pairOK {A Q : Type} {k : ℕ} (a b : Option (CGLetter A Q k)) : Bool := decide (
191	(∀ q q' : Q, ∀ ca cb, a = some ca → b = some cb → ca.nxt q = some (q', some true) →
192	cb.prv q' = some (q, some true)) ∧
193	(∀ q q' : Q, ∀ ca cb, a = some ca → b = some cb → cb.nxt q = some (q', some false) →
194	ca.prv q' = some (q, some false)) ∧
195	(∀ q q' : Q, ∀ cb, b = some cb → cb.nxt q = some (q', none) → cb.prv q' = some (q, none)) ∧
196	(∀ q : Q, ∀ cb, b = some cb → cb.src q = true → cb.prv q = none))
197
198	/-- The string is locally consistent at every gap. -/
199	def Chk {A Q : Type} {k : ℕ} (u : List (CGLetter A Q k)) : Prop :=
200	∀ i ≤ u.length, pairOK (leftLet u i) u[i]? = true
201
202	/-- `p 0, …, p m` is the run of children described by the locally consistent
203	string `u`: `p 0` is the unique first child, each `p (t+1)` is reached from `p t`
204	by the recorded edge, and `p m` has no outgoing edge. -/
205	structure CGPath {A Q : Type} {k : ℕ} (u : List (CGLetter A Q k)) (m : ℕ) (p : ℕ → Vtx Q) :
206	Prop where
207	/-- The string is locally consistent. -/
208	chk : Chk u
209	/-- `p 0` is the unique vertex marked as the first child. -/
210	srcEq : ∀ v, IsSrc u v ↔ v = p 0
211	/-- Every vertex of the run sits in a real column. -/
212	inRange : ∀ t ≤ m, (u[(p t).2]?).isSome
213	/-- Consecutive children are joined by the recorded edge. -/
214	step : ∀ t < m, succOf u (p t) = some (p (t + 1))
215	/-- The last child has no outgoing edge. -/
216	last : succOf u (p m) = none
217
218	/-- The concatenation of the representations of the children, in order. -/
219	def cgOut {A Q : Type} {k : ℕ} (u : List (CGLetter A Q k)) (m : ℕ) (p : ℕ → Vtx Q) :
220	List (ConfLetter A Q k) :=
221	((List.range (m + 1)).map fun t => confAt u (p t)).flatten
222
223	/-- `v` is the string representation of the children of the configuration whose
224	child configuration graph `u` represents. -/
225	def CGOutIs {A Q : Type} {k : ℕ} (u : List (CGLetter A Q k)) (v : List (ConfLetter A Q k)) :
226	Prop :=
227	∃ m p, CGPath u m p ∧ v = cgOut u m p
228
229	end Lax194892.ChildConfigurationGraphs
230

Formalization notes

A child is the vertex $(q, p)$ standing for the configuration whose stack is the parent's with the gap $p$ on top ( $cfgOf$ ); $FirstChild$ and $NextChild$ are runs that stay strictly above the children's height ( $StrictAbove$ , a run of at least one step whose intermediate configurations have height at least $h$ ), and $IsChildSeq M w q st ch m$ says that $ch 0, …, ch m$ is the list of the children of $(q, st)$ . $confEnc$ is the string representation of a single configuration (the shape of $PebbleConfigurationEncoding$ , for one configuration). A letter of the child configuration graph carries the input letter, the fixed pebbles of the gap, the index of the moving pebble, which states are the first child in this column, and for every state the outgoing and the incoming edge of the vertex, the latter redundant but what makes the representation locally checkable ( $Chk$ ). $cgOfChildren$ is the representation of the graph of a configuration with children $ch$ , and $CGOutIs u v$ says that $v$ is the concatenation of the children's representations read off the graph $u$ ( $CGPath$ ); a string determines at most one such $v$ .

Builds on

Lax194892.PebbleConfigurationEncoding

Used by

From Mathlib

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