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

Implementation notes

The witness style IsX k f := ∃ r : OSLRule k α β, r.apply = f mirrors Subregular.IsLeftInputStrictlyLocal. 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.

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 its reverse-conjugate is k-Left-OSL — some k-OSL rule computes it via right-to-left scan.

Equations

• Subregular.IsRightOutputStrictlyLocal k f = Subregular.IsLeftOutputStrictlyLocal k (List.revConj f)

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

ScanDirection-parameterised OSL predicate.

Equations

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

@[simp]

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

@[simp]

theorem Subregular.isOutputStrictlyLocal_right {α : Type u_1} {β : Type u_2} (k : ℕ) (f : List α → List β) : IsOutputStrictlyLocal ScanDirection.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 — definitionally, with the conjugated class as primary.

OSL ⊆ Subsequential

OSLRule.toFinSubsequentialTransducer projects an OSL rule into the sliding-window transducer SubsequentialTransducer.ofWindow, with the bounded output window (length ≤ k − 1) as state. Co-located on the source side because the dependency direction (the transducer lives 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.toFinSubsequentialTransducer {α : Type u_1} {β : Type u_2} {k : ℕ} (r : OSLRule k α β) : SubsequentialTransducer { l : List β // l.length ≤ k - 1 } α β

Every Left-OSL rule induces a window transducer tracking the last k − 1 output symbols (the window accumulates what windowOutput emits), with empty finalOutput.

Equations

• r.toFinSubsequentialTransducer = SubsequentialTransducer.ofWindow (k - 1) r.windowOutput r.windowOutput

theorem Subregular.OSLRule.applyAux_eq_windowRun {α : Type u_1} {β : Type u_2} {k : ℕ} (r : OSLRule k α β) : r.applyAux = SubsequentialTransducer.windowRun (k - 1) r.windowOutput r.windowOutput

OSLRule.applyAux is the canonical window recursion accumulating the output.

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

The window transducer 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.isMealyComputable_of_OSLRule {α : Type u_1} {β : Type u_2} {k : ℕ} [Fintype β] (r : OSLRule k α β) (hs : ∀ (w : List β) (x : α), (r.windowOutput w x).length = 1) : IsMealyComputable r.apply

A single-symbol left-OSL rule is Mealy-computable, with the bounded output window as the synchronous state.

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: the left inclusion at the reverse-conjugate, since both right classes are the List.revConj-images of their left classes.

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

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