Strictly local languages (SL_k)

A language L is strictly k-local when membership is determined by the length-k substrings of the boundary-augmented input: a grammar is a set G of permitted k-factors, and w ∈ L iff every k-factor of boundary k w lies in G. The forbidden-factor dual (G = Fᶜ) is finite even over an infinite alphabet.

Main definitions

• SLGrammar α: a grammar is just a set of permitted factors over Augmented α; the locality width k is supplied to language, not baked in.
• SLGrammar.language k: the Language α it generates at width k.
• SLGrammar.ofForbidden: the grammar of a forbidden-factor set (its complement).
• Language.IsStrictlyLocal L k: L is strictly k-local.
• Language.SuffixSubstitutionClosed L k: members sharing a length-(k − 1) window admit suffix crossover.

Main results

• Language.isStrictlyLocal_iff_suffixSubstitutionClosed: for k ≥ 2, strict k-locality is exactly closure under suffix substitution: the crossover's factors split into the two members' shared parts, and conversely the canonical grammar of licensed factors regenerates the language by stitching a member window-by-window.

@[reducible, inline]

abbrev SLGrammar (α : Type u_2) : Type u_2

A strictly-local grammar over α: a set of permitted factors over the boundary-augmented alphabet Option α (none the boundary). The locality width k is supplied to language, not baked into the carrier.

Equations

• SLGrammar α = Set (Augmented α)

def SLGrammar.language {α : Type u_1} (k : ℕ) (G : SLGrammar α) : Language α

The language generated at width k: strings whose boundary-augmented form has every k-factor permitted.

Equations

• SLGrammar.language k G = {w : List α | ∀ f ∈ List.kFactors k (boundary k w), f ∈ G}

@[simp]

theorem SLGrammar.mem_language {α : Type u_1} (k : ℕ) (G : SLGrammar α) (w : List α) : w ∈ language k G ↔ ∀ f ∈ List.kFactors k (boundary k w), f ∈ G

def SLGrammar.ofForbidden {α : Type u_1} (forbidden : Set (Augmented α)) : SLGrammar α

The grammar of a forbidden-factor set is its complement: a string is accepted iff none of its k-factors are forbidden.

Equations

• SLGrammar.ofForbidden forbidden = forbiddenᶜ

@[simp]

theorem SLGrammar.mem_ofForbidden_language {α : Type u_1} (forbidden : Set (Augmented α)) (k : ℕ) (w : List α) : w ∈ language k (ofForbidden forbidden) ↔ ∀ f ∈ List.kFactors k (boundary k w), f ∉ forbidden

theorem SLGrammar.mem_language_iff_window {α : Type u_1} {k : ℕ} {G : SLGrammar α} {w : List α} (hk : 1 ≤ k) : w ∈ language k G ↔ ∀ (i : ℤ), 1 - ↑k ≤ i → i < ↑w.length → List.window k w i ∈ G

Membership in an SL language, position-indexed: every window over [1 - k, w.length) is permitted.

Count-vector characterisation

Membership in a forbidden-factor SL language is a zero-test of a single linear functional of the word's k-factor count vector — the total count of forbidden factors — with unit margin on nonmembers. Strict locality is thus linearly detectable on the factor-count (cue) representation.

theorem SLGrammar.mem_ofForbidden_language_iff_sum_count_eq_zero {α : Type u_1} [DecidableEq α] (F : Finset (Augmented α)) (k : ℕ) (w : List α) : w ∈ language k (ofForbidden ↑F) ↔ ∑ f ∈ F, List.count f (List.kFactors k (boundary k w)) = 0

SL membership is the vanishing of the forbidden-factor count.

theorem SLGrammar.one_le_sum_count_of_not_mem_ofForbidden_language {α : Type u_1} [DecidableEq α] {F : Finset (Augmented α)} {k : ℕ} {w : List α} (h : w ∉ language k (ofForbidden ↑F)) : 1 ≤ ∑ f ∈ F, List.count f (List.kFactors k (boundary k w))

Nonmembers score at least 1 on the forbidden-factor count: the linear detector has unit margin.

def Language.IsStrictlyLocal {α : Type u_2} (L : Language α) (k : ℕ) : Prop

A language L is strictly k-local iff some SLGrammar α generates it at width k. Witness-style, mirroring Language.IsRegular/Language.IsContextFree ("L is regular iff some DFA accepts L").

Equations

• L.IsStrictlyLocal k = ∃ (G : SLGrammar α), SLGrammar.language k G = L

Suffix substitution closure

def Language.SuffixSubstitutionClosed {α : Type u_2} (L : Language α) (k : ℕ) : Prop

L is closed under suffix substitution at width k: two members sharing a length-(k − 1) window admit the crossover of their suffixes at it.

Equations

• L.SuffixSubstitutionClosed k = ∀ (u₁ v₁ u₂ v₂ x : List α), x.length = k - 1 → u₁ ++ x ++ v₁ ∈ L → u₂ ++ x ++ v₂ ∈ L → u₁ ++ x ++ v₂ ∈ L

theorem Language.IsStrictlyLocal.suffixSubstitutionClosed {α : Type u_2} {L : Language α} {k : ℕ} (h : L.IsStrictlyLocal k) : L.SuffixSubstitutionClosed k

A strictly local language is closed under suffix substitution: every k-factor of the crossover lies in the shared left part — a factor of the first member — or in the shared window-and-right part — a factor of the second.

theorem Language.SuffixSubstitutionClosed.isStrictlyLocal {α : Type u_2} {L : Language α} {k : ℕ} (hk : 2 ≤ k) (h : L.SuffixSubstitutionClosed k) : L.IsStrictlyLocal k

A suffix-substitution-closed language is strictly local: the canonical grammar of all licensed member-factors regenerates it, stitching a member left-to-right through the shared windows.

theorem Language.isStrictlyLocal_iff_suffixSubstitutionClosed {α : Type u_2} {L : Language α} {k : ℕ} (hk : 2 ≤ k) : L.IsStrictlyLocal k ↔ L.SuffixSubstitutionClosed k

The suffix-substitution characterization of strict locality: for widths k ≥ 2, a language is strictly k-local if and only if it is closed under suffix substitution at k.