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

• StrictlyLocalGrammar α: a grammar is just a set of permitted factors over Augmented α; the locality width k is supplied to language, not baked in.
• StrictlyLocalGrammar.language k: the Language α it generates at width k.
• StrictlyLocalGrammar.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.

• Language.IsStrictlyLocal.toIsLocallyTestable: SL_k ⊆ LT_k.

• Language.IsStrictlyLocal.isStarFree: SL_k ⊆ SF over a finite alphabet.

References

• [RP11]
• [McNP71]

@[reducible, inline]

abbrev StrictlyLocalGrammar (α : Type u_2) : Type u_2

A strictly-local grammar over α is a set of permitted factors over the boundary-augmented alphabet Option α, with none the boundary. The locality width k is an argument of language.

Equations

• StrictlyLocalGrammar α = Set (Augmented α)

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

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

Equations

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

@[simp]

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

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

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

Equations

• StrictlyLocalGrammar.ofForbidden forbidden = forbiddenᶜ

@[simp]

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

A string is in an SL language iff 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 StrictlyLocalGrammar.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 StrictlyLocalGrammar.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 StrictlyLocalGrammar α 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 : StrictlyLocalGrammar α), StrictlyLocalGrammar.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 when 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, since 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

For widths k ≥ 2, a language is strictly k-local if and only if it is closed under suffix substitution at k.

Local testability

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

A strictly k-local language is locally k-testable. Padding a word with boundary markers pulls it back from the words over the augmented alphabet whose factors of length k are all permitted, and that language is locally k-testable outright.

theorem Language.IsStrictlyLocal.isStarFree {α : Type u_2} [Finite α] {L : Language α} {k : ℕ} (h : L.IsStrictlyLocal k) : L.IsStarFree

Over a finite alphabet strictly local languages are star-free.