Lax194892.PebbleTransducers

Pebble transducers

concepts/Lax194892/PebbleTransducers.lean · lax-194892

definition

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

In the paper

page 165 of the paper of lax-157538, Transducers

Definition

A pebble transducer (Section D.2 of Transducers) extends a two-way transducer by a stack of at most $k$ pebbles pointing to gaps of the input string; the topmost pebble is the head, and only it can be moved. The transducer has a finite set of states with an initial state; it looks at its state and, for every pebble on the stack, at the two input letters adjacent to it and the set of pebbles in the same place, and deterministically chooses a new state and an action: output a letter, move the head one position left or right, push a new pebble at the first gap, pop the head, or terminate. It computes $v$ on $w$ if the run from the initial state with an empty stack terminates with output $v$ . Pebble transducers compute exactly the functions of for-transducers (Theorem D.2.4), hence the polyregular functions.

Lean source view on GitHub

1	import Mathlib.Data.Finite.Defs
2	import Mathlib.Data.List.Basic
3
4	/-!
5	---
6	title: Pebble transducers
7	type: definition
8	---
9	A pebble transducer (Section D.2 of Transducers) extends a two-way
10	transducer by a stack of at most $k$ pebbles pointing to gaps of the input
11	string; the topmost pebble is the head, and only it can be moved. The
12	transducer has a finite set of states with an initial state; it looks at its
13	state and, for every pebble on the stack, at the two input letters adjacent to
14	it and the set of pebbles in the same place, and deterministically chooses a
15	new state and an action: output a letter, move the head one position left or
16	right, push a new pebble at the first gap, pop the head, or terminate. It
17	computes $v$ on $w$ if the run from the initial state with an empty stack
18	terminates with output $v$ . Pebble transducers compute exactly the functions of
19	for-transducers (Theorem D.2.4), hence the polyregular functions.
20
21	# Formalization notes
22
23	The information available to the transducer is its `PebbleView`: for each
24	pebble, from the bottom of the stack, the two adjacent letters and the Booleans
25	saying which pebbles share its place. A configuration is a state and the stack
26	of gaps, or the halting vertex; a step is undefined if the head would leave the
27	input, the stack bound would be exceeded, or an empty stack popped. `IsPebbleTransducer`
28	asks for some bound `k`, a finite state space and a transducer computing `f w`
29	on every `w`.
30	-/
31
32	namespace Lax194892.PebbleTransducers
33
34	/-- What a pebble transducer sees: for every pebble on the stack, from the
35	bottom, the two adjacent letters and the pebbles in the same place. -/
36	abbrev PebbleView (A : Type) := List ((Option A × Option A) × List Bool)
37
38	/-- The view of the input from a stack of gaps. -/
39	def viewOf {A : Type} (w : List A) (st : List ℕ) : PebbleView A :=
40	st.map (fun p => ((if p = 0 then none else w[p - 1]?, w[p]?),
41	st.map (fun q => decide (q = p))))
42
43	/-- The actions of a pebble transducer. -/
44	inductive PebbleAction (B : Type) : Type
45	/-- Output a letter. -/
46	\| out : B → PebbleAction B
47	/-- Move the head right (`true`) or left (`false`). -/
48	\| move : Bool → PebbleAction B
49	/-- Push a new pebble at the first gap. -/
50	\| push : PebbleAction B
51	/-- Pop the topmost pebble. -/
52	\| pop : PebbleAction B
53	/-- Terminate. -/
54	\| terminate : PebbleAction B
55
56	/-- A `k`-pebble transducer: a deterministic machine with a stack of at most `k`
57	pebbles pointing to gaps of the input. -/
58	structure Pebble (A B Q : Type) (k : ℕ) where
59	/-- The initial state. -/
60	init : Q
61	/-- The transition function. -/
62	step : Q → PebbleView A → Q × PebbleAction B
63
64	/-- A configuration: the state and the stack of gaps (from the bottom), or the
65	halting vertex. -/
66	inductive PebbleCfg (Q : Type) : Type
67	\| conf : Q → List ℕ → PebbleCfg Q
68	\| halt : PebbleCfg Q
69
70	namespace Pebble
71
72	variable {A B Q : Type} {k : ℕ}
73
74	/-- One step: the produced output and the next configuration, undefined if the
75	head leaves the input, the stack bound is exceeded, or an empty stack is popped. -/
76	def stepCfg (M : Pebble A B Q k) (w : List A) : PebbleCfg Q → Option (List B × PebbleCfg Q)
77	\| PebbleCfg.halt => none
78	\| PebbleCfg.conf q st =>
79	let r := M.step q (viewOf w st)
80	match r.2 with
81	\| PebbleAction.out b => some ([b], PebbleCfg.conf r.1 st)
82	\| PebbleAction.terminate => some ([], PebbleCfg.halt)
83	\| PebbleAction.push =>
84	if st.length < k then some ([], PebbleCfg.conf r.1 (st ++ [0])) else none
85	\| PebbleAction.pop =>
86	if st = [] then none else some ([], PebbleCfg.conf r.1 st.dropLast)
87	\| PebbleAction.move dir =>
88	match st.getLast? with
89	\| none => none
90	\| some p =>
91	if dir then
92	(if p < w.length then some ([], PebbleCfg.conf r.1 (st.dropLast ++ [p + 1]))
93	else none)
94	else
95	(if 0 < p then some ([], PebbleCfg.conf r.1 (st.dropLast ++ [p - 1]))
96	else none)
97
98	/-- Reachability in the configuration graph, recording the output. -/
99	inductive Reaches (M : Pebble A B Q k) (w : List A) :
100	PebbleCfg Q → List B → PebbleCfg Q → Prop
101	\| refl (c : PebbleCfg Q) : Reaches M w c [] c
102	\| step {c c' c'' : PebbleCfg Q} {o o' : List B} :
103	M.stepCfg w c = some (o, c') → Reaches M w c' o' c'' → Reaches M w c (o ++ o') c''
104
105	/-- The transducer produces `v` on `w`. -/
106	def Computes (M : Pebble A B Q k) (w : List A) (v : List B) : Prop :=
107	M.Reaches w (PebbleCfg.conf M.init []) v PebbleCfg.halt
108
109	end Pebble
110
111	/-- A function computed by a pebble transducer with finitely many states, for some
112	bound on the number of pebbles. -/
113	def IsPebbleTransducer {A B : Type} (f : List A → List B) : Prop :=
114	∃ (k : ℕ) (Q : Type) (_ : Finite Q) (M : Pebble A B Q k), ∀ w, M.Computes w (f w)
115
116	end Lax194892.PebbleTransducers
117

Formalization notes

The information available to the transducer is its $PebbleView$ : for each pebble, from the bottom of the stack, the two adjacent letters and the Booleans saying which pebbles share its place. A configuration is a state and the stack of gaps, or the halting vertex; a step is undefined if the head would leave the input, the stack bound would be exceeded, or an empty stack popped. $IsPebbleTransducer$ asks for some bound $k$ , a finite state space and a transducer computing $f w$ on every $w$ .

Builds on

none

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