Synchronous (letter) left-subsequential functions

A Mealy machine is a deterministic left-to-right transducer emitting exactly one output symbol per input symbol — the synchronous case, length-preserving by construction. Its output coordinate i is a function of the input prefix [0..i], so the class is cleanly characterised by the OutputDependsOn footprint (SideDeterminacy.lean): IsLetterLeftSubsequential f → ∀ i, LeftDetermined f i, hence right-myopic.

This is the characterisation the block IsLeftSubsequential (Subsequential.lean) lacks: a length-preserving block transducer can delay output (emit [] then [x,y]), so output coordinate 0 depends on input position 1 — not prefix-determined. The synchronous restriction is what makes the dependency-footprint view line up with the machine view.

Main definitions

• Mealy — synchronous one-symbol-per-step transducer; run is length-preserving.
• IsLetterLeftSubsequential — computed by a finite-state Mealy.

Main results

• Mealy.runFrom_getElem? — output i is (step (state-after-prefix) (input i)).2.
• IsLetterLeftSubsequential.leftDetermined / .isRightMyopic — synchronous left-subsequential maps are prefix-determined, hence right-myopic.

Todo

• The Myhill–Nerode converse: (∀ i, LeftDetermined f i) ∧ finite prefix-congruence ⟹ IsLetterLeftSubsequential f (build the transducer from the prefix-congruence quotient).

structure Subregular.Mealy (σ : Type u_4) (α : Type u_5) (β : Type u_6) : Type (max (max u_4 u_5) u_6)

A synchronous letter-to-letter left-to-right transducer: exactly one output symbol per input symbol (length-preserving by construction).

• initial : σ
• step : σ → α → σ × β

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

State reached after consuming a prefix.

Equations

• T.stateAfter x✝ [] = x✝
• T.stateAfter x✝ (x_2 :: xs) = T.stateAfter (T.step x✝ x_2).1 xs

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

Run from a state: one output symbol per input symbol.

Equations

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

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

Run from the initial state.

Equations

• T.run = T.runFrom T.initial

@[simp]

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

@[simp]

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

@[simp]

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

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

The run is length-preserving (one output symbol per input symbol).

theorem Subregular.Mealy.run_length {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : Mealy σ α β) (xs : List α) : (T.run xs).length = xs.length

theorem Subregular.Mealy.runFrom_getElem? {σ : Type u_1} {α : Type u_2} {β : Type u_3} (T : Mealy σ α β) (s : σ) (xs : List α) (i : ℕ) : (T.runFrom s xs)[i]? = Option.map (fun (x : α) => (T.step (T.stateAfter s (List.take i xs)) x).2) xs[i]?

The coordinate characterization: output i is the step output at (state after the prefix [0..i-1], input i).

Flag machines

The recurring one-sided-trigger shape (the Mealy counterpart of Bimachine.ofFlags): the state is the one-bit "some earlier symbol satisfies p" flag, so stateAfter computes List.any and each output cell sees the flag over its strict prefix. Scanned right-to-left (reverse, run, reverse), the cell sees the flag over its strict suffix (ofFlag_run_reverse_getElem?).

def Subregular.Mealy.ofFlag {α : Type u_2} {β : Type u_3} (p : α → Bool) (out : Bool → α → β) : Mealy Bool α β

The Mealy machine whose state is the monotone flag "a symbol satisfying p has occurred".

Equations

• Subregular.Mealy.ofFlag p out = { initial := false, step := fun (b : Bool) (a : α) => (b || p a, out b a) }

@[simp]

theorem Subregular.Mealy.ofFlag_stateAfter {α : Type u_2} {β : Type u_3} (p : α → Bool) (out : Bool → α → β) (b : Bool) (xs : List α) : (ofFlag p out).stateAfter b xs = (b || xs.any p)

theorem Subregular.Mealy.ofFlag_run_getElem? {α : Type u_2} {β : Type u_3} (p : α → Bool) (out : Bool → α → β) (xs : List α) (i : ℕ) : ((ofFlag p out).run xs)[i]? = Option.map (fun (a : α) => out ((List.take i xs).any p) a) xs[i]?

theorem Subregular.Mealy.ofFlag_run_reverse_getElem? {α : Type u_2} {β : Type u_3} (p : α → Bool) (out : Bool → α → β) (xs : List α) (i : ℕ) : ((ofFlag p out).run xs.reverse).reverse[i]? = Option.map (fun (a : α) => out ((List.drop (i + 1) xs).any p) a) xs[i]?

Coordinates of a flag machine scanned right-to-left: cell i sees the flag over its strict suffix.

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

Transfer a Mealy along a state-space equivalence σ ≃ τ, preserving run. Mirrors SFST.transferEquiv; the use case is bringing a Type* finite state down to Fin (Fintype.card σ) : Type 0 so a universe-polymorphic machine can witness the Type 0-state existential of IsLetterLeftSubsequential.

Equations

• T.transferEquiv e = { initial := e T.initial, step := fun (t : τ) (x : α) => (e (T.step (e.symm t) x).1, (T.step (e.symm t) x).2) }

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

@[simp]

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

The transferred machine computes the same string function.

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

The synchronous left-subsequential class: computed by a finite-state Mealy.

Equations

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

theorem Subregular.Mealy.isLetterLeftSubsequential {σ : Type u_4} [Fintype σ] {α : Type u_5} {β : Type u_6} (T : Mealy σ α β) : IsLetterLeftSubsequential T.run

Constructor lemma: every finite-state Mealy witnesses IsLetterLeftSubsequential for its run. The state σ is accepted at arbitrary Type* and brought down to Fin (Fintype.card σ) : Type 0 via transferEquiv and Fintype.equivFin, so bounded-window ISL/OSL states at the alphabet's universe can witness the predicate (mirrors SFST.isLeftSubsequential).

theorem Subregular.IsLetterLeftSubsequential.leftDetermined {α : Type u_2} {β : Type u_3} {f : List α → List β} (hf : IsLetterLeftSubsequential f) (i : ℕ) : LeftDetermined f i

Forward footprint bridge. A letter-left-subsequential map is left-determined at every coordinate — output i depends only on the prefix {k | k ≤ i}. (The block IsLeftSubsequential lacks this, by delayed output.)

theorem Subregular.IsLetterLeftSubsequential.isRightMyopic {α : Type u_2} {β : Type u_3} {f : List α → List β} (hf : IsLetterLeftSubsequential f) : IsMyopicTowards f Direction.right

A synchronous left-subsequential map is right-myopic — it has no look-ahead.

Myhill–Nerode converse

f is letter-left-subsequential as soon as it admits a finite-state, left-congruent summary that determines its output — the constructive direction of Myhill–Nerode. The finite state plays the role of the prefix-congruence's quotient; δ/out are the induced transition and output. (The natural Nerode congruence, when of finite index, is one such summary — that instantiation is the Todo above.)

theorem Subregular.isLetterLeftSubsequential_of_stateSummary {α : Type u_2} {β : Type u_3} {f : List α → List β} {σ : Type} [Fintype σ] (state : List α → σ) (δ : σ → α → σ) (out : σ → α → β) (hδ : ∀ (u : List α) (x : α), state (u ++ [x]) = δ (state u) x) (hout : ∀ (u : List α) (x : α) (w : List α), (f (u ++ x :: w))[u.length]? = some (out (state u) x)) (hlen : ∀ (xs : List α), (f xs).length = xs.length) : IsLetterLeftSubsequential f

Myhill–Nerode converse (constructive). A length-preserving f with a finite state : List α → σ that is left-congruent (hδ) and determines f's output at each position (hout) is letter-left-subsequential.