Subsequential functions and finite-state transducers

A subsequential transducer is a deterministic state machine which maps strings to strings, emitting a block of output for each input symbol and a final block determined by the ending state [Sch77] [Moh97]. The functions so computed — subsequential, with left- and right-scan variants — form a proper subclass of the rational functions [FR16].

We show that each class is closed under composition, that the two are isomorphic under reverse-conjugation, and that both contain the Mealy-computable functions; a left-subsequential function withholds at most a bounded output suffix (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.ofWindow: the sliding-window transducer
• IsLeftSubsequential f, IsRightSubsequential f, IsSubsequential d f: some finite-state transducer computes f in the given scan direction

Implementation notes

The name follows [Cho77] and [Moh97]: sequential without state-final output, subsequential with. [Sak09] calls this class sequential (and the empty-flush case pure sequential), flagging his usage as unconventional (cf. [BR99b]); we keep the Choffrut spelling. Mealy is the letter-to-letter case.

step is total, so only the total subsequential functions are modelled — a sink state does not recover partiality — and the initial-output function of [Sak09] is omitted. 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 [Cho77]: 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.

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

A subsequential finite-state transducer is a set of states (σ), a starting state (start), a transition function (step), a per-symbol output function (output) and a state-final output (finalOutput).

• start : σ

  Starting state.

• step : σ → α → σ

  Transition function.

• output : σ → α → List β

  The block of output symbols emitted on reading an input symbol in a state.

• finalOutput : σ → List β

  Output emitted on terminating in a state.

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

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

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

T.stateAfter s x is the state reached from s after consuming the input x.

Equations

• T.stateAfter s = List.foldl T.step s

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

T.emitted s x is the output emitted while consuming the input x from the state s, without the final flush.

Equations

• T.emitted x✝ [] = []
• T.emitted x✝ (x_2 :: xs) = T.output x✝ x_2 ++ T.emitted (T.step x✝ x_2) xs

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: the emitted 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.stateAfter_nil {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : SubsequentialTransducer σ α β) (s : σ) : T.stateAfter s [] = s

@[simp]

theorem SubsequentialTransducer.stateAfter_cons {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : SubsequentialTransducer σ α β) (s : σ) (x : α) (xs : List α) : T.stateAfter s (x :: xs) = T.stateAfter (T.step s x) xs

@[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.stateAfter_append {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : SubsequentialTransducer σ α β) (s : σ) (xs ys : List α) : T.stateAfter s (xs ++ ys) = T.stateAfter (T.stateAfter s xs) ys

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[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.stateAfter_map {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : SubsequentialTransducer σ α β) {τ : Type u_4} (g : σ ≃ τ) (t : τ) (xs : List α) : (map g T).stateAfter t xs = g (T.stateAfter (g.symm t) xs)

@[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 τ α β

map 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₂ — the classical product construction [Moh97] — computing T₂.run ∘ T₁.run.

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_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.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.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

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; 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_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_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_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✝ = []

@[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

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 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 []

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 σ α β

View a Mealy machine as a block SubsequentialTransducer: singleton outputs, empty flush.

Equations

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

@[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 : σ → α → β

  The single symbol emitted at a cell.

• 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 σ α β

The Mealy machine emitting each cell's symbol.

Equations

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

@[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✝¹

@[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_initial {σ : Type u_1} {α : Type u_2} {β : Type u_3} {T : SubsequentialTransducer σ α β} (w : T.LetterToLetter) : w.toMealy.initial = T.start

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 : ScanDirection) (f : List α → List β) : Prop

A function f : List α → List β is subsequential in direction d if some finite-state SubsequentialTransducer computes it via the corresponding scan direction.

Equations

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

@[simp]

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

@[simp]

theorem isSubsequential_right_iff {α : Type u_2} {β : Type u_3} {f : List α → List β} : IsSubsequential ScanDirection.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

The universe-polymorphic form of IsLeftSubsequential.

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

The universe-polymorphic form of IsRightSubsequential, in the runRight shape.

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.

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

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

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

theorem isLeftSubsequential_id {α : Type u_2} : IsLeftSubsequential id

theorem isRightSubsequential_iff_left_reverse {α : Type u_2} {β : Type u_3} {f : List α → List β} : IsRightSubsequential f ↔ IsLeftSubsequential fun (xs : List α) => (f xs.reverse).reverse

A function is right-subsequential iff its reverse-conjugate is left-subsequential — definitionally: the right class is the List.revConj-image of the left class.

theorem IsLeftSubsequential.bounded_delay {α : Type u_2} {β : Type u_3} {f : List α → List β} (hf : IsLeftSubsequential f) : ∃ (N : ℕ), ∀ (u v : List α), ∃ (p : List β) (su : List β) (sv : List β), f u = p ++ su ∧ f (u ++ v) = p ++ sv ∧ su.length ≤ N

A left-subsequential function withholds at most the longest state-final output: f u and f (u ++ v) share a prefix covering all but boundedly many symbols of f u. Much weaker than [Cho77]'s bounded-variation characterization — this compares u only with its own extensions.

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]?

The coordinate form of bounded_delay: coordinates of f u more than N positions before its end are stable under extending the input.

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 : ℕ), List.DependsOn (fun (u : List α) => (f u)[i]?) (Set.Iic (i + N))

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

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.

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 the classical product construction [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 closure under composition: conjugate the left closure.

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

Subsequential functions are closed under composition in either scan direction.