Output Strictly Local (OSL) Functions

A function f : List α → List β is k-Output Strictly Local when each output block depends only on the last k - 1 output symbols plus the current input symbol. OSL captures iterative processes where the output already emitted at position i feeds forward to the decision at position i + 1. The function-level subregular hierarchy at this layer is ISL ⊊ OSL ⊊ Subsequential.

Main definitions

• OSLRule k α β — a k-OSL rule: a window-based output function List β → α → List β consuming the (k - 1)-symbol output context plus the current input symbol and emitting an output block.
• OSLRule.apply — the induced string function, threading the output window left-to-right.
• IsLeftOutputStrictlyLocal k f, IsRightOutputStrictlyLocal k f — witness predicates for each scan direction.
• IsOutputStrictlyLocal d k f — direction-parameterised umbrella.

Main results

• isRightOutputStrictlyLocal_iff_left_reverse — Right-OSL is the reverse-conjugate of Left-OSL.
• isLeftOutputStrictlyLocal_left_subsequential — Left-OSL ⊆ Left-Subsequential, via OSLRule.toSFST.

Implementation notes

The witness style IsX k f := ∃ r : OSLRule k α β, r.apply = f mirrors IsLeftInputStrictlyLocal in ISL.lean. Unlike ISL, whose window is over input symbols and threads independently of what was emitted, the OSL window is over already-emitted output — each step truncates outputWindow ++ windowOutput outputWindow x to the last k - 1 symbols before recursing. The k parameter is a type-level annotation; window-length truncation in applyAux is what enforces it semantically.

OSLRule.toSFST deliberately repeats r.windowOutput outputWindow x in the two tuple components of step rather than let-binding it, so that (step ow x).2 reduces definitionally for toSFST_run_eq_apply.

structure Subregular.OSLRule (k : ℕ) (α : Type u_3) (β : Type u_4) : Type (max u_3 u_4)

A k-Output-Strictly-Local rule over input alphabet α and output alphabet β. The single field windowOutput consumes the (k − 1)-symbol output context window plus the current input symbol and emits an output block.

In contrast to ISLRule (whose window is over input symbols), the window here is over already-emitted output symbols. This lets the rule see what it has just produced and react accordingly — the mechanism behind iterative output dependence.

The k parameter is a type-level annotation; semantic enforcement happens in apply's window threading.

• windowOutput : List β → α → List β

  Map from (output context window, current input symbol) to output block. The window argument has length at most k - 1 when called by OSLRule.apply.

def Subregular.OSLRule.applyAux {α : Type u_1} {β : Type u_2} {k : ℕ} (r : OSLRule k α β) (outputWindow : List β) (rest : List α) : List β

Apply the rule, threading a window of accumulated output symbols. At each input position, emit r.windowOutput outputWindow x, then extend the output window with the just-emitted block (truncated to keep at most k − 1 symbols).

Equations

• r.applyAux x✝ [] = []
• r.applyAux x✝ (x_2 :: xs) = r.windowOutput x✝ x_2 ++ r.applyAux ((x✝ ++ r.windowOutput x✝ x_2).rtake (k - 1)) xs

def Subregular.OSLRule.apply {α : Type u_1} {β : Type u_2} {k : ℕ} (r : OSLRule k α β) (input : List α) : List β

Apply a k-OSL rule to an input string, scanning left-to-right.

Equations

• r.apply input = r.applyAux [] input

@[simp]

theorem Subregular.OSLRule.applyAux_nil {α : Type u_1} {β : Type u_2} {k : ℕ} (r : OSLRule k α β) (outputWindow : List β) : r.applyAux outputWindow [] = []

@[simp]

theorem Subregular.OSLRule.applyAux_cons {α : Type u_1} {β : Type u_2} {k : ℕ} (r : OSLRule k α β) (outputWindow : List β) (x : α) (xs : List α) : r.applyAux outputWindow (x :: xs) = r.windowOutput outputWindow x ++ r.applyAux ((outputWindow ++ r.windowOutput outputWindow x).rtake (k - 1)) xs

@[simp]

theorem Subregular.OSLRule.apply_nil {α : Type u_1} {β : Type u_2} {k : ℕ} (r : OSLRule k α β) : r.apply [] = []

@[simp]

theorem Subregular.OSLRule.apply_singleton {α : Type u_1} {β : Type u_2} {k : ℕ} (r : OSLRule k α β) (x : α) : r.apply [x] = r.windowOutput [] x

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

A function f : List α → List β is k-Left-Output-Strictly-Local iff some k-OSL rule computes it via left-to-right scan.

Equations

• Subregular.IsLeftOutputStrictlyLocal k f = ∃ (r : Subregular.OSLRule k α β), r.apply = f

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

A function f : List α → List β is k-Right-Output-Strictly-Local iff some k-OSL rule computes it via right-to-left scan.

Equations

• Subregular.IsRightOutputStrictlyLocal k f = ∃ (r : Subregular.OSLRule k α β), (fun (input : List α) => (r.apply input.reverse).reverse) = f

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

Direction-parameterised OSL predicate.

Equations

• Subregular.IsOutputStrictlyLocal Subregular.Direction.left k f = Subregular.IsLeftOutputStrictlyLocal k f
• Subregular.IsOutputStrictlyLocal Subregular.Direction.right k f = Subregular.IsRightOutputStrictlyLocal k f

@[simp]

theorem Subregular.isOutputStrictlyLocal_left {α : Type u_1} {β : Type u_2} (k : ℕ) (f : List α → List β) : IsOutputStrictlyLocal Direction.left k f ↔ IsLeftOutputStrictlyLocal k f

@[simp]

theorem Subregular.isOutputStrictlyLocal_right {α : Type u_1} {β : Type u_2} (k : ℕ) (f : List α → List β) : IsOutputStrictlyLocal Direction.right k f ↔ IsRightOutputStrictlyLocal k f

theorem Subregular.OSLRule.isLeftOutputStrictlyLocal_apply {α : Type u_1} {β : Type u_2} {k : ℕ} (r : OSLRule k α β) : IsLeftOutputStrictlyLocal k r.apply

Every OSL rule witnesses IsLeftOutputStrictlyLocal for the function it computes.

theorem Subregular.isRightOutputStrictlyLocal_iff_left_reverse {α : Type u_1} {β : Type u_2} {k : ℕ} (f : List α → List β) : IsRightOutputStrictlyLocal k f ↔ IsLeftOutputStrictlyLocal k fun (xs : List α) => (f xs.reverse).reverse

Reverse-conjugation lemma: a function is k-Right-OSL iff its reverse-conjugate is k-Left-OSL. The two classes are isomorphic via the involution f ↦ List.reverse ∘ f ∘ List.reverse.

OSL ⊆ Subsequential

OSLRule.toFinSFST projects an OSL rule into an SFST whose state is the bounded output window (length ≤ k − 1). The inclusion rides on the run-equality plus the Fintype instance for the bounded-window subtype (reusing fintypeListLengthLE from ISL.lean). Co-located on the source side because the dependency direction (SFST in Subsequential.lean; OSL projects into it) forces both construction and cast into this file.

The output alphabet [Fintype β] constraint matches [Moh97]'s finite-alphabet assumption — the state space (a bounded output window) is finite precisely when the output alphabet is.

def Subregular.OSLRule.toFinSFST {α : Type u_1} {β : Type u_2} {k : ℕ} (r : OSLRule k α β) : SFST α β { l : List β // l.length ≤ k - 1 }

Construction: every Left-OSL rule induces an SFST whose state is the output window — a list of output symbols of length at most k − 1 — and whose finalOutput is empty.

The windowOutput call is repeated in the two tuple components rather than let-bound so that (step ow x).2 reduces definitionally to r.windowOutput ow x for the proof of toFinSFST_run_eq_apply.

Equations

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

theorem Subregular.OSLRule.toFinSFST_run_eq_apply {α : Type u_1} {β : Type u_2} {k : ℕ} (r : OSLRule k α β) : r.toFinSFST.run = r.apply

The SFST induced by an OSL rule computes the same string function.

theorem Subregular.isLeftOutputStrictlyLocal_left_subsequential {α : Type u_1} {β : Type u_2} {k : ℕ} [Fintype β] {f : List α → List β} (h : IsLeftOutputStrictlyLocal k f) : IsLeftSubsequential f

Left-OSL ⊆ Left-Subsequential (over a finite output alphabet). The [Fintype β] matches [Moh97]'s finite-alphabet assumption and lets the bounded output window serve as a finite state space.

theorem Subregular.isRightOutputStrictlyLocal_right_subsequential {α : Type u_1} {β : Type u_2} {k : ℕ} [Fintype β] {f : List α → List β} (h : IsRightOutputStrictlyLocal k f) : IsRightSubsequential f

Right-OSL ⊆ Right-Subsequential, derived from the Left- side via the reverse-conjugation lemmas. The Right-OSL ↔ Left-OSL and Right-Subseq ↔ Left-Subseq isomorphisms commute.

theorem Subregular.isOutputStrictlyLocal_isSubsequential {α : Type u_1} {β : Type u_2} {d : Direction} {k : ℕ} [Fintype β] {f : List α → List β} (h : IsOutputStrictlyLocal d k f) : IsSubsequential d f

Direction-parameterised OSL ⊆ Subsequential umbrella: in both scan directions, OSL functions are subsequential. Delegates to the Left- / Right- specialised theorems.