Output strictly local functions

This file defines the output strictly local functions. A function f : List α → List β is k-output strictly local (k-OSL) when the block it emits for each input symbol depends only on that symbol and the last k - 1 symbols already emitted. Progressive spreading is the motivating case, since its trigger is adjacent in the output however far back it lies in the input. Chandlee, Eyraud and Heinz characterize the class by tails and show it incomparable with the input strictly local functions, and Burness and McMullin relativize the window to a tier of the output alphabet.

We compute OSL functions by rules, characterize them by residuals, and prove that the classes nest in k and are subsequential over a finite alphabet. Dissimilation after an input symbol is ISL and not OSL, progressive spreading is OSL and neither ISL nor right-OSL, and long-distance assimilation across transparent symbols is Mealy-computable and neither ISL nor OSL.

Main definitions

• OSLRule k α β: a rule emitting a block from a window of k - 1 output symbols
• OSLRule.apply: the function a rule computes
• OSLRule.applyOnTier: a rule run with its window over the tier projection of its output
• IsLeftOutputStrictlyLocal k f, IsRightOutputStrictlyLocal k f: some rule computes f, scanning left to right or right to left

Main results

• isLeftOutputStrictlyLocal_iff_factorsThrough_residual: characterization by residuals
• IsLeftOutputStrictlyLocal.weaken: k-OSL functions are k'-OSL for k ≤ k'
• isLeftOutputStrictlyLocal_one_iff: the 1-OSL functions are the letterwise homomorphisms
• IsLeftOutputStrictlyLocal.isLeftSubsequential: OSL functions are subsequential
• ISLRule.dissimilate_not_isLeftOutputStrictlyLocal, OSLRule.spread_not_isLeftInputStrictlyLocal: ISL and OSL are incomparable
• longDistanceAgree_not_isLeftInputStrictlyLocal, longDistanceAgree_not_isLeftOutputStrictlyLocal: a Mealy-computable function in neither

Implementation notes

Rules carry neither the initial nor the final output of Chandlee, Eyraud and Heinz's transducers, so the classes are the sequential ones with f [] = []; progressive spreading fails right-OSL here for want of a final output. 0-OSL and 1-OSL coincide, and k indexes apply alone.

TODO

• Final outputs, recovering Chandlee, Eyraud and Heinz's classes through Function.prefixFunction.
• The output tier-based class as a predicate, characterized by residuals.

References

• J. Chandlee, R. Eyraud and J. Heinz, Learning Strictly Local Subsequential Functions (2014)
• J. Chandlee, R. Eyraud and J. Heinz, Output Strictly Local Functions (2015)
• P. Burness and K. McMullin, Multi-Tiered Strictly Local Functions (2020)

structure Subregular.OSLRule (k : ℕ) (α : Type u_3) (β : Type u_4) : Type (max u_3 u_4)

A k-output strictly local rule emits, for each input symbol, a block computed from the last k - 1 symbols it has emitted and the input symbol itself.

• windowOutput : List β → α → List β

  The block emitted for the current input symbol after the given window of output.

def Subregular.OSLRule.applyAux {α : Type u_1} {β : Type u_2} {k : ℕ} (r : OSLRule k α β) (outputWindow : List β) (rest : List α) : List β

The rule applied from a given window, the window recursion windowRun that accumulates what the rule emits truncated to k - 1 symbols.

Equations

• r.applyAux = SubsequentialTransducer.windowRun (k - 1) r.windowOutput r.windowOutput

def Subregular.OSLRule.apply {α : Type u_1} {β : Type u_2} {k : ℕ} (r : OSLRule k α β) (input : List α) : List β

The string function computed by the rule, scanning left to right from the empty window.

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

theorem Subregular.OSLRule.apply_append_singleton {α : Type u_1} {β : Type u_2} {k : ℕ} (r : OSLRule k α β) (u : List α) (x : α) : r.apply (u ++ [x]) = r.apply u ++ r.windowOutput ((r.apply u).rtake (k - 1)) x

The window before each symbol is the last k - 1 symbols of the output so far.

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

f is k-left-output strictly local if some k-OSL rule computes it.

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

f is k-right-output strictly local if its reverse-conjugate is k-left-OSL, that is, if some k-OSL rule computes it scanning right to left.

Equations

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

theorem Subregular.OSLRule.isLeftOutputStrictlyLocal_apply {α : Type u_1} {β : Type u_2} {k : ℕ} (r : OSLRule k α β) : IsLeftOutputStrictlyLocal k r.apply

Residuals

theorem Subregular.IsLeftOutputStrictlyLocal.map_nil {α : Type u_1} {β : Type u_2} {k : ℕ} {f : List α → List β} (hf : IsLeftOutputStrictlyLocal k f) : f [] = []

theorem Subregular.IsLeftOutputStrictlyLocal.isPrefix {α : Type u_1} {β : Type u_2} {k : ℕ} {f : List α → List β} (hf : IsLeftOutputStrictlyLocal k f) (u v : List α) : f u <+: f (u ++ v)

theorem Subregular.IsLeftOutputStrictlyLocal.factorsThrough_residual {α : Type u_1} {β : Type u_2} {k : ℕ} {f : List α → List β} (hf : IsLeftOutputStrictlyLocal k f) : Function.FactorsThrough (Function.residual f) fun (u : List α) => (f u).rtake (k - 1)

The residuals of a k-OSL function factor through the last k - 1 output symbols, so inputs whose outputs end alike have the same continuations.

theorem Subregular.IsLeftOutputStrictlyLocal.of_factorsThrough_residual {α : Type u_1} {β : Type u_2} {k : ℕ} {f : List α → List β} (h₀ : f [] = []) (hpre : ∀ (u v : List α), f u <+: f (u ++ v)) (hf : Function.FactorsThrough (Function.residual f) fun (u : List α) => (f u).rtake (k - 1)) : IsLeftOutputStrictlyLocal k f

theorem Subregular.isLeftOutputStrictlyLocal_iff_factorsThrough_residual {α : Type u_1} {β : Type u_2} {k : ℕ} {f : List α → List β} : IsLeftOutputStrictlyLocal k f ↔ f [] = [] ∧ (∀ (u v : List α), f u <+: f (u ++ v)) ∧ Function.FactorsThrough (Function.residual f) fun (u : List α) => (f u).rtake (k - 1)

A function is k-OSL if and only if it fixes [], is prefix-preserving, and has residuals factoring through the last k - 1 output symbols.

The hierarchy in k

theorem Subregular.IsLeftOutputStrictlyLocal.weaken {α : Type u_1} {β : Type u_2} {k k' : ℕ} {f : List α → List β} (hf : IsLeftOutputStrictlyLocal k f) (hk : k ≤ k') : IsLeftOutputStrictlyLocal k' f

A k-OSL function is k'-OSL for every k' ≥ k.

theorem Subregular.IsRightOutputStrictlyLocal.weaken {α : Type u_1} {β : Type u_2} {k k' : ℕ} {f : List α → List β} (hf : IsRightOutputStrictlyLocal k f) (hk : k ≤ k') : IsRightOutputStrictlyLocal k' f

theorem Subregular.isLeftOutputStrictlyLocal_one_iff {α : Type u_1} {β : Type u_2} {f : List α → List β} : IsLeftOutputStrictlyLocal 1 f ↔ ∃ (h : α → List β), List.flatMap h = f

The 1-OSL functions are the letterwise homomorphisms List.flatMap h, which are also the 1-ISL functions.

OSL ⊆ Subsequential

An OSL rule is a window recursion accumulating its own output, so over a finite output alphabet the bounded output window is a finite state space (isLeftSubsequential_windowRun).

theorem Subregular.IsLeftOutputStrictlyLocal.isLeftSubsequential {α : Type u_1} {β : Type u_2} {k : ℕ} {f : List α → List β} [Fintype β] (hf : IsLeftOutputStrictlyLocal k f) : IsLeftSubsequential f

Over a finite output alphabet, left-OSL functions are left-subsequential.

theorem Subregular.OSLRule.isMealyComputable_apply {α : 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 rule emitting one symbol per input symbol is Mealy-computable, the bounded output window being the state.

theorem Subregular.IsRightOutputStrictlyLocal.isRightSubsequential {α : Type u_1} {β : Type u_2} {k : ℕ} {f : List α → List β} [Fintype β] (hf : IsRightOutputStrictlyLocal k f) : IsRightSubsequential f

Over a finite output alphabet, right-OSL functions are right-subsequential.

Output tiers

def Subregular.OSLRule.applyOnTier {α : Type u_1} {β : Type u_2} {k : ℕ} (r : OSLRule k α β) (p : β → Prop) [DecidablePred p] : List α → List β

The rule run with its window over the tier p of the output alphabet, so that each block depends on the last k - 1 on-tier symbols emitted ([BMcM20], Definition 8).

Equations

• r.applyOnTier p = SubsequentialTransducer.windowRun (k - 1) r.windowOutput (fun (w : List β) (x : α) => List.filter (fun (x : β) => decide (p x)) (r.windowOutput w x)) []

@[simp]

theorem Subregular.OSLRule.applyOnTier_nil {α : Type u_1} {β : Type u_2} {k : ℕ} (r : OSLRule k α β) (p : β → Prop) [DecidablePred p] : r.applyOnTier p [] = []

theorem Subregular.OSLRule.applyOnTier_append_singleton {α : Type u_1} {β : Type u_2} {k : ℕ} (r : OSLRule k α β) (p : β → Prop) [DecidablePred p] (u : List α) (x : α) : r.applyOnTier p (u ++ [x]) = r.applyOnTier p u ++ r.windowOutput ((List.filter (fun (x : β) => decide (p x)) (r.applyOnTier p u)).rtake (k - 1)) x

The window before each symbol is the last k - 1 on-tier symbols of the output so far.

theorem Subregular.OSLRule.applyOnTier_true {α : Type u_1} {β : Type u_2} {k : ℕ} (r : OSLRule k α β) : (r.applyOnTier fun (x : β) => True) = r.apply

Over the total tier, applyOnTier is apply.

theorem Subregular.OSLRule.filter_applyOnTier {α : Type u_1} {k : ℕ} (r : OSLRule k α α) {p : α → Prop} [DecidablePred p] (hr : ∀ (w : List α) (x y : α), y ∈ r.windowOutput w x → (p y ↔ p x)) (l : List α) : List.filter (fun (x : α) => decide (p x)) (r.applyOnTier p l) = r.apply (List.filter (fun (x : α) => decide (p x)) l)

Restricted to the tier, applyOnTier is apply on the tier projection of the input, provided each block stays on the tier exactly when its input symbol is on it.

theorem Subregular.OSLRule.isLeftSubsequential_applyOnTier {α : Type u_1} {β : Type u_2} {k : ℕ} (r : OSLRule k α β) (p : β → Prop) [DecidablePred p] [Fintype β] : IsLeftSubsequential (r.applyOnTier p)

Over a finite output alphabet the rule run over a tier is left-subsequential, the bounded tier window being the state.

ISL and OSL are incomparable

Chandlee, Eyraud and Heinz separate the two classes and place a subsequential function outside both. Over the residual characterizations each separation is one pair of inputs with the same window and different continuations.

def Subregular.ISLRule.dissimilate {α : Type u_1} [DecidableEq α] (a b : α) : ISLRule 2 α α

Dissimilation of a to b after an input a (the function f₂ of [CEH14], Theorem 5).

Equations

• Subregular.ISLRule.dissimilate a b = { windowOutput := fun (w : List α) (x : α) => if w = [a] ∧ x = a then [b] else [x] }

theorem Subregular.ISLRule.dissimilate_not_isLeftOutputStrictlyLocal {α : Type u_1} [DecidableEq α] {a b : α} (hab : a ≠ b) (k : ℕ) : ¬IsLeftOutputStrictlyLocal k (dissimilate a b).apply

Dissimilation is not OSL, since aa and ab have the same output ab but continue differently on a.

def Subregular.OSLRule.spread {α : Type u_1} [DecidableEq α] (a : α) : OSLRule 2 α α

Unbounded progressive spreading of a, under which every symbol after an a surfaces as a.

Equations

• Subregular.OSLRule.spread a = { windowOutput := fun (w : List α) (x : α) => if w = [a] then [a] else [x] }

theorem Subregular.OSLRule.spread_not_isLeftInputStrictlyLocal {α : Type u_1} [DecidableEq α] {a b : α} (hab : a ≠ b) (k : ℕ) : ¬IsLeftInputStrictlyLocal k (spread a).apply

Spreading is not ISL, since a bᵏ⁻¹ and bᵏ end in the same k - 1 input symbols while a further b surfaces as a after the first and as b after the second.

theorem Subregular.OSLRule.spread_not_isRightOutputStrictlyLocal {α : Type u_1} [DecidableEq α] {a b : α} (hab : a ≠ b) (k : ℕ) : ¬IsRightOutputStrictlyLocal k (spread a).apply

Spreading is not right-OSL, since scanned right to left its output on b is not a prefix of its output on ba.

def Subregular.longDistanceAgree {α : Type u_1} [DecidableEq α] (a b : α) : Mealy Bool α α

The flag machine for long-distance assimilation of b to a, under which b surfaces as a after an a however far back (the function f₁ of [CEH14], Theorem 4).

Equations

• Subregular.longDistanceAgree a b = Mealy.ofFlag (fun (x : α) => decide (x = a)) fun (s : Bool) (x : α) => if s = true ∧ x = b then a else x

theorem Subregular.longDistanceAgree_not_isLeftInputStrictlyLocal {α : Type u_1} [DecidableEq α] {a b c : α} (hab : a ≠ b) (hca : c ≠ a) (k : ℕ) : ¬IsLeftInputStrictlyLocal k (longDistanceAgree a b).run

Long-distance assimilation is not ISL, since acᵏ⁻¹ and bcᵏ⁻¹ end alike while a further b surfaces as a only after the first.

theorem Subregular.longDistanceAgree_not_isLeftOutputStrictlyLocal {α : Type u_1} [DecidableEq α] {a b c : α} (hab : a ≠ b) (hca : c ≠ a) (hcb : c ≠ b) (k : ℕ) : ¬IsLeftOutputStrictlyLocal k (longDistanceAgree a b).run

Long-distance assimilation is not OSL, since acᵏ⁻¹ and bcᵏ⁻¹ are output unchanged and end alike while a further b surfaces as a only after the first.