Lax916827.ConfigurationGraphs

The string representation of the reachable configuration graph

concepts/Lax916827/ConfigurationGraphs.lean · lax-916827

definition

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

In the paper

page 94 of the paper of lax-157538, Transducers

Definition

The proof of Theorem C.2.2 of Transducers represents the reachable configuration graph of a two-way transducer on a fixed input — the configurations on its run, with the transition between consecutive ones — as a string over a finite alphabet $C$ . The graph is sliced along the letters of the input: the slice at a letter is a bipartite graph whose vertices are two copies of the state space $Q$ , one for the gap to the left of the letter and one for the gap to its right, with a directed edge, labelled by an output string, for every transition of the run that crosses the letter; each vertex has at most one outgoing edge, and it goes to the other copy of $Q$ . The alphabet $C$ consists of these slices, and is finite because only the finitely many output strings occurring in the transition function label edges. A special letter represents the graph of the empty input, which has no letter to slice at.

Lemma C.2.3 says that the map from an input to the representation of its reachable configuration graph is rational; Lemma C.2.4 that the representations whose output string lies in a regular language form a regular language. The output string of a representation is read by a two-way transducer over $C$ that walks along the represented path and prints the labels it meets.

Lean source view on GitHub

1	import Mathlib.Data.Set.Finite.Basic
2	import Lax916827.TwoWayTransducers
3
4	/-!
5	---
6	title: The string representation of the reachable configuration graph
7	type: definition
8	---
9	The proof of Theorem C.2.2 of Transducers represents the *reachable
10	configuration graph* of a two-way transducer on a fixed input — the
11	configurations on its run, with the transition between consecutive ones — as a
12	string over a finite alphabet $C$ . The graph is sliced along the letters of the
13	input: the slice at a letter is a bipartite graph whose vertices are two copies
14	of the state space $Q$ , one for the gap to the left of the letter and one for
15	the gap to its right, with a directed edge, labelled by an output string, for
16	every transition of the run that crosses the letter; each vertex has at most one
17	outgoing edge, and it goes to the other copy of $Q$ . The alphabet $C$ consists
18	of these slices, and is finite because only the finitely many output strings
19	occurring in the transition function label edges. A special letter represents
20	the graph of the empty input, which has no letter to slice at.
21
22	Lemma C.2.3 says that the map from an input to the representation of its
23	reachable configuration graph is rational; Lemma C.2.4 that the representations
24	whose output string lies in a regular language form a regular language. The
25	output string of a representation is read by a two-way transducer over $C$ that
26	walks along the represented path and prints the labels it meets.
27
28	# Formalization notes
29
30	A slice is a function `Bool × Q → VOut Q L` giving the outgoing edge of every
31	vertex: none, an edge to a state of the other copy with a label, or the halting
32	vertex with the label of the halting transition (recorded on both copies of the
33	cut where the transducer halts, since the halting vertex belongs to no copy).
34	The labels are the output strings occurring in the transition function of the
35	transducer, `Lab M`, a finite set. `enc M w` records, in the slice of the letter
36	at position `i`, the outgoing edges of the reachable configurations at the
37	gaps `i` and `i + 1`: a configuration not visited by the run gets no edge, and
38	the empty input gets the special letter carrying the output of the halting
39	transition on the empty input, if the run halts there. `pathTrans M` is the
40	transducer over `C` that walks along the path; on a string that represents
41	nothing its behaviour is irrelevant.
42	-/
43
44	namespace Lax916827.ConfigurationGraphs
45
46	open Lax916827.TwoWayTransducers
47
48	/-- The outgoing edge of a vertex inside one slice: none, an edge to the state `q'`
49	of the other copy labelled `l`, or the halting vertex with the output `l`. -/
50	inductive VOut (Q L : Type) where
51	/-- No outgoing edge inside this slice. -/
52	\| nil : VOut Q L
53	/-- An edge to the state `q'` of the other copy, labelled `l`. -/
54	\| move (q' : Q) (l : L) : VOut Q L
55	/-- The transducer halts here, producing `l`. -/
56	\| halt (l : L) : VOut Q L
57
58	/-- A slice of the configuration graph at a letter: the outgoing edge of every
59	vertex, `(false, q)` being the state `q` at the gap to the left of the letter and
60	`(true, q)` at the gap to its right. -/
61	abbrev Slice (Q L : Type) := Bool × Q → VOut Q L
62
63	/-- The alphabet `C`: the slices, and the special letter for the empty input,
64	carrying the output of the halting transition on the empty input if the run
65	halts there. -/
66	abbrev CLet (Q L : Type) := Slice Q L ⊕ Option L
67
68	namespace TwoWay
69
70	variable {A B Q : Type}
71
72	/-- The output string produced by a transition. -/
73	def transOut (M : TwoWay A B Q) (l : Option A) (q : Q) (r : Option A) : List B :=
74	match M.step l q r with
75	\| Sum.inl o => o
76	\| Sum.inr (_, o, _) => o
77
78	/-- The output strings occurring in the transition function. -/
79	def OutLabels (M : TwoWay A B Q) : Set (List B) :=
80	Set.range (fun p : Option A × Q × Option A => transOut M p.1 p.2.1 p.2.2)
81
82	/-- The finite set of edge labels: the output strings of the transitions. -/
83	abbrev Lab (M : TwoWay A B Q) : Type := {o : List B // o ∈ OutLabels M}
84
85	/-- The label of the edge produced by a transition. -/
86	def labOf (M : TwoWay A B Q) (l : Option A) (q : Q) (r : Option A) : Lab M :=
87	⟨transOut M l q r, ⟨(l, q, r), rfl⟩⟩
88
89	/-- The outgoing edge recorded, in the direction `d`, for the state `q` at a gap
90	with adjacent letters `l` and `r`: the left copy of a slice records the
91	transitions moving right, the right copy those moving left, and a halting
92	transition is recorded on both copies of its gap. -/
93	def edgeOf (M : TwoWay A B Q) (l : Option A) (q : Q) (r : Option A) (d : Bool) : VOut Q (Lab M) :=
94	match M.step l q r with
95	\| Sum.inl _ => VOut.halt (labOf M l q r)
96	\| Sum.inr (q', _, dir) => if dir = d then VOut.move q' (labOf M l q r) else VOut.nil
97
98	/-- The letter to the left of the gap `j` of `w`, if any. -/
99	def prevAt (w : List A) (j : ℕ) : Option A := if j = 0 then none else w[j - 1]?
100
101	open scoped Classical in
102	/-- The outgoing edge, in the direction `d`, of the state `q` at the gap `j` of
103	`w`, for the reachable configurations only: a configuration the run does not
104	visit has no edge. -/
105	noncomputable def cutV (M : TwoWay A B Q) (w : List A) (j : ℕ) (q : Q) (d : Bool) :
106	VOut Q (Lab M) :=
107	if M.Visits w (Cfg.conf (w.take j) q (w.drop j)) then edgeOf M (prevAt w j) q w[j]? d
108	else VOut.nil
109
110	/-- The slice of the reachable configuration graph of `M` on `w` at the letter of
111	position `i`. -/
112	noncomputable def encSlice (M : TwoWay A B Q) (w : List A) (i : ℕ) : Slice Q (Lab M) :=
113	fun v => cutV M w (if v.1 then i + 1 else i) v.2 (!v.1)
114
115	/-- The special letter for the empty input: the output of the halting transition on
116	the empty input, if the run on the empty input halts at once. -/
117	def emptyOut (M : TwoWay A B Q) : Option (Lab M) :=
118	match M.step none M.init none with
119	\| Sum.inl _ => some (labOf M none M.init none)
120	\| Sum.inr _ => none
121
122	/-- The string representation of the reachable configuration graph of `M` on `w`:
123	one slice per input letter, and the special letter for the empty input. -/
124	noncomputable def enc (M : TwoWay A B Q) (w : List A) : List (CLet Q (Lab M)) :=
125	if w.isEmpty then [Sum.inr (emptyOut M)]
126	else (List.range w.length).map (fun i => Sum.inl (encSlice M w i))
127
128	variable {L : Type}
129
130	/-- The outgoing edge at the current gap recorded by the letter to the right of
131	the head. -/
132	def readR (r : Option (CLet Q L)) (q : Q) : VOut Q L :=
133	match r with
134	\| some (Sum.inl s) => s (false, q)
135	\| some (Sum.inr (some lab)) => VOut.halt lab
136	\| _ => VOut.nil
137
138	/-- The outgoing edge at the current gap recorded by the letter to the left of the
139	head. -/
140	def readL (l : Option (CLet Q L)) (q : Q) : VOut Q L :=
141	match l with
142	\| some (Sum.inl s) => s (true, q)
143	\| _ => VOut.nil
144
145	/-- The two-way transducer over `C` that walks along the path of a represented
146	configuration graph, printing the labels of the edges it follows; on a string
147	that represents nothing it halts with empty output. -/
148	def pathTrans (M : TwoWay A B Q) : TwoWay (CLet Q (Lab M)) B Q where
149	init := M.init
150	step := fun l q r =>
151	match readR r q with
152	\| VOut.move q' lab => Sum.inr (q', lab.val, true)
153	\| VOut.halt lab => Sum.inl lab.val
154	\| VOut.nil =>
155	match readL l q with
156	\| VOut.move q' lab => Sum.inr (q', lab.val, false)
157	\| VOut.halt lab => Sum.inl lab.val
158	\| VOut.nil => Sum.inl []
159
160	end TwoWay
161
162	end Lax916827.ConfigurationGraphs
163

Formalization notes

A slice is a function $Bool × Q → VOut Q L$ giving the outgoing edge of every vertex: none, an edge to a state of the other copy with a label, or the halting vertex with the label of the halting transition (recorded on both copies of the cut where the transducer halts, since the halting vertex belongs to no copy). The labels are the output strings occurring in the transition function of the transducer, $Lab M$ , a finite set. $enc M w$ records, in the slice of the letter at position $i$ , the outgoing edges of the reachable configurations at the gaps $i$ and $i + 1$ : a configuration not visited by the run gets no edge, and the empty input gets the special letter carrying the output of the halting transition on the empty input, if the run halts there. $pathTrans M$ is the transducer over $C$ that walks along the path; on a string that represents nothing its behaviour is irrelevant.

Builds on

Lax916827.TwoWayTransducers

Used by

From Mathlib

Mathlib.Data.Set.Finite.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