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

• Subregular.SLGrammar α — a grammar is just a set of permitted factors over Augmented α; the locality width k is supplied to language, not baked in.
• Subregular.SLGrammar.language k — the Language α it generates at width k.
• Subregular.SLGrammar.ofForbidden — the grammar of a forbidden-factor set (its complement).
• Language.IsStrictlyLocal L k — L is strictly k-local.

@[reducible, inline]

abbrev Subregular.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

• Subregular.SLGrammar α = Set (Subregular.Augmented α)

def Subregular.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

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

@[simp]

theorem Subregular.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 Subregular.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

• Subregular.SLGrammar.ofForbidden forbidden = forbiddenᶜ

@[simp]

theorem Subregular.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

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 Subregular.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 Subregular.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_1} (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 : Subregular.SLGrammar α), Subregular.SLGrammar.language k G = L