Lax916827.TwoWayTransducers

Two-way transducers

concepts/Lax916827/TwoWayTransducers.lean · lax-916827

definition

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

In the paper

page 91 of the paper of lax-157538, Transducers

Definition

A two-way transducer (Definition C.2.1 of Transducers) consists of a finite input alphabet $A$ , a finite output alphabet $B$ , a finite set of states $Q$ with an initial state, and a transition function

(A + 1) \times Q \times (A + 1) \;\to\; B^* + (Q \times B^* \times \{-1, +1\})

which, on the letter to the left of the head, the current state and the letter to the right of the head (each possibly missing, at the ends of the input), either produces an output string and halts, or produces an output string, changes state and moves the head left or right. The head sits in a gap between two positions of the input; the run starts in the leftmost gap in the initial state, and the transducer computes $v$ on $w$ if the run started there halts with the concatenation of the produced outputs equal to $v$ . Since the transducer is deterministic, it computes at most one output on every input; a function is computed by a two-way transducer if its graph is.

Lean source view on GitHub

1	import Mathlib.Data.Finite.Defs
2
3	/-!
4	---
5	title: Two-way transducers
6	type: definition
7	---
8	A two-way transducer (Definition C.2.1 of Transducers) consists of a finite
9	input alphabet $A$ , a finite output alphabet $B$ , a finite set of states $Q$
10	with an initial state, and a transition function
11	$(A + 1) \times Q \times (A + 1) \;\to\; B^* + (Q \times B^* \times \{-1, +1\})$
12	which, on the letter to the left of the head, the current state and the letter
13	to the right of the head (each possibly missing, at the ends of the input),
14	either produces an output string and halts, or produces an output string,
15	changes state and moves the head left or right. The head sits in a gap
16	between two positions of the input; the run starts in the leftmost gap in the
17	initial state, and the transducer computes $v$ on $w$ if the run started there
18	halts with the concatenation of the produced outputs equal to $v$ . Since the
19	transducer is deterministic, it computes at most one output on every input; a
20	function is computed by a two-way transducer if its graph is.
21
22	# Formalization notes
23
24	A configuration is the input split at the head, `Cfg.conf u q v` with `u` to
25	the left and `v` to the right, or the halting vertex. `stepCfg` is one step of
26	the machine, `none` when the head would leave the input; `Reaches` is
27	reachability in the configuration graph with the produced output recorded;
28	`Computes M w v` says that the run from the initial configuration halts with
29	output `v`. The run indexed by time, `cfgAt M w n` — `none` once it has halted or
30	got stuck — and the configurations it `Visits` are what the string
31	representation of the reachable configuration graph is built from.
32	`IsTwoWay f` asks for a finite state space and a transducer computing `f w` on
33	every `w`.
34	-/
35
36	namespace Lax916827.TwoWayTransducers
37
38	/-- A two-way transducer: on the letters adjacent to the head and the state, it
39	either produces an output string and halts (`Sum.inl`), or produces an output
40	string, changes state and moves the head left (`false`) or right (`true`). -/
41	structure TwoWay (A B Q : Type) where
42	/-- The initial state. -/
43	init : Q
44	/-- The transition function. -/
45	step : Option A → Q → Option A → List B ⊕ (Q × List B × Bool)
46
47	/-- A configuration: the input to the left of the head, the state, and the input
48	to the right of the head; or the halting vertex. -/
49	inductive Cfg (A Q : Type) : Type
50	\| conf : List A → Q → List A → Cfg A Q
51	\| halt : Cfg A Q
52
53	namespace TwoWay
54
55	variable {A B Q : Type}
56
57	/-- One step of the computation: the produced output and the next configuration,
58	if the head does not fall off the input. -/
59	def stepCfg (M : TwoWay A B Q) : Cfg A Q → Option (List B × Cfg A Q)
60	\| Cfg.halt => none
61	\| Cfg.conf u q v =>
62	match M.step u.getLast? q v.head? with
63	\| Sum.inl o => some (o, Cfg.halt)
64	\| Sum.inr (q', o, true) =>
65	match v with
66	\| [] => none
67	\| a :: v' => some (o, Cfg.conf (u ++ [a]) q' v')
68	\| Sum.inr (q', o, false) =>
69	match u.getLast? with
70	\| none => none
71	\| some a => some (o, Cfg.conf u.dropLast q' (a :: v))
72
73	/-- Reachability in the configuration graph, recording the produced output. -/
74	inductive Reaches (M : TwoWay A B Q) : Cfg A Q → List B → Cfg A Q → Prop
75	\| refl (c : Cfg A Q) : Reaches M c [] c
76	\| step {c c' c'' : Cfg A Q} {o o' : List B} :
77	M.stepCfg c = some (o, c') → Reaches M c' o' c'' → Reaches M c (o ++ o') c''
78
79	/-- The transducer produces the output `v` on the input `w`: the run from the
80	initial configuration reaches the halting vertex with output `v`. -/
81	def Computes (M : TwoWay A B Q) (w : List A) (v : List B) : Prop :=
82	M.Reaches (Cfg.conf [] M.init w) v Cfg.halt
83
84	/-- The configuration of the run on `w` after `n` steps; `none` once the run has
85	halted or got stuck. -/
86	def cfgAt (M : TwoWay A B Q) (w : List A) : ℕ → Option (Cfg A Q)
87	\| 0 => some (Cfg.conf [] M.init w)
88	\| n + 1 => (cfgAt M w n).bind fun c => (M.stepCfg c).map Prod.snd
89
90	/-- A configuration lies on the run of `M` on `w`. -/
91	def Visits (M : TwoWay A B Q) (w : List A) (c : Cfg A Q) : Prop := ∃ n, cfgAt M w n = some c
92
93	end TwoWay
94
95	/-- A function computed by a two-way transducer with a finite state space. -/
96	def IsTwoWay {A B : Type} (f : List A → List B) : Prop :=
97	∃ (Q : Type) (_ : Finite Q) (M : TwoWay A B Q), ∀ w, M.Computes w (f w)
98
99	end Lax916827.TwoWayTransducers
100

Formalization notes

A configuration is the input split at the head, $Cfg.conf u q v$ with $u$ to the left and $v$ to the right, or the halting vertex. $stepCfg$ is one step of the machine, $none$ when the head would leave the input; $Reaches$ is reachability in the configuration graph with the produced output recorded; $Computes M w v$ says that the run from the initial configuration halts with output $v$ . The run indexed by time, $cfgAt M w n$ — $none$ once it has halted or got stuck — and the configurations it $Visits$ are what the string representation of the reachable configuration graph is built from. $IsTwoWay f$ asks for a finite state space and a transducer computing $f w$ on every $w$ .

Builds on

none

Used by

From Mathlib

Mathlib.Data.Finite.Defs

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