Subsequential Functions and Finite-State Transducers

A function f : List α → List β is subsequential when it is computed by a deterministic finite-state transducer with state-based final output [Moh97]. Subsequential functions form a proper subclass of the rational functions (the functional regular relations).

The class has left and right variants according to scan direction; the two are isomorphic under input/output reversal (f is right-subsequential iff List.reverse ∘ f ∘ List.reverse is left-subsequential).

Main definitions

• SFST α β σ: a deterministic FST with states σ, input alphabet α, output alphabet β, a total output-emitting transition, and a state-indexed finalOutput emitted on termination.
• SFST.run, SFST.runRight: the left-to-right and right-to-left passes.
• IsLeftSubsequential f, IsRightSubsequential f: f is computed by some finite-state SFST scanning in that direction.
• IsSubsequential d f: direction-parameterised umbrella over the two.

Main theorems

• IsLeftSubsequential.comp, IsRightSubsequential.comp, IsSubsequential.comp: subsequential functions are closed under composition (Schützenberger–Choffrut, [Moh97]) — the fact that makes the weakly-deterministic class well-defined.
• isRightSubsequential_iff_left_reverse: the left and right classes are isomorphic via reverse-conjugation.

Implementation notes

SFST models the total subsequential functions: step is total, so run is a total function on List α. Partial subsequential functions can be encoded by adding a sink state.

TODO

• Finite-state minimisation, canonical forms, and SFST equivalence (Choffrut, [Moh97]).
• Two-way subsequential functions (two-way deterministic transducers).
• p-subsequential functions [Moh97] (multiple outputs per input).

structure Subregular.SFST (α : Type u_1) (β : Type u_2) (σ : Type u_3) : Type (max (max u_1 u_2) u_3)

A subsequential finite-state transducer: a deterministic FST with state space σ, input alphabet α, output alphabet β, and state-final outputs [Moh97]. The transition step is total, so the machine computes a total function List α → List β.

• start : σ

  Starting state.

• step : σ → α → σ × List β

  Total deterministic transition: move to a next state and emit a (possibly empty) output block.

• finalOutput : σ → List β

  Output emitted on terminating in a given state.

def Subregular.SFST.runFrom {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : SFST α β σ) : σ → List α → List β

T.runFrom s x runs T from state s, concatenating each step's output block and finally T.finalOutput of the terminating state.

Equations

• T.runFrom x✝ [] = T.finalOutput x✝
• T.runFrom x✝ (x_2 :: xs) = (T.step x✝ x_2).2 ++ T.runFrom (T.step x✝ x_2).1 xs

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

T.run x runs T from its start state; the left-subsequential function T denotes.

Equations

• T.run = T.runFrom T.start

def Subregular.SFST.runRight {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : SFST α β σ) (input : List α) : List β

T.runRight x runs T right-to-left: reverse the input, run, reverse the output.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def Subregular.SFST.runOnList {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : SFST α β σ) : σ → List α → σ × List β

T.runOnList s x walks T from s without the final flush: the terminating state with the concatenated per-step outputs. Building block for compose.

Equations

• T.runOnList x✝ [] = (x✝, [])
• T.runOnList x✝ (x_2 :: xs) = match T.step x✝ x_2 with | (s', out) => Prod.map id (fun (x : List β) => out ++ x) (T.runOnList s' xs)

@[simp]

theorem Subregular.SFST.runOnList_nil {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : SFST α β σ) (s : σ) : T.runOnList s [] = (s, [])

@[simp]

theorem Subregular.SFST.runOnList_cons {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : SFST α β σ) (s : σ) (x : α) (xs : List α) : T.runOnList s (x :: xs) = ((T.runOnList (T.step s x).1 xs).1, (T.step s x).2 ++ (T.runOnList (T.step s x).1 xs).2)

theorem Subregular.SFST.runFrom_eq_runOnList {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : SFST α β σ) (s : σ) (xs : List α) : T.runFrom s xs = (T.runOnList s xs).2 ++ T.finalOutput (T.runOnList s xs).1

The relationship between runFrom and runOnList: runFrom is runOnList followed by appending the final-state output.

theorem Subregular.SFST.runOnList_append {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : SFST α β σ) (s : σ) (xs ys : List α) : T.runOnList s (xs ++ ys) = ((T.runOnList (T.runOnList s xs).1 ys).1, (T.runOnList s xs).2 ++ (T.runOnList (T.runOnList s xs).1 ys).2)

runOnList distributes over input concatenation: walking on xs ++ ys equals walking on xs then on ys from the resulting state, with outputs concatenated.

theorem Subregular.SFST.runFrom_append {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : SFST α β σ) (s : σ) (xs ys : List α) : T.runFrom s (xs ++ ys) = (T.runOnList s xs).2 ++ T.runFrom (T.runOnList s xs).1 ys

runFrom distributes over input concatenation: walking on xs ++ ys equals walking the prefix via runOnList (no final emission yet), then running runFrom from the resulting state on ys (which DOES include the final emission).

State-space transfer

Transferring an SFST along a state-space equivalence preserves its run function. The headline use case is bringing a universe-polymorphic state down to Fin n (universe Type 0) via Fintype.equivFin, which lets the universe-polymorphic constructions in ISL.lean / OSL.lean witness the Type 0-state existential of IsLeftSubsequential / IsRightSubsequential.

def Subregular.SFST.transferEquiv {σ : Type u_1} {τ : Type u_2} {α : Type u_3} {β : Type u_4} (T : SFST α β σ) (e : σ ≃ τ) : SFST α β τ

Transfer an SFST along a state-space equivalence σ ≃ τ. Replaces each state-valued field with the corresponding τ-valued one via the equivalence.

Equations

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

theorem Subregular.SFST.transferEquiv_runFrom {σ : Type u_1} {τ : Type u_2} {α : Type u_3} {β : Type u_4} (T : SFST α β σ) (e : σ ≃ τ) (s : σ) (xs : List α) : (T.transferEquiv e).runFrom (e s) xs = T.runFrom s xs

@[simp]

theorem Subregular.SFST.transferEquiv_run {σ : Type u_1} {τ : Type u_2} {α : Type u_3} {β : Type u_4} (T : SFST α β σ) (e : σ ≃ τ) : (T.transferEquiv e).run = T.run

The transferred SFST computes the same string function as the original.

Composition

Subsequential functions are closed under composition ([Moh97], back to Schützenberger and Choffrut). This is the load-bearing fact that makes the weakly-deterministic class (compositions of two subsequentials) well-defined.

Construction: the product SFST with state σ_f × σ_g threads both machines, where the consumer FST T_g walks over each output block emitted by the producer FST T_f.

def Subregular.SFST.compose {σf : Type u_1} {σg : Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_5} (Tg : SFST β γ σg) (Tf : SFST α β σf) : SFST α γ (σf × σg)

Compose two SFSTs: T_f : SFST α β σ_f and T_g : SFST β γ σ_g yield an SFST with state σ_f × σ_g whose run computes T_g.run ∘ T_f.run.

State threading: each input symbol triggers one T_f step (which may emit a multi-symbol β block); T_g then walks through that block via runOnList, advancing its state. The combined finalOutput runs T_f.finalOutput through T_g (including T_g's own final flush).

Equations

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

theorem Subregular.SFST.compose_runFrom {σf : Type u_1} {σg : Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_5} (Tg : SFST β γ σg) (Tf : SFST α β σf) (s : σf × σg) (xs : List α) : (Tg.compose Tf).runFrom s xs = Tg.runFrom s.2 (Tf.runFrom s.1 xs)

compose's runFrom agrees with sequential runFroms: the product SFST compose Tg Tf walks Tf over the input from s.1, threading each emitted block through Tg from s.2.

Subsequential classification predicates

The witness-style predicates below follow mathlib's Language.IsRegular shape: the state space σ is existentially quantified at Type with a Fintype σ instance, while the alphabets α β are universe-polymorphic at Type*. The Fintype constraint matches the source literature ([Moh97]), where every SFST has finitely many states by definition, and also lets the universe parameter for state collapse cleanly without universe declarations or ULift coercions.

Constructor lemmas (SFST.isLeftSubsequential, SFST.isRightSubsequential below) hide the existential-over-types shape so future redesigns (e.g. to a Myhill–Nerode finite-index characterization with σ ≃ Fin n) won't touch consumer sites. Downstream ISL/OSL inclusion theorems take [Fintype α] / [Fintype β] and use a bounded-window finite state to witness the predicate (Function/{ISL,OSL}.lean).

def Subregular.IsLeftSubsequential {α : Type u_1} {β : Type u_2} (f : List α → List β) : Prop

A function f : List α → List β is left-subsequential iff some SFST with a finite state space computes it via left-to-right scan. The Fintype σ constraint matches the source literature [Moh97].

Equations

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

def Subregular.IsRightSubsequential {α : Type u_1} {β : Type u_2} (f : List α → List β) : Prop

A function f : List α → List β is right-subsequential iff some SFST with a finite state space computes it via right-to-left scan (runRight).

Equations

• Subregular.IsRightSubsequential f = ∃ (σ : Type) (x : Fintype σ) (T : Subregular.SFST α β σ), T.runRight = f

def Subregular.IsSubsequential {α : Type u_1} {β : Type u_2} (d : Direction) (f : List α → List β) : Prop

A function f : List α → List β is subsequential in direction d iff some finite-state SFST computes it via the corresponding scan direction. Direction-parameterised umbrella; concrete claims should typically use one of IsLeftSubsequential / IsRightSubsequential directly for clarity.

Equations

• Subregular.IsSubsequential Subregular.Direction.left f = Subregular.IsLeftSubsequential f
• Subregular.IsSubsequential Subregular.Direction.right f = Subregular.IsRightSubsequential f

@[simp]

theorem Subregular.isSubsequential_left {α : Type u_1} {β : Type u_2} (f : List α → List β) : IsSubsequential Direction.left f ↔ IsLeftSubsequential f

@[simp]

theorem Subregular.isSubsequential_right {α : Type u_1} {β : Type u_2} (f : List α → List β) : IsSubsequential Direction.right f ↔ IsRightSubsequential f

theorem Subregular.SFST.isLeftSubsequential {α : Type u_1} {β : Type u_2} {σ : Type u_4} [Fintype σ] (T : SFST α β σ) : IsLeftSubsequential T.run

Every finite-state SFST witnesses IsLeftSubsequential for its run. Consumers use T.isLeftSubsequential instead of building the existential quadruple, so a redesign of IsLeftSubsequential touches only this lemma. The arbitrary-Type* state is brought down to Fin (Fintype.card σ) via SFST.transferEquiv and Fintype.equivFin.

theorem Subregular.SFST.isRightSubsequential {α : Type u_1} {β : Type u_2} {σ : Type u_4} [Fintype σ] (T : SFST α β σ) : IsRightSubsequential T.runRight

Every finite-state SFST witnesses IsRightSubsequential for its runRight. See SFST.isLeftSubsequential for rationale.

theorem Subregular.isRightSubsequential_iff_left_reverse {α : Type u_1} {β : Type u_2} (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: the two classes are isomorphic via the involution f ↦ List.reverse ∘ f ∘ List.reverse.

theorem Subregular.IsLeftSubsequential.bounded_delay {α : Type u_1} {β : Type u_2} {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 has bounded delay ([Moh97]): on any input u it has already emitted a prefix of f u shared with f (u ++ v) for every continuation v, withholding at most the longest state-final output.

theorem Subregular.not_isLeftSubsequential_of_diverging {α : Type u_1} {β : Type u_2} {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 working form of bounded_delay for impossibility proofs (e.g. unbounded tonal plateauing, [Jar16]).

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

Subsequential functions are closed under composition ([Moh97], originally Schützenberger and Choffrut) — the load-bearing fact that makes the weakly-deterministic class (composition of two subsequential functions reading from opposite directions) well-defined. The product state σf × σg inherits Fintype from Mathlib.Data.Fintype.Prod.

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

Right-Subsequential closure under composition, derived from the Left- counterpart via isRightSubsequential_iff_left_reverse: the reverse-conjugate of a composition is the composition of reverse-conjugates.

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

Direction-parameterised composition closure: both Left- and Right-Subsequential functions are closed under composition. Delegates to IsLeftSubsequential.comp / IsRightSubsequential.comp.