Subsequential functions and finite-state transducers

A subsequential transducer, in the sense of Schützenberger and Mohri, is a sequential transducer together with a final block of output determined by the ending state. A sequential transducer is a deterministic state machine emitting a block of output for each input symbol, which is a Mealy machine over the output alphabet List β. The functions so computed, subsequential with left- and right-scan variants, form a proper subclass of the rational functions.

We show that each class is closed under composition, that the two are isomorphic under reverse-conjugation, that both contain the Mealy-computable functions, and that left-subsequential functions pull back regular languages; a subsequential function withholds at most a bounded stretch of output (bounded_delay).

Like DFA, this definition allows for machines with infinite states; the classification predicates require a Fintype instance.

Main definitions

• SubsequentialTransducer σ α β: transducer over alphabets α, β and states σ
• SubsequentialTransducer.run / SubsequentialTransducer.runRight: the two passes
• SubsequentialTransducer.comp: the machine computing the composite function
• SubsequentialTransducer.ofWindow: the sliding-window transducer
• DFA.comapSubsequential: pulls an acceptor back along a transducer
• IsLeftSubsequential f, IsRightSubsequential f, IsSubsequential d f: some finite-state transducer computes f in the given scan direction

Main theorems

• IsLeftSubsequential.comp, IsRightSubsequential.comp: closure under composition
• IsMealyComputable.isLeftSubsequential: Mealy-computable functions are left-subsequential
• IsLeftSubsequential.isRegular_preimage, IsRightSubsequential.isRegular_preimage: subsequential functions pull back regular languages
• IsLeftSubsequential.bounded_delay, IsRightSubsequential.bounded_delay: all but boundedly many symbols of f u survive extending the input on the far side

Implementation notes

The name follows Choffrut and Mohri: sequential without state-final output, subsequential with. Sakarovitch calls this class sequential (and the empty-flush case pure sequential), flagging his usage as unconventional (compare Bruyère and Reutenauer); we keep the Choffrut spelling. Mealy is the letter-to-letter case.

step is total, so only the total subsequential functions are modelled, since a sink state does not recover partiality, and Sakarovitch's initial-output function is omitted. The state run stateAfter and its lemmas are those of the underlying Mealy machine. There are two disjoint sets of simp lemmas, one for run and another for runFrom; switch from the former to the latter via simp [run].

TODO

• Choffrut's theorem: a rational function is subsequential iff it has bounded variation, decidably via twinning; bounded_delay is far weaker.
• Canonical forms and minimization; two-way transducers; p-subsequential functions.

References

• [Sch77]
• [Cho77]
• [Moh97]
• [BR99b]
• [Sak09]
• [FR16]

structure SubsequentialTransducer (σ : Type u_4) (α : Type u_5) (β : Type u_6) extends Mealy σ α (List β) : Type (max (max u_4 u_5) u_6)

A subsequential finite-state transducer is a sequential transducer — a Mealy machine whose output is the block of symbols emitted on reading an input symbol in a state — together with a state-final output (finalOutput).

• start : σ
• step : σ → α → σ
• output : σ → α → List β
• finalOutput : σ → List β

  finalOutput s is the block emitted on terminating in the state s.

theorem SubsequentialTransducer.ext {σ : Type u_4} {α : Type u_5} {β : Type u_6} {x y : SubsequentialTransducer σ α β} (start : x.start = y.start) (step : x.step = y.step) (output : x.output = y.output) (finalOutput : x.finalOutput = y.finalOutput) : x = y

theorem SubsequentialTransducer.ext_iff {σ : Type u_4} {α : Type u_5} {β : Type u_6} {x y : SubsequentialTransducer σ α β} : x = y ↔ x.start = y.start ∧ x.step = y.step ∧ x.output = y.output ∧ x.finalOutput = y.finalOutput

@[instance_reducible]

instance instInhabitedSubsequentialTransducer {σ : Type u_1} {α : Type u_2} {β : Type u_3} [Inhabited σ] : Inhabited (SubsequentialTransducer σ α β)

Equations

• instInhabitedSubsequentialTransducer = { default := { toMealy := default, finalOutput := fun (x : σ) => [] } }

def SubsequentialTransducer.emitted {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : SubsequentialTransducer σ α β) (s : σ) (xs : List α) : List β

T.emitted s x is the output emitted while consuming the input x from the state s without the final flush, the concatenated blocks of the sequential run.

Equations

• T.emitted s xs = (T.runFrom s xs).flatten

def SubsequentialTransducer.runFrom {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : SubsequentialTransducer σ α β) (s : σ) (xs : List α) : List β

T.runFrom s x runs T on the input x from the state s, emitting the output followed by the final flush.

Equations

• T.runFrom s xs = T.emitted s xs ++ T.finalOutput (T.stateAfter s xs)

def SubsequentialTransducer.run {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : SubsequentialTransducer σ α β) : List α → List β

T.run x runs T on the input x from the state T.start.

Equations

• T.run = T.runFrom T.start

def SubsequentialTransducer.runRight {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : SubsequentialTransducer σ α β) (xs : List α) : List β

T.runRight x runs T right-to-left on the input x.

Equations

• T.runRight xs = (T.run xs.reverse).reverse

theorem SubsequentialTransducer.runRight_eq_revConj_run {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : SubsequentialTransducer σ α β) : T.runRight = List.revConj T.run

@[simp]

theorem SubsequentialTransducer.emitted_nil {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : SubsequentialTransducer σ α β) (s : σ) : T.emitted s [] = []

@[simp]

theorem SubsequentialTransducer.emitted_cons {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : SubsequentialTransducer σ α β) (s : σ) (x : α) (xs : List α) : T.emitted s (x :: xs) = T.output s x ++ T.emitted (T.step s x) xs

@[simp]

theorem SubsequentialTransducer.runFrom_nil {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : SubsequentialTransducer σ α β) (s : σ) : T.runFrom s [] = T.finalOutput s

@[simp]

theorem SubsequentialTransducer.runFrom_cons {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : SubsequentialTransducer σ α β) (s : σ) (x : α) (xs : List α) : T.runFrom s (x :: xs) = T.output s x ++ T.runFrom (T.step s x) xs

@[simp]

theorem SubsequentialTransducer.run_nil {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : SubsequentialTransducer σ α β) : T.run [] = T.finalOutput T.start

@[simp]

theorem SubsequentialTransducer.runRight_nil {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : SubsequentialTransducer σ α β) : T.runRight [] = (T.finalOutput T.start).reverse

@[simp]

theorem SubsequentialTransducer.runRight_reverse {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : SubsequentialTransducer σ α β) (xs : List α) : T.runRight xs.reverse = (T.run xs).reverse

theorem SubsequentialTransducer.emitted_append {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : SubsequentialTransducer σ α β) (s : σ) (xs ys : List α) : T.emitted s (xs ++ ys) = T.emitted s xs ++ T.emitted (T.stateAfter s xs) ys

theorem SubsequentialTransducer.runFrom_append {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : SubsequentialTransducer σ α β) (s : σ) (xs ys : List α) : T.runFrom s (xs ++ ys) = T.emitted s xs ++ T.runFrom (T.stateAfter s xs) ys

theorem SubsequentialTransducer.run_append {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : SubsequentialTransducer σ α β) (xs ys : List α) : T.run (xs ++ ys) = T.emitted T.start xs ++ T.runFrom (T.stateAfter T.start xs) ys

Transport along state equivalences

def SubsequentialTransducer.map {σ : Type u_1} {α : Type u_2} {β : Type u_3} {τ : Type u_4} (g : σ ≃ τ) (T : SubsequentialTransducer σ α β) : SubsequentialTransducer τ α β

Transport a transducer along an equivalence on states.

Equations

• SubsequentialTransducer.map g T = { toMealy := Mealy.map g T.toMealy, finalOutput := fun (t : τ) => T.finalOutput (g.symm t) }

@[simp]

theorem SubsequentialTransducer.map_toMealy {σ : Type u_1} {α : Type u_2} {β : Type u_3} {τ : Type u_4} (g : σ ≃ τ) (T : SubsequentialTransducer σ α β) : (map g T).toMealy = Mealy.map g T.toMealy

@[simp]

theorem SubsequentialTransducer.map_finalOutput {σ : Type u_1} {α : Type u_2} {β : Type u_3} {τ : Type u_4} (g : σ ≃ τ) (T : SubsequentialTransducer σ α β) (t : τ) : (map g T).finalOutput t = T.finalOutput (g.symm t)

@[simp]

theorem SubsequentialTransducer.map_refl {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : SubsequentialTransducer σ α β) : map (Equiv.refl σ) T = T

@[simp]

theorem SubsequentialTransducer.map_map {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : SubsequentialTransducer σ α β) {τ : Type u_4} {υ : Type u_5} (g : σ ≃ τ) (h : τ ≃ υ) : map h (map g T) = map (g.trans h) T

@[simp]

theorem SubsequentialTransducer.emitted_map {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : SubsequentialTransducer σ α β) {τ : Type u_4} (g : σ ≃ τ) (t : τ) (xs : List α) : (map g T).emitted t xs = T.emitted (g.symm t) xs

@[simp]

theorem SubsequentialTransducer.runFrom_map {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : SubsequentialTransducer σ α β) {τ : Type u_4} (g : σ ≃ τ) (t : τ) (xs : List α) : (map g T).runFrom t xs = T.runFrom (g.symm t) xs

@[simp]

theorem SubsequentialTransducer.run_map {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : SubsequentialTransducer σ α β) {τ : Type u_4} (g : σ ≃ τ) : (map g T).run = T.run

@[simp]

theorem SubsequentialTransducer.runRight_map {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : SubsequentialTransducer σ α β) {τ : Type u_4} (g : σ ≃ τ) : (map g T).runRight = T.runRight

def SubsequentialTransducer.reindex {σ : Type u_1} {α : Type u_2} {β : Type u_3} {τ : Type u_4} (g : σ ≃ τ) : SubsequentialTransducer σ α β ≃ SubsequentialTransducer τ α β

reindex g is map g as an equivalence of machines.

Equations

• SubsequentialTransducer.reindex g = { toFun := SubsequentialTransducer.map g, invFun := SubsequentialTransducer.map g.symm, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem SubsequentialTransducer.coe_reindex {σ : Type u_1} {α : Type u_2} {β : Type u_3} {τ : Type u_4} (g : σ ≃ τ) : ⇑(reindex g) = map g

@[simp]

theorem SubsequentialTransducer.symm_reindex {σ : Type u_1} {α : Type u_2} {β : Type u_3} {τ : Type u_4} (g : σ ≃ τ) : (reindex g).symm = reindex g.symm

Composition

def SubsequentialTransducer.comp {σ : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_5} {σ' : Type u_6} (T₂ : SubsequentialTransducer σ' β γ) (T₁ : SubsequentialTransducer σ α β) : SubsequentialTransducer (σ' × σ) α γ

T₂.comp T₁ feeds each output block of T₁ to T₂, computing T₂.run ∘ T₁.run, which is the construction behind the closure of the subsequential functions under composition [Moh97].

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SubsequentialTransducer.comp_step {σ : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_5} {σ' : Type u_6} (T₂ : SubsequentialTransducer σ' β γ) (T₁ : SubsequentialTransducer σ α β) (p : σ' × σ) (x : α) : (T₂.comp T₁).step p x = (T₂.stateAfter p.1 (T₁.output p.2 x), T₁.step p.2 x)

@[simp]

theorem SubsequentialTransducer.comp_finalOutput {σ : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_5} {σ' : Type u_6} (T₂ : SubsequentialTransducer σ' β γ) (T₁ : SubsequentialTransducer σ α β) (p : σ' × σ) : (T₂.comp T₁).finalOutput p = T₂.runFrom p.1 (T₁.finalOutput p.2)

@[simp]

theorem SubsequentialTransducer.comp_start {σ : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_5} {σ' : Type u_6} (T₂ : SubsequentialTransducer σ' β γ) (T₁ : SubsequentialTransducer σ α β) : (T₂.comp T₁).start = (T₂.start, T₁.start)

@[simp]

theorem SubsequentialTransducer.comp_output {σ : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_5} {σ' : Type u_6} (T₂ : SubsequentialTransducer σ' β γ) (T₁ : SubsequentialTransducer σ α β) (p : σ' × σ) (x : α) : (T₂.comp T₁).output p x = T₂.emitted p.1 (T₁.output p.2 x)

@[simp]

theorem SubsequentialTransducer.runFrom_comp {σ : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_5} {σ' : Type u_6} (T₂ : SubsequentialTransducer σ' β γ) (T₁ : SubsequentialTransducer σ α β) (p : σ' × σ) (xs : List α) : (T₂.comp T₁).runFrom p xs = T₂.runFrom p.1 (T₁.runFrom p.2 xs)

@[simp]

theorem SubsequentialTransducer.run_comp {σ : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_5} {σ' : Type u_6} (T₂ : SubsequentialTransducer σ' β γ) (T₁ : SubsequentialTransducer σ α β) : (T₂.comp T₁).run = T₂.run ∘ T₁.run

Pulling back acceptors

def DFA.comapSubsequential {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : SubsequentialTransducer σ α β) {τ : Type u_5} (M : DFA β τ) : DFA α (σ × τ)

M.comapSubsequential T pulls the acceptor M back along the transducer T. The product machine runs T, feeds each output block to M, and accepts in a state from which M accepts the final flush, so it accepts x if and only if M accepts T.run x.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem DFA.comapSubsequential_step {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : SubsequentialTransducer σ α β) {τ : Type u_5} (M : DFA β τ) (p : σ × τ) (a : α) : (comapSubsequential T M).step p a = (T.step p.1 a, M.evalFrom p.2 (T.output p.1 a))

@[simp]

theorem DFA.comapSubsequential_accept {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : SubsequentialTransducer σ α β) {τ : Type u_5} (M : DFA β τ) : (comapSubsequential T M).accept = {p : σ × τ | M.evalFrom p.2 (T.finalOutput p.1) ∈ M.accept}

@[simp]

theorem DFA.comapSubsequential_start {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : SubsequentialTransducer σ α β) {τ : Type u_5} (M : DFA β τ) : (comapSubsequential T M).start = (T.start, M.start)

@[simp]

theorem DFA.evalFrom_comapSubsequential {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : SubsequentialTransducer σ α β) {τ : Type u_5} (M : DFA β τ) (p : σ × τ) (xs : List α) : (comapSubsequential T M).evalFrom p xs = (T.stateAfter p.1 xs, M.evalFrom p.2 (T.emitted p.1 xs))

@[simp]

theorem DFA.accepts_comapSubsequential {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : SubsequentialTransducer σ α β) {τ : Type u_5} (M : DFA β τ) : (comapSubsequential T M).accepts = T.run ⁻¹' M.accepts

Window transducers

def SubsequentialTransducer.ofWindow {α : Type u_2} {β : Type u_3} {γ : Type u_5} (n : ℕ) (out : List γ → α → List β) (upd : List γ → α → List γ) : SubsequentialTransducer { l : List γ // l.length ≤ n } α β

The transducer whose state is a window of the last n accumulated symbols. out emits from the window and the current symbol, and upd chooses what the window accumulates (fun _ x ↦ [x] for the input, out for the output).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SubsequentialTransducer.ofWindow_step_coe {α : Type u_2} {β : Type u_3} {γ : Type u_5} (n : ℕ) (out : List γ → α → List β) (upd : List γ → α → List γ) (w : { l : List γ // l.length ≤ n }) (x : α) : ↑((ofWindow n out upd).step w x) = (↑w ++ upd (↑w) x).rtake n

@[simp]

theorem SubsequentialTransducer.ofWindow_start_coe {α : Type u_2} {β : Type u_3} {γ : Type u_5} (n : ℕ) (out : List γ → α → List β) (upd : List γ → α → List γ) : ↑(ofWindow n out upd).start = []

@[simp]

theorem SubsequentialTransducer.ofWindow_output {α : Type u_2} {β : Type u_3} {γ : Type u_5} (n : ℕ) (out : List γ → α → List β) (upd : List γ → α → List γ) (w : { l : List γ // l.length ≤ n }) (x : α) : (ofWindow n out upd).output w x = out (↑w) x

@[simp]

theorem SubsequentialTransducer.ofWindow_finalOutput {α : Type u_2} {β : Type u_3} {γ : Type u_5} (n : ℕ) (out : List γ → α → List β) (upd : List γ → α → List γ) (x✝ : { l : List γ // l.length ≤ n }) : (ofWindow n out upd).finalOutput x✝ = []

def SubsequentialTransducer.windowRun {α : Type u_2} {β : Type u_3} {γ : Type u_5} (n : ℕ) (out : List γ → α → List β) (upd : List γ → α → List γ) : List γ → List α → List β

The window recursion computed by ofWindow, each step of which emits out and extends the window by upd, truncated to length n.

Equations

• SubsequentialTransducer.windowRun n out upd x✝ [] = []
• SubsequentialTransducer.windowRun n out upd x✝ (x_2 :: xs) = out x✝ x_2 ++ SubsequentialTransducer.windowRun n out upd ((x✝ ++ upd x✝ x_2).rtake n) xs

theorem SubsequentialTransducer.runFrom_ofWindow {α : Type u_2} {β : Type u_3} {γ : Type u_5} {n : ℕ} {out : List γ → α → List β} {upd : List γ → α → List γ} (w : { l : List γ // l.length ≤ n }) (xs : List α) : (ofWindow n out upd).runFrom w xs = windowRun n out upd (↑w) xs

theorem SubsequentialTransducer.run_ofWindow {α : Type u_2} {β : Type u_3} {γ : Type u_5} {n : ℕ} {out : List γ → α → List β} {upd : List γ → α → List γ} : (ofWindow n out upd).run = windowRun n out upd []

theorem SubsequentialTransducer.windowRun_append_singleton {α : Type u_2} {β : Type u_3} {γ : Type u_5} {n : ℕ} {out : List γ → α → List β} {upd : List γ → α → List γ} {w : List γ} (hw : w.length ≤ n) (u : List α) (x : α) : windowRun n out upd w (u ++ [x]) = windowRun n out upd w u ++ out ((w ++ windowRun n upd upd w u).rtake n) x

The window after reading u is the last n symbols of the update stream, so a window recursion extends by one block per letter.

Letter-to-letter machines as block transducers

A Mealy machine is a SubsequentialTransducer emitting singleton blocks with an empty final flush; LetterToLetter witnesses the singleton blocks, and the two views are mutually inverse.

def Mealy.toSubsequentialTransducer {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : Mealy σ α β) : SubsequentialTransducer σ α β

A Mealy machine as a block SubsequentialTransducer, with singleton outputs and an empty flush.

Equations

• T.toSubsequentialTransducer = { start := T.start, step := T.step, output := fun (s : σ) (x : α) => [T.output s x], finalOutput := fun (x : σ) => [] }

@[simp]

theorem Mealy.toSubsequentialTransducer_finalOutput {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : Mealy σ α β) (x✝ : σ) : T.toSubsequentialTransducer.finalOutput x✝ = []

@[simp]

theorem Mealy.toSubsequentialTransducer_step {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : Mealy σ α β) (a✝ : σ) (a✝¹ : α) : T.toSubsequentialTransducer.step a✝ a✝¹ = T.step a✝ a✝¹

@[simp]

theorem Mealy.toSubsequentialTransducer_output {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : Mealy σ α β) (s : σ) (x : α) : T.toSubsequentialTransducer.output s x = [T.output s x]

@[simp]

theorem Mealy.toSubsequentialTransducer_start {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : Mealy σ α β) : T.toSubsequentialTransducer.start = T.start

@[simp]

theorem Mealy.toSubsequentialTransducer_runFrom {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : Mealy σ α β) (s : σ) (xs : List α) : T.toSubsequentialTransducer.runFrom s xs = T.runFrom s xs

@[simp]

theorem Mealy.toSubsequentialTransducer_run {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : Mealy σ α β) : T.toSubsequentialTransducer.run = T.run

structure SubsequentialTransducer.LetterToLetter {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : SubsequentialTransducer σ α β) : Type (max (max u_1 u_2) u_3)

A witness that every output block of T is a singleton, named by cell.

• cell : σ → α → β

  cell s a is the symbol emitted on reading a in the state s.

• output_eq (s : σ) (x : α) : T.output s x = [self.cell s x]

  Every output block is that singleton.

def SubsequentialTransducer.LetterToLetter.ofLength {σ : Type u_1} {α : Type u_2} {β : Type u_3} {T : SubsequentialTransducer σ α β} (hs : ∀ (s : σ) (x : α), (T.output s x).length = 1) : T.LetterToLetter

Extract a witness from a bound on block lengths.

Equations

• SubsequentialTransducer.LetterToLetter.ofLength hs = { cell := fun (s : σ) (x : α) => (T.output s x).head ⋯, output_eq := ⋯ }

def SubsequentialTransducer.LetterToLetter.toMealy {σ : Type u_1} {α : Type u_2} {β : Type u_3} {T : SubsequentialTransducer σ α β} (w : T.LetterToLetter) : Mealy σ α β

w.toMealy is the Mealy machine emitting each cell's symbol.

Equations

• w.toMealy = { start := T.start, step := T.step, output := w.cell }

@[simp]

theorem SubsequentialTransducer.LetterToLetter.toMealy_output {σ : Type u_1} {α : Type u_2} {β : Type u_3} {T : SubsequentialTransducer σ α β} (w : T.LetterToLetter) (a✝ : σ) (a✝¹ : α) : w.toMealy.output a✝ a✝¹ = w.cell a✝ a✝¹

@[simp]

theorem SubsequentialTransducer.LetterToLetter.toMealy_start {σ : Type u_1} {α : Type u_2} {β : Type u_3} {T : SubsequentialTransducer σ α β} (w : T.LetterToLetter) : w.toMealy.start = T.start

@[simp]

theorem SubsequentialTransducer.LetterToLetter.toMealy_step {σ : Type u_1} {α : Type u_2} {β : Type u_3} {T : SubsequentialTransducer σ α β} (w : T.LetterToLetter) (a✝ : σ) (a✝¹ : α) : w.toMealy.step a✝ a✝¹ = T.step a✝ a✝¹

theorem SubsequentialTransducer.LetterToLetter.runFrom_toMealy {σ : Type u_1} {α : Type u_2} {β : Type u_3} {T : SubsequentialTransducer σ α β} (w : T.LetterToLetter) (hf : ∀ (s : σ), T.finalOutput s = []) (s : σ) (xs : List α) : w.toMealy.runFrom s xs = T.runFrom s xs

theorem SubsequentialTransducer.LetterToLetter.run_toMealy {σ : Type u_1} {α : Type u_2} {β : Type u_3} {T : SubsequentialTransducer σ α β} (w : T.LetterToLetter) (hf : ∀ (s : σ), T.finalOutput s = []) : w.toMealy.run = T.run

theorem SubsequentialTransducer.LetterToLetter.toSubsequentialTransducer_toMealy {σ : Type u_1} {α : Type u_2} {β : Type u_3} {T : SubsequentialTransducer σ α β} (w : T.LetterToLetter) (hf : ∀ (s : σ), T.finalOutput s = []) : w.toMealy.toSubsequentialTransducer = T

A letter-to-letter transducer with no final flush is the block form of its Mealy view.

theorem SubsequentialTransducer.LetterToLetter.isMealyComputable {σ : Type u_1} {α : Type u_2} {β : Type u_3} {T : SubsequentialTransducer σ α β} [Fintype σ] (w : T.LetterToLetter) (hf : ∀ (s : σ), T.finalOutput s = []) : IsMealyComputable T.run

A finite-state letter-to-letter transducer with no final flush computes a Mealy-computable function.

def Mealy.letterToLetter {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : Mealy σ α β) : T.toSubsequentialTransducer.LetterToLetter

The canonical witness that a Mealy machine's block form is letter-to-letter.

Equations

• T.letterToLetter = { cell := T.output, output_eq := ⋯ }

@[simp]

theorem Mealy.toMealy_letterToLetter {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : Mealy σ α β) : T.letterToLetter.toMealy = T

Subsequential classification predicates

def IsLeftSubsequential {α : Type u_2} {β : Type u_3} (f : List α → List β) : Prop

A function f : List α → List β is left-subsequential if some finite-state transducer computes it via left-to-right scan [Moh97].

Equations

• IsLeftSubsequential f = ∃ (σ : Type) (x : Fintype σ) (T : SubsequentialTransducer σ α β), T.run = f

def IsRightSubsequential {α : Type u_2} {β : Type u_3} (f : List α → List β) : Prop

A function f : List α → List β is right-subsequential if its reverse-conjugate is left-subsequential — equivalently, some finite-state transducer computes it via right-to-left scan (isRightSubsequential_iff).

Equations

• IsRightSubsequential f = IsLeftSubsequential (List.revConj f)

def IsSubsequential {α : Type u_2} {β : Type u_3} (d : Edge) (f : List α → List β) : Prop

A function f : List α → List β is subsequential from the edge d if some finite-state transducer computes it by a scan starting from that edge.

Equations

• IsSubsequential Edge.left f = IsLeftSubsequential f
• IsSubsequential Edge.right f = IsRightSubsequential f

@[simp]

theorem isSubsequential_left_iff {α : Type u_2} {β : Type u_3} {f : List α → List β} : IsSubsequential Edge.left f ↔ IsLeftSubsequential f

@[simp]

theorem isSubsequential_right_iff {α : Type u_2} {β : Type u_3} {f : List α → List β} : IsSubsequential Edge.right f ↔ IsRightSubsequential f

theorem isLeftSubsequential_iff {α : Type u_2} {β : Type u_3} {f : List α → List β} : IsLeftSubsequential f ↔ ∃ (σ : Type v) (x : Fintype σ) (T : SubsequentialTransducer σ α β), T.run = f

IsLeftSubsequential holds as soon as a transducer with states in any universe computes f.

theorem isRightSubsequential_iff {α : Type u_2} {β : Type u_3} {f : List α → List β} : IsRightSubsequential f ↔ ∃ (σ : Type v) (x : Fintype σ) (T : SubsequentialTransducer σ α β), T.runRight = f

IsRightSubsequential holds as soon as a transducer with states in any universe computes f right to left.

theorem SubsequentialTransducer.isLeftSubsequential {α : Type u_2} {β : Type u_3} {σ : Type u_5} [Fintype σ] (T : SubsequentialTransducer σ α β) : IsLeftSubsequential T.run

Every finite-state transducer computes a left-subsequential function, whatever the universe of its state type.

theorem SubsequentialTransducer.isRightSubsequential {α : Type u_2} {β : Type u_3} {σ : Type u_5} [Fintype σ] (T : SubsequentialTransducer σ α β) : IsRightSubsequential T.runRight

Every finite-state transducer computes a right-subsequential function via runRight.

Reverse conjugation

theorem IsRightSubsequential.revConj {α : Type u_2} {β : Type u_3} {f : List α → List β} (hf : IsRightSubsequential f) : IsLeftSubsequential (List.revConj f)

The reverse-conjugate of a right-subsequential function is left-subsequential, by definition.

theorem IsLeftSubsequential.revConj {α : Type u_2} {β : Type u_3} {f : List α → List β} (hf : IsLeftSubsequential f) : IsRightSubsequential (List.revConj f)

The reverse-conjugate of a left-subsequential function is right-subsequential.

theorem isLeftSubsequential_revConj_iff {α : Type u_2} {β : Type u_3} {f : List α → List β} : IsLeftSubsequential (List.revConj f) ↔ IsRightSubsequential f

@[simp]

theorem isRightSubsequential_revConj_iff {α : Type u_2} {β : Type u_3} {f : List α → List β} : IsRightSubsequential (List.revConj f) ↔ IsLeftSubsequential f

Mealy-computable functions

theorem IsMealyComputable.isLeftSubsequential {α : Type u_2} {β : Type u_3} {f : List α → List β} (hf : IsMealyComputable f) : IsLeftSubsequential f

A Mealy-computable function is left-subsequential, since Mealy.toSubsequentialTransducer presents a Mealy machine as a block transducer emitting singleton blocks.

theorem Mealy.isLeftSubsequential {α : Type u_2} {β : Type u_3} {σ : Type u_5} [Fintype σ] (T : Mealy σ α β) : IsLeftSubsequential T.run

A finite Mealy machine computes a left-subsequential function.

theorem Mealy.isRightSubsequential {α : Type u_2} {β : Type u_3} {σ : Type u_5} [Fintype σ] (T : Mealy σ α β) : IsRightSubsequential T.runRight

A finite Mealy machine run right-to-left computes a right-subsequential function.

theorem isLeftSubsequential_map {α : Type u_2} {β : Type u_3} (h : α → β) : IsLeftSubsequential (List.map h)

theorem isLeftSubsequential_id {α : Type u_2} : IsLeftSubsequential id

theorem isRightSubsequential_map {α : Type u_2} {β : Type u_3} (h : α → β) : IsRightSubsequential (List.map h)

theorem isRightSubsequential_id {α : Type u_2} : IsRightSubsequential id

theorem isSubsequential_map {α : Type u_2} {β : Type u_3} (d : Edge) (h : α → β) : IsSubsequential d (List.map h)

theorem isSubsequential_id {α : Type u_2} (d : Edge) : IsSubsequential d id

Window functions

theorem isLeftSubsequential_windowRun {α : Type u_2} {β : Type u_3} {δ : Type u_5} [Fintype δ] (n : ℕ) (out : List δ → α → List β) (upd : List δ → α → List δ) : IsLeftSubsequential (SubsequentialTransducer.windowRun n out upd [])

A window recursion over a finite window alphabet is left-subsequential, the bounded window being the state of SubsequentialTransducer.ofWindow.

theorem isMealyComputable_windowRun {α : Type u_2} {β : Type u_3} {δ : Type u_5} [Fintype δ] (n : ℕ) (out : List δ → α → List β) (upd : List δ → α → List δ) (hs : ∀ (w : List δ) (x : α), (out w x).length = 1) : IsMealyComputable (SubsequentialTransducer.windowRun n out upd [])

A window recursion emitting exactly one symbol per step is Mealy-computable, with the bounded window as the synchronous state.

Closure under composition

theorem IsLeftSubsequential.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} {f : List α → List β} {g : List β → List γ} (hg : IsLeftSubsequential g) (hf : IsLeftSubsequential f) : IsLeftSubsequential (g ∘ f)

Left-subsequential functions are closed under composition, by SubsequentialTransducer.comp [Moh97].

theorem IsRightSubsequential.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} {f : List α → List β} {g : List β → List γ} (hg : IsRightSubsequential g) (hf : IsRightSubsequential f) : IsRightSubsequential (g ∘ f)

Right-subsequential functions are closed under composition, by conjugating the left closure.

theorem IsSubsequential.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} {f : List α → List β} {g : List β → List γ} {d : Edge} (hg : IsSubsequential d g) (hf : IsSubsequential d f) : IsSubsequential d (g ∘ f)

Subsequential functions are closed under composition in either scan direction.

Regular preimages

theorem IsLeftSubsequential.isRegular_preimage {α : Type u_2} {β : Type u_3} {f : List α → List β} (hf : IsLeftSubsequential f) {L : Language β} (hL : L.IsRegular) : Language.IsRegular (f ⁻¹' L)

Left-subsequential functions pull back regular languages (DFA.comapSubsequential).

theorem IsRightSubsequential.isRegular_preimage {α : Type u_2} {β : Type u_3} {f : List α → List β} (hf : IsRightSubsequential f) {L : Language β} (hL : L.IsRegular) : Language.IsRegular (f ⁻¹' L)

Right-subsequential functions pull back regular languages, by conjugating the left case through the closure of the regular languages under reversal.

theorem IsSubsequential.isRegular_preimage {α : Type u_2} {β : Type u_3} {f : List α → List β} {d : Edge} (hf : IsSubsequential d f) {L : Language β} (hL : L.IsRegular) : Language.IsRegular (f ⁻¹' L)

Subsequential functions pull back regular languages in either scan direction.

Bounded delay

theorem IsLeftSubsequential.bounded_delay {α : Type u_2} {β : Type u_3} {f : List α → List β} (hf : IsLeftSubsequential f) : ∃ (N : ℕ), ∀ (u v : List α), (f u).rdrop N <+: f (u ++ v)

A left-subsequential function withholds at most the longest state-final output, so all but the last N symbols of f u are a prefix of f (u ++ v). This is much weaker than [Cho77]'s bounded-variation characterization, comparing u only with its own extensions.

theorem IsRightSubsequential.bounded_delay {α : Type u_2} {β : Type u_3} {f : List α → List β} (hf : IsRightSubsequential f) : ∃ (N : ℕ), ∀ (u v : List α), List.drop N (f u) <:+ f (v ++ u)

For a right-subsequential f, all but the first N symbols of f u are a suffix of f (v ++ u).

theorem IsLeftSubsequential.exists_getElem?_append_eq {α : Type u_2} {β : Type u_3} {f : List α → List β} (hf : IsLeftSubsequential f) : ∃ (N : ℕ), ∀ (u v : List α) (i : ℕ), i + N < (f u).length → (f u)[i]? = (f (u ++ v))[i]?

Coordinates of f u more than N positions before its end are stable under extending the input, for a left-subsequential f.

theorem IsLeftSubsequential.exists_dependsOn_Iic {α : Type u_2} {β : Type u_3} {f : List α → List β} (hlen : ∀ (w : List α), (f w).length = w.length) (hf : IsLeftSubsequential f) : ∃ (N : ℕ), ∀ (i n : ℕ), DependsOn (fun (x : Fin n → α) => (f (List.ofFn x))[i]?) (Fin.val ⁻¹' Set.Iic (i + N))

A length-preserving left-subsequential function is oblivious to input beyond a fixed margin of each output coordinate, since the delay bound of exists_getElem?_append_eq caps how far to the right an output coordinate can look.

theorem IsRightSubsequential.exists_getElem?_append_eq {α : Type u_2} {β : Type u_3} {f : List α → List β} (hlen : ∀ (w : List α), (f w).length = w.length) (hf : IsRightSubsequential f) : ∃ (N : ℕ), ∀ (u v : List α) (i : ℕ), N ≤ i → (f u)[i]? = (f (v ++ u))[v.length + i]?

Coordinates of f u at least N positions from its start are stable under extending the input on the left, for a length-preserving right-subsequential f.

theorem IsRightSubsequential.exists_dependsOn_Ici {α : Type u_2} {β : Type u_3} {f : List α → List β} (hlen : ∀ (w : List α), (f w).length = w.length) (hf : IsRightSubsequential f) : ∃ (N : ℕ), ∀ (i n : ℕ), DependsOn (fun (x : Fin n → α) => (f (List.ofFn x))[i]?) (Fin.val ⁻¹' Set.Ici (i - N))

A length-preserving right-subsequential function is oblivious to input beyond a fixed margin to the left of each output coordinate.

theorem not_isLeftSubsequential_of_diverging {α : Type u_2} {β : Type u_3} {f : List α → List β} (h : ∀ (N : ℕ), ∃ (u : List α) (v : List α) (i : ℕ), i + N < (f u).length ∧ (f u)[i]? ≠ (f (u ++ v))[i]?) : ¬IsLeftSubsequential f

f is not left-subsequential if for every N some images f u and f (u ++ v) disagree more than N positions before the end of f u — the contrapositive of bounded_delay.