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. ISL is the most restrictive class of the function-level subregular hierarchy.

Main definitions

• ISLRule k α β — a k-ISL rule: a window-based output function List α → α → List β consuming the k - 1-symbol left context plus the current input symbol and emitting an output block.
• ISLRule.apply — the induced string function List α → List β.
• IsLeftInputStrictlyLocal k f, IsRightInputStrictlyLocal k f — witness predicates: there exists an ISLRule k α β whose apply computes f (resp. via right-to-left scan).
• IsInputStrictlyLocal d k f — direction-parameterised umbrella.

Main results

• isRightInputStrictlyLocal_iff_left_reverse — the right class is the reverse-conjugate of the left class.
• isLeftInputStrictlyLocal_left_subsequential — every Left-ISL function is Left-Subsequential, witnessed by ISLRule.toSFST.
• flatMap_isLeftInputStrictlyLocal_one, filterMap_isLeftInputStrictlyLocal_one — letterwise homomorphisms and erasing (tier) projections are the k = 1 specialisation.

Implementation notes

The witness style IsX k f := ∃ r : XRule k α β, r.apply = f mirrors Language.IsStrictlyLocal L k := ∃ G, G.language k = L from StrictlyLocal.lean. The k parameter is a type-level annotation only: windowOutput is unconstrained at the type level; applyAux truncates the threaded window to length k - 1.

@[implicit_reducible]

noncomputable instance Subregular.fintypeListLengthLE {α : Type u_3} [Fintype α] (n : ℕ) : Fintype { l : List α // l.length ≤ n }

The "list of length at most n" subtype is finite when α is. The witness is a surjection from Σ m : Fin (n + 1), List.Vector α m (which has a Fintype instance via Mathlib.Data.Fintype.{Sigma,Vector}). Used to give ISL/OSL projections into SFST a manifestly-finite state space (matching [Moh97]'s finite-state assumption). Uses classical to discharge the DecidableEq side condition without imposing it on consumers (matches mathlib pattern for finite types over Fintype α).

Equations

• Subregular.fintypeListLengthLE n = Fintype.ofSurjective (fun (s : (m : Fin (n + 1)) × List.Vector α ↑m) => ⟨s.snd.toList, ⋯⟩) ⋯

structure Subregular.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 Subregular.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 ((x✝ ++ [x_2]).rtake (k - 1)) xs

def Subregular.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 Subregular.ISLRule.applyAux_nil {α : Type u_1} {β : Type u_2} {k : ℕ} (r : ISLRule k α β) (window : List α) : r.applyAux window [] = []

@[simp]

theorem Subregular.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 ((window ++ [x]).rtake (k - 1)) xs

@[simp]

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

@[simp]

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

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

f : List α → List β is k-Left-Input-Strictly-Local iff some k-ISL rule computes it via left-to-right scan.

Equations

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

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

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 f ↦ List.reverse ∘ f ∘ List.reverse; see isRightInputStrictlyLocal_iff_left_reverse.

Equations

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

def Subregular.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

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

@[simp]

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

@[simp]

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

theorem Subregular.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 Subregular.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 Subregular.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.

Letterwise homomorphisms / Tier as the k = 1 specialisation

A letterwise string homomorphism h : α → List β (string action List.flatMap h, the free-monoid lift) is the k = 1 specialisation: the window argument is always empty and only the current input symbol matters. An erasing letterwise map g : α → Option β (string action List.filterMap g) is the further erasing specialisation.

def Subregular.ISLRule.ofStringHom {α : Type u_1} {β : Type u_2} (h : α → List β) : ISLRule 1 α β

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

Equations

• Subregular.ISLRule.ofStringHom h = { windowOutput := fun (x : List α) (x_1 : α) => h x_1 }

@[simp]

theorem Subregular.ISLRule.ofStringHom_apply {α : Type u_1} {β : Type u_2} (h : α → List β) : (ofStringHom h).apply = List.flatMap h

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

theorem Subregular.flatMap_isLeftInputStrictlyLocal_one {α : Type u_1} {β : Type u_2} (h : α → List β) : IsLeftInputStrictlyLocal 1 (List.flatMap h)

Every letterwise string homomorphism is 1-Left-ISL. The substrate-level claim that the letterwise-homomorphism function class (List.flatMap h for h : α → List β) and ISLRule 1 α β denote the same function class.

theorem Subregular.filterMap_isLeftInputStrictlyLocal_one {α : Type u_1} {β : Type u_2} (g : α → Option β) : IsLeftInputStrictlyLocal 1 (List.filterMap g)

Every erasing letterwise projection is 1-Left-ISL. List.filterMap g (for g : α → Option β) is letterwise erasing, hence a special case of ISLRule.ofStringHom via fun x => (g x).toList.

ISL ⊆ Subsequential

ISLRule.toFinSFST projects an ISL rule into a finite-state SFST whose state space is the bounded input window {l : List α // l.length ≤ k - 1}. The [Fintype α] constraint matches the source literature [Moh97]: every subsequential model has a finite alphabet and finite state by definition. The inclusion theorem rides on the run-equality. Co-located on the source side because the dependency direction (SFST in Subsequential.lean; ISL projects into it) forces both construction and cast into this file.

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

Construction: every ISL rule induces a finite-state SFST whose state is the bounded input window {l : List α // l.length ≤ k - 1}, and whose finalOutput is empty. The state is manifestly finite via fintypeListLengthLE, witnessing ISL ⊆ Subsequential under the source literature's finite-state assumption.

Equations

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

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

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

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

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

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

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

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

Direction-parameterised: ISL_d ⊆ Subseq_d for both directions (over a finite input alphabet). Delegates to the Left- / Right- specialised theorems.