Input Strictly Local (ISL) Functions

A function f : List α → List β is k-Input Strictly Local when each output block depends only on the last k − 1 input symbols plus the current input symbol — a strict bound on input-window memory @cite{chandlee-2014} @cite{chandlee-heinz-2018}.

ISL is the most restrictive class of the function-level subregular hierarchy (@cite{aksenova-rawski-graf-heinz-2020} §2; @cite{meinhardt-mai-bakovic-mccollum-2024} Fig. 1). It captures local non-iterative phonological maps: Quechua postnasal voicing, English flapping, German final devoicing, etc. It is properly contained in the Output Strictly Local class (OSL.lean), which is in turn properly contained in the Subsequential class (Subsequential.lean); see Hierarchy.lean for the inclusion theorems.

ISL does not capture iterative spreading (which requires output context — OSL), unbounded long-distance assimilation (which requires tier projections), bidirectional harmony (Weakly Deterministic class), or tone (which is non-subsequential per @cite{jardine-2016}).

Architectural parallel

This file is the function-level analogue of StrictlyLocal.lean (which defines IsStrictlyLocal k L : Prop := ∃ G, G.lang = L for languages). We mirror the same witness-style: IsInputStrictlyLocal k f : Prop := ∃ r : ISLRule k α β, r.apply = f. The witness type ISLRule is the substantive content of the class — the bounded-window memory.

Main definitions

• ISLRule k α β — a k-ISL rule: a window-based output function (List α) → α → List β that consumes the (k − 1)-symbol left context plus the current symbol and emits an output block.
• ISLRule.apply r — the induced string function List α → List β.
• IsInputStrictlyLocal k f — predicate witness-style.

Reuse

Linglib/Core/StringHom.lean provides letterwise homomorphisms (StringHom α β := α → List β). These are the k = 1 specialisation of ISL — no left context. We do not yet provide the embedding StringHom α β ≃ ISLRule 1 α β; this is straightforward and lives in a follow-up Function/StringHom.lean bridge once a consumer needs it.

def Core.Computability.Subregular.Function.lastN {α : Type u_1} (n : ℕ) (xs : List α) : List α

The last n elements of a list. Defined as xs.drop (xs.length - n); when n ≥ xs.length, returns xs (since Nat subtraction truncates).

Equivalent to String.takeRight and Substring.takeRight in Lean core but no List.takeRight exists yet (batteries flags -- TODO: takeRight, dropRight in Batteries/Data/String/Lemmas.lean). Promote upstream once a List.takeRight lands.

Equations

• Core.Computability.Subregular.Function.lastN n xs = List.drop (xs.length - n) xs

@[simp]

theorem Core.Computability.Subregular.Function.lastN_nil {α : Type u_1} (n : ℕ) : lastN n [] = []

structure Core.Computability.Subregular.Function.ISLRule (k : ℕ) (α : Type u_3) (β : Type u_4) : Type (max u_3 u_4)

A k-Input-Strictly-Local rule over input alphabet α and output alphabet β. The single field windowOutput consumes the (k − 1)-symbol left context window plus the current input symbol and emits an output block (a list of output symbols, which can be empty for deletion or contain multiple symbols for insertion-on-trigger).

The k parameter is purely a type-level annotation — it constrains the intended semantics of windowOutput's first argument (the caller in apply always supplies a window of length at most k - 1) but is not enforced by the type. This mirrors SLGrammar k α from StrictlyLocal.lean, where the permitted factor set is similarly unconstrained at the type level.

• windowOutput : List α → α → List β

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

def Core.Computability.Subregular.Function.ISLRule.applyAux {α : Type u_1} {β : Type u_2} {k : ℕ} (r : ISLRule k α β) (window rest : List α) : List β

Apply the rule, threading a window of accumulated input symbols. Tail-recursive on the remaining input. The window grows from [] and is truncated to keep at most k − 1 symbols at each step.

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✝ ++ [x_2])) xs

def Core.Computability.Subregular.Function.ISLRule.apply {α : Type u_1} {β : Type u_2} {k : ℕ} (r : ISLRule k α β) (input : List α) : List β

Apply a k-ISL rule to an input string. Scans left-to-right; at each position emits r.windowOutput window x where window is the (last k − 1) preceding input symbols and x is the current symbol.

Equations

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

@[simp]

theorem Core.Computability.Subregular.Function.ISLRule.applyAux_nil {α : Type u_1} {β : Type u_2} {k : ℕ} (r : ISLRule k α β) (window : List α) : r.applyAux window [] = []

@[simp]

theorem Core.Computability.Subregular.Function.ISLRule.applyAux_cons {α : Type u_1} {β : Type u_2} {k : ℕ} (r : ISLRule k α β) (window : List α) (x : α) (xs : List α) : r.applyAux window (x :: xs) = r.windowOutput window x ++ r.applyAux (lastN (k - 1) (window ++ [x])) xs

@[simp]

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

@[simp]

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

def Core.Computability.Subregular.Function.IsLeftInputStrictlyLocal {α : Type u_1} {β : Type u_2} (k : ℕ) (f : List α → List β) : Prop

A function f : List α → List β is k-Left-Input-Strictly-Local iff some k-ISL rule computes it via left-to-right scan (the canonical ISL direction in @cite{chandlee-heinz-2018}). Witness-style, mirroring IsStrictlyLocal k L := ∃ G, G.lang = L from StrictlyLocal.lean.

Equations

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

def Core.Computability.Subregular.Function.IsRightInputStrictlyLocal {α : Type u_1} {β : Type u_2} (k : ℕ) (f : List α → List β) : Prop

A function f : List α → List β is k-Right-Input-Strictly-Local iff some k-ISL rule computes it via right-to-left scan. Mirror image of the left class via the involution f ↦ List.reverse ∘ f ∘ List.reverse (see isRightInputStrictlyLocal_iff_left_reverse).

Equations

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

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

Direction-parameterised ISL predicate. Mirrors the OSL/Subseq umbrella style; concrete claims should typically use one of IsLeftInputStrictlyLocal / IsRightInputStrictlyLocal directly for clarity.

Equations

• Core.Computability.Subregular.Function.IsInputStrictlyLocal Core.Direction.left k f = Core.Computability.Subregular.Function.IsLeftInputStrictlyLocal k f
• Core.Computability.Subregular.Function.IsInputStrictlyLocal Core.Direction.right k f = Core.Computability.Subregular.Function.IsRightInputStrictlyLocal k f

@[simp]

theorem Core.Computability.Subregular.Function.isInputStrictlyLocal_left {α : Type u_1} {β : Type u_2} (k : ℕ) (f : List α → List β) : IsInputStrictlyLocal Direction.left k f ↔ IsLeftInputStrictlyLocal k f

@[simp]

theorem Core.Computability.Subregular.Function.isInputStrictlyLocal_right {α : Type u_1} {β : Type u_2} (k : ℕ) (f : List α → List β) : IsInputStrictlyLocal Direction.right k f ↔ IsRightInputStrictlyLocal k f

theorem Core.Computability.Subregular.Function.ISLRule.isLeftInputStrictlyLocal_apply {α : Type u_1} {β : Type u_2} {k : ℕ} (r : ISLRule k α β) : IsLeftInputStrictlyLocal k r.apply

Every ISL rule witnesses IsLeftInputStrictlyLocal for the function it computes.

theorem Core.Computability.Subregular.Function.isRightInputStrictlyLocal_iff_left_reverse {α : Type u_1} {β : Type u_2} {k : ℕ} (f : List α → List β) : IsRightInputStrictlyLocal k f ↔ IsLeftInputStrictlyLocal k fun (xs : List α) => (f xs.reverse).reverse

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

theorem Core.Computability.Subregular.Function.isLeftInputStrictlyLocal_const_nil {α : Type u_1} {β : Type u_2} (k : ℕ) : IsLeftInputStrictlyLocal k fun (x : List α) => []

The empty-output function is ISL for any k. Witness: the rule that emits [] regardless of window or current symbol.

def Core.Computability.Subregular.Function.StringHomBridge.toISLRule {α : Type u_1} {β : Type u_2} (h : StringHom α β) : ISLRule 1 α β

Embed a string homomorphism as a 1-ISL rule (no left context). The windowOutput ignores its window argument and behaves letterwise.

Equations

• Core.Computability.Subregular.Function.StringHomBridge.toISLRule h = { windowOutput := fun (x : List α) (x_1 : α) => h x_1 }

@[simp]

theorem Core.Computability.Subregular.Function.StringHomBridge.toISLRule_apply {α : Type u_1} {β : Type u_2} (h : StringHom α β) : (toISLRule h).apply = h.apply

The 1-ISL rule constructed from h computes h on lists. Definitional up to applyAux unfolding; the inductive proof handles the window-threading.

theorem Core.Computability.Subregular.Function.Core.StringHom.apply_isLeftInputStrictlyLocal_one {α : Type u_1} {β : Type u_2} (h : StringHom α β) : IsLeftInputStrictlyLocal 1 h.apply

Every string homomorphism is 1-Left-ISL. The substrate-level claim that StringHom α β and ISLRule 1 α β denote the same function class.

theorem Core.Computability.Subregular.Function.Core.Tier.apply_isLeftInputStrictlyLocal_one {α : Type u_1} {β : Type u_2} (T : Tier α β) : IsLeftInputStrictlyLocal 1 T.apply

Every tier projection is 1-Left-ISL. Tier projections (per Core/StringHom.lean's Tier α β := α → Option β) are letterwise erasing, hence a special case of the StringHom bridge.

ISL → Subsequential

Construction-with-cast co-located on the source side: ISLRule.toSFST is the SFST view of an ISL rule, and the inclusion proof rides on it. This diverges from the language-side convention "cast lives with the larger class" because the dependency direction (SFST primitive in Subsequential.lean; ISL projects into it) forces the construction's home file to also house the cast. Mathlib precedent for X.toY living with the source X: MulHom.toAddHom, Subgroup.toSubmonoid.

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

Construction: every ISL rule induces an SFST whose state is the input window (length ≤ k − 1) and whose finalOutput is empty.

Equations

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

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

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

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

Left-ISL ⊆ Left-Subsequential: every Left-ISL function is computed by some SFST scanning left-to-right (@cite{chandlee-heinz-2018} §4).

theorem Core.Computability.Subregular.Function.isInputStrictlyLocal_isSubsequential {α β : Type} {d : Direction} {k : ℕ} {f : List α → List β} (h : IsInputStrictlyLocal d k f) : IsSubsequential d f

Direction-parameterised: ISL_d ⊆ Subseq_d for both directions.