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 @cite{chandlee-eyraud-heinz-2015}. The OSL class captures iterative spreading processes — patterns where the spreading feature value of segment i depends on the spreading feature value of segment i − 1 (already determined by the OSL function), not on the underlying input value.

Like Subsequential, OSL has left and right variants depending on scan direction. Left-OSL: each output block depends on previous output (processed left-to-right). Right-OSL: each output block depends on following output (process right-to-left).

OSL is properly contained in Subsequential and properly contains ISL @cite{aksenova-rawski-graf-heinz-2020}. The proper containments are:

• ISL ⊊ OSL: many iterative spreading patterns (e.g. progressive nasal harmony) are OSL but not ISL — output decisions feed forward.
• OSL ⊊ Subsequential: subsequential FSTs can carry richer state than bounded output windows; iterative-with-blocking patterns may need this.

Bidirectional iterative harmony patterns (Maasai, Turkana ATR harmony) are above all unidirectional OSL classes — they need the Weakly Deterministic class @cite{heinz-lai-2013} @cite{meinhardt-mai-bakovic-mccollum-2024}.

Main definitions

• OSLRule k α β — a k-OSL rule: a window-based output function (List β) → α → List β that consumes the (k − 1)-symbol output context plus the current input symbol and emits an output block.
• OSLRule.apply r — the induced string function List α → List β, threading the output window left-to-right.
• IsLeftOutputStrictlyLocal k f, IsRightOutputStrictlyLocal k f, IsOutputStrictlyLocal d k f — Direction-parameterised predicates.

structure Core.Computability.Subregular.Function.OSLRule (k : ℕ) (α : Type u_1) (β : Type u_2) : Type (max u_1 u_2)

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

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 Core.Computability.Subregular.Function.OSLRule.applyAux {α β : Type} {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 (Core.Computability.Subregular.Function.lastN (k - 1) (x✝ ++ r.windowOutput x✝ x_2)) xs

def Core.Computability.Subregular.Function.OSLRule.apply {α β : Type} {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 Core.Computability.Subregular.Function.OSLRule.applyAux_nil {α β : Type} {k : ℕ} (r : OSLRule k α β) (outputWindow : List β) : r.applyAux outputWindow [] = []

@[simp]

theorem Core.Computability.Subregular.Function.OSLRule.applyAux_cons {α β : Type} {k : ℕ} (r : OSLRule k α β) (outputWindow : List β) (x : α) (xs : List α) : r.applyAux outputWindow (x :: xs) = r.windowOutput outputWindow x ++ r.applyAux (lastN (k - 1) (outputWindow ++ r.windowOutput outputWindow x)) xs

@[simp]

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

@[simp]

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

def Core.Computability.Subregular.Function.IsLeftOutputStrictlyLocal {α β : Type} (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

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

def Core.Computability.Subregular.Function.IsRightOutputStrictlyLocal {α β : Type} (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

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

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

Direction-parameterised OSL predicate.

Equations

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

@[simp]

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

@[simp]

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

theorem Core.Computability.Subregular.Function.OSLRule.isLeftOutputStrictlyLocal_apply {α β : Type} {k : ℕ} (r : OSLRule k α β) : IsLeftOutputStrictlyLocal k r.apply

Every OSL rule witnesses IsLeftOutputStrictlyLocal for the function it computes.

theorem Core.Computability.Subregular.Function.isRightOutputStrictlyLocal_iff_left_reverse {α β : Type} {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

Construction-with-cast co-located on the source side, mirroring the ISL treatment.

def Core.Computability.Subregular.Function.OSLRule.toSFST {α β : Type} {k : ℕ} (r : OSLRule k α β) : SFST (List β) α β

Construction: every Left-OSL rule induces an SFST whose state is the output window (length ≤ 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 toSFST_run_eq_apply.

Equations

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

theorem Core.Computability.Subregular.Function.OSLRule.toSFST_run_eq_apply {α β : Type} {k : ℕ} (r : OSLRule k α β) : r.toSFST.run = r.apply

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

theorem Core.Computability.Subregular.Function.isLeftOutputStrictlyLocal_left_subsequential {α β : Type} {k : ℕ} {f : List α → List β} (h : IsLeftOutputStrictlyLocal k f) : IsLeftSubsequential f

Left-OSL ⊆ Left-Subsequential: every Left-OSL function is computed by some SFST scanning left-to-right.