Input strictly local functions

This file defines the input strictly local functions. A function f : List α → List β is k-input strictly local (k-ISL) when the block it emits for each input symbol depends only on that symbol and the k - 1 input symbols before it. Chandlee introduced the class for the local phonological processes that apply simultaneously, such as substitution, epenthesis, deletion and metathesis, and Chandlee, Eyraud and Heinz characterize it by tails. We compute ISL functions by rules, show that a function is k-ISL exactly when its residuals factor through the last k - 1 input symbols, and prove that the classes nest in k, begin at k = 1 with the letterwise homomorphisms, and are subsequential over a finite alphabet.

Main definitions

• ISLRule k α β: a rule emitting a block from a window of k - 1 input symbols
• ISLRule.apply: the function a rule computes
• IsLeftInputStrictlyLocal k f, IsRightInputStrictlyLocal k f: some rule computes f, scanning left to right or right to left

Main results

• isLeftInputStrictlyLocal_iff_factorsThrough_residual: characterization by residuals
• IsLeftInputStrictlyLocal.weaken: k-ISL functions are k'-ISL for k ≤ k'
• isLeftInputStrictlyLocal_one_iff: the 1-ISL functions are the letterwise homomorphisms
• IsLeftInputStrictlyLocal.isLeftSubsequential: ISL functions are subsequential

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 [] = []; final devoicing, left-ISL there through a final output, is right-ISL here. 0-ISL and 1-ISL coincide, and k indexes apply alone.

References

• J. Chandlee, Strictly Local Phonological Processes (2014)
• J. Chandlee, R. Eyraud and J. Heinz, Learning Strictly Local Subsequential Functions (2014)
• J. Chandlee and J. Heinz, Strict Locality and Phonological Maps (2018)

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

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

• windowOutput : List α → α → List β

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

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

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

Equations

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

def Subregular.ISLRule.apply {α : Type u_1} {β : Type u_2} {k : ℕ} (r : ISLRule 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.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

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

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

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

f is k-left-input strictly local if some k-ISL rule computes it.

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 is k-right-input strictly local if its reverse-conjugate is k-left-ISL, that is, if some k-ISL rule computes it scanning right to left.

Equations

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

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

Residuals

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

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

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

The residuals of a k-ISL function factor through the last k - 1 input symbols, so inputs ending alike have the same continuations.

theorem Subregular.IsLeftInputStrictlyLocal.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 α) => u.rtake (k - 1)) : IsLeftInputStrictlyLocal k f

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

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

The hierarchy in k

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

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

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

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

The 1-ISL functions are the letterwise homomorphisms List.flatMap h, among them the erasing projections List.filterMap g.

ISL ⊆ Subsequential

An ISL rule is a window recursion accumulating the input, so over a finite input alphabet the bounded input window is a finite state space (isLeftSubsequential_windowRun).

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

Over a finite input alphabet, left-ISL functions are left-subsequential.

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

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

Over a finite input alphabet, right-ISL functions are right-subsequential.