Lax916827.StreamingStringTransducers

Streaming string transducers

concepts/Lax916827/StreamingStringTransducers.lean · lax-916827

definition

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

In the paper

page 109 of the paper of lax-157538, Transducers

Definition

A streaming string transducer (Definition C.3.1 of Transducers) processes its input in a single left-to-right pass, storing intermediate results in finitely many registers that hold strings over the output alphabet. It has a finite set of states with an initial state, a finite set of registers, all initially empty, and a transition function that on a state and an input letter gives a new state and a register update: for every register, a string over the output alphabet and the register names, which is evaluated by substituting the current contents of the registers. Updates are copyless: each register name occurs at most once across all the strings of an update, so that no register content is ever duplicated. After the whole input has been read, a final output string over the output alphabet and the register names, chosen by the final state, is evaluated in the same way. Streaming string transducers compute exactly the regular functions (Theorem C.3.2).

Lean source view on GitHub

1	import Mathlib.Data.Fintype.Basic
2	import Mathlib.Data.List.Basic
3
4	/-!
5	---
6	title: Streaming string transducers
7	type: definition
8	---
9	A streaming string transducer (Definition C.3.1 of Transducers) processes
10	its input in a single left-to-right pass, storing intermediate results in
11	finitely many registers that hold strings over the output alphabet. It has a
12	finite set of states with an initial state, a finite set of registers, all
13	initially empty, and a transition function that on a state and an input letter
14	gives a new state and a register update: for every register, a string over
15	the output alphabet and the register names, which is evaluated by substituting
16	the current contents of the registers. Updates are copyless: each register
17	name occurs at most once across all the strings of an update, so that no
18	register content is ever duplicated. After the whole input has been read, a
19	final output string over the output alphabet and the register names, chosen by
20	the final state, is evaluated in the same way. Streaming string transducers
21	compute exactly the regular functions (Theorem C.3.2).
22
23	# Formalization notes
24
25	A string over the output alphabet and the register names is a `List (X ⊕ B)`;
26	`subst η s` substitutes the contents `η` of the registers into it. `Copyless`
27	counts the register occurrences over all registers, which needs the register
28	set to be a `Fintype` (for the enumeration), whereas the state space is only
29	required to be finite in `IsSST`. The copyless restriction is part of the
30	structure, as in the definition.
31	-/
32
33	namespace Lax916827.StreamingStringTransducers
34
35	/-- A register update is copyless if each register name occurs at most once in the
36	concatenation of the strings assigned to the registers. -/
37	def Copyless {X B : Type} [Fintype X] (u : X → List (X ⊕ B)) : Prop :=
38	((Finset.univ.toList.map u).flatten.filterMap
39	(fun z => match z with \| Sum.inl x => some x \| Sum.inr _ => none)).Nodup
40
41	/-- A streaming string transducer with states `Q` and registers `X`. -/
42	structure SST (A B Q X : Type) [Fintype X] where
43	/-- The initial state. -/
44	init : Q
45	/-- The transition function: a new state and a register update. -/
46	step : Q → A → Q × (X → List (X ⊕ B))
47	/-- Every register update is copyless. -/
48	step_copyless : ∀ q a, Copyless (step q a).2
49	/-- The final output string, chosen by the final state. -/
50	final : Q → List (X ⊕ B)
51
52	namespace SST
53
54	variable {A B Q X : Type} [Fintype X]
55
56	/-- Substituting the contents of the registers into a string over `X + B`. -/
57	def subst (η : X → List B) (s : List (X ⊕ B)) : List B :=
58	(s.map (fun z => match z with \| Sum.inl x => η x \| Sum.inr b => [b])).flatten
59
60	/-- Reading one input letter: the new state and the new register contents. -/
61	def stepConfig (T : SST A B Q X) (c : Q × (X → List B)) (a : A) : Q × (X → List B) :=
62	((T.step c.1 a).1, fun x => subst c.2 ((T.step c.1 a).2 x))
63
64	/-- The state and register contents after reading an input string, starting from
65	the initial state with empty registers. -/
66	def runConfig (T : SST A B Q X) (w : List A) : Q × (X → List B) :=
67	w.foldl T.stepConfig (T.init, fun _ => [])
68
69	/-- The semantics: the final output string of the last state, with the final
70	register contents substituted. -/
71	def eval (T : SST A B Q X) (w : List A) : List B :=
72	subst (T.runConfig w).2 (T.final (T.runConfig w).1)
73
74	end SST
75
76	/-- A function computed by a streaming string transducer with finite state space
77	and finitely many registers. -/
78	def IsSST {A B : Type} (f : List A → List B) : Prop :=
79	∃ (Q X : Type) (_ : Finite Q) (instX : Fintype X) (T : @SST A B Q X instX), T.eval = f
80
81	end Lax916827.StreamingStringTransducers
82

Formalization notes

A string over the output alphabet and the register names is a $List (X ⊕ B)$ ; $subst η s$ substitutes the contents $η$ of the registers into it. $Copyless$ counts the register occurrences over all registers, which needs the register set to be a $Fintype$ (for the enumeration), whereas the state space is only required to be finite in $IsSST$ . The copyless restriction is part of the structure, as in the definition.

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