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 @cite{mohri-1997}. Subsequential functions form a proper subclass of the regular relations (= rational functions) and a proper superclass of the Output Strictly Local class @cite{aksenova-rawski-graf-heinz-2020}.

The class comes in left and right variants depending on whether the FST consumes input left-to-right or right-to-left @cite{meinhardt-mai-bakovic-mccollum-2024}. The right-subsequential class equals the image of the left-subsequential class under input/output reversal: f ∈ R-Subseq ↔ (List.reverse ∘ f ∘ List.reverse) ∈ L-Subseq.

Main definitions

• Direction — .left or .right; orientation of the FST scan.
• SFST σ α β — a deterministic finite-state transducer with state space σ, input alphabet α, output alphabet β, total transition emitting an output block, plus a state-indexed finalOutput emitted on termination.
• SFST.run — left-to-right pass: input → output.
• SFST.runRight — right-to-left pass via List.reverse-conjugation.
• IsSubsequential d f — predicate witness-style: some SFST computes f under direction d.

What this file does NOT cover

• Finite-state minimisation, canonical forms, equivalence of SFSTs (Choffrut 1979, Mohri 1997 §5).
• Two-way subsequential functions (extended class for some reduplication patterns, Dolatian-Heinz 2020).
• p-subsequential functions (Mohri 1997 footnote 7) — handle variation/optionality with multiple outputs per input.

Direction of FST scan

Direction (left or right) controls whether an FST consumes its input head-first (left scan) or tail-first via List.reverse conjugation (right scan). The two scan modes give rise to distinct function classes isomorphic under reversal but not equal as subclasses of the regular functions over un-reversed strings.

Re-exported from Core/Direction.lean so the classification predicates below can use .left/.right unqualified.

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

A subsequential finite-state transducer with state space σ, input alphabet α, output alphabet β. The scan is total deterministic — step always returns a next state and an output block — and the FST emits finalOutput on terminating in any state.

This is the standard subsequential model of @cite{mohri-1997}: a deterministic FST with state-final outputs, computing partial functions extended to total functions on List α. We model totality by requiring step to be total; partial subsequential functions can be encoded by adding a none/sink state.

• initial : σ

  The starting state from which scans begin.

• step : σ → α → σ × List β

  Total deterministic transition: at each state, on each input symbol, move to a next state and emit a (possibly empty) output block.

• finalOutput : σ → List β

  Output emitted upon terminating in a given state.

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

Run the FST starting from a given state, accumulating output. The scan walks left-to-right, emitting each transition's output block, and finally appends the terminating state's finalOutput.

Equations

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

def Core.Computability.Subregular.Function.SFST.run {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : SFST σ α β) (input : List α) : List β

Run the FST from its initial state. The standard left-subsequential function denoted by T.

Equations

• T.run input = T.runFrom T.initial input

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

Right-subsequential application: reverse the input, run the FST left-to-right, then reverse the output. The standard "right-to-left scan" interpretation.

Equations

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

@[simp]

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

@[simp]

theorem Core.Computability.Subregular.Function.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).snd ++ T.runFrom (T.step s x).fst xs

@[simp]

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

@[simp]

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

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

Walk an SFST over an input list without appending the final-state output. Returns the terminating state and the concatenation of all transition outputs along the way.

Useful as a building block for product constructions (e.g. composition closure): the consumer FST may need to see only the transition outputs of the producer, not the producer's final flush.

Equations

• T.runOnList x✝ [] = (x✝, [])
• T.runOnList x✝ (x_2 :: xs) = match T.step x✝ x_2 with | (s', out) => match T.runOnList s' xs with | (s'', rest) => (s'', out ++ rest)

@[simp]

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

@[simp]

theorem Core.Computability.Subregular.Function.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).fst xs).fst, (T.step s x).snd ++ (T.runOnList (T.step s x).fst xs).snd)

theorem Core.Computability.Subregular.Function.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).snd ++ T.finalOutput (T.runOnList s xs).fst

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

theorem Core.Computability.Subregular.Function.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).fst ys).fst, (T.runOnList s xs).snd ++ (T.runOnList (T.runOnList s xs).fst ys).snd)

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

theorem Core.Computability.Subregular.Function.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).snd ++ T.runFrom (T.runOnList s xs).fst 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).

Composition

Subsequential functions are closed under composition (Mohri 1997 §3, back to Schützenberger and Choffrut). This is the load-bearing fact that makes the Heinz-Lai 2013 Weakly Deterministic class definition work (compositions of two subsequentials).

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 Core.Computability.Subregular.Function.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 σ_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 Core.Computability.Subregular.Function.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.snd (Tf.runFrom s.fst 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.

Universe-level constraint on classification predicates

The witness-style predicates below restrict alphabet binders to Type 0 rather than Type*. The reason: ∃ σ : Type, ∃ T : SFST σ α β, … requires σ's universe to be fixed at definition site (a σ at universe w plus alphabets at universes u, v would force the body into universe max u v w, which Prop accepts only with ULift/PLift boilerplate). Phonological alphabets are concrete inductive types at Type 0, so the constraint is non-binding for current consumers; if a Type* consumer ever appears, lift via ULift or duplicate predicates at the needed universe rather than universe-polymorphising in place.

def Core.Computability.Subregular.Function.IsLeftSubsequential {α β : Type} (f : List α → List β) : Prop

A function f : List α → List β is left-subsequential iff some SFST computes it via left-to-right scan.

Equations

• Core.Computability.Subregular.Function.IsLeftSubsequential f = ∃ (σ : Type), ∃ (T : Core.Computability.Subregular.Function.SFST σ α β), T.run = f

def Core.Computability.Subregular.Function.IsRightSubsequential {α β : Type} (f : List α → List β) : Prop

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

Equations

• Core.Computability.Subregular.Function.IsRightSubsequential f = ∃ (σ : Type), ∃ (T : Core.Computability.Subregular.Function.SFST σ α β), T.runRight = f

def Core.Computability.Subregular.Function.IsSubsequential {α β : Type} (d : Direction) (f : List α → List β) : Prop

A function f : List α → List β is subsequential in direction d iff some SFST computes it via the corresponding scan direction. The audit-recommended Direction-parameterised form (rather than separate Left/Right files); concrete claims should typically use one of IsLeftSubsequential / IsRightSubsequential directly for clarity.

Equations

• Core.Computability.Subregular.Function.IsSubsequential Core.Direction.left f = Core.Computability.Subregular.Function.IsLeftSubsequential f
• Core.Computability.Subregular.Function.IsSubsequential Core.Direction.right f = Core.Computability.Subregular.Function.IsRightSubsequential f

@[simp]

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

@[simp]

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

theorem Core.Computability.Subregular.Function.isRightSubsequential_iff_left_reverse {α β : Type} (f : List α → List β) : IsRightSubsequential f ↔ IsLeftSubsequential fun (xs : List α) => (f xs.reverse).reverse

Reverse-conjugation lemma: 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 Core.Computability.Subregular.Function.IsLeftSubsequential.comp {α β γ : Type} {g : List β → List γ} (hg : IsLeftSubsequential g) {f : List α → List β} (hf : IsLeftSubsequential f) : IsLeftSubsequential (g ∘ f)

Subsequential functions are closed under composition (Mohri 1997 §3, originally Schützenberger and Choffrut). The load-bearing fact that makes the Heinz-Lai 2013 Weakly Deterministic class definition work as the composition of two subsequential functions reading from opposite directions.