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

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

Equations

• Subregular.IsRightInputStrictlyLocal k f = Subregular.IsLeftInputStrictlyLocal k (List.revConj f)

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

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

Equations

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

@[simp]

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

@[simp]

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

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.toFinSubsequentialTransducer projects an ISL rule into the sliding-window transducer SubsequentialTransducer.ofWindow, with the bounded input window {l : List α // l.length ≤ k - 1} as state. Co-located on the source side because the dependency direction (the transducer lives in Subsequential.lean; ISL projects into it) forces both construction and cast into this file.

def Subregular.ISLRule.toFinSubsequentialTransducer {α : Type u_1} {β : Type u_2} {k : ℕ} (r : ISLRule k α β) : SubsequentialTransducer { l : List α // l.length ≤ k - 1 } α β

Every ISL rule induces a window transducer tracking the last k - 1 input symbols, with empty finalOutput. Finite-state over a finite alphabet (List.fintypeSubtypeLengthLE), witnessing ISL ⊆ Subsequential under the source literature's finite-state assumption [Moh97].

Equations

• r.toFinSubsequentialTransducer = SubsequentialTransducer.ofWindow (k - 1) r.windowOutput fun (x : List α) (x_1 : α) => [x_1]

theorem Subregular.ISLRule.applyAux_eq_windowRun {α : Type u_1} {β : Type u_2} {k : ℕ} (r : ISLRule k α β) : r.applyAux = SubsequentialTransducer.windowRun (k - 1) r.windowOutput fun (x : List α) (x_1 : α) => [x_1]

ISLRule.applyAux is the canonical window recursion accumulating the input.

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

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

A single-symbol left-ISL rule is Mealy-computable. The bounded input window that makes ISLRule.toFinSubsequentialTransducer finite-state is already the synchronous state.

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

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

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