Strictly Local Languages (SL_k)

A language L is strictly k-local when membership in L is determined by which length-k substrings the boundary-augmented form of the input contains @cite{rogers-pullum-2011} @cite{lambert-2022}. The two equivalent presentations are:

• Positive: a set G of permitted k-factors. w ∈ L iff every k-factor of boundary k w is in G.
• Negative: a set F of forbidden k-factors. w ∈ L iff no k-factor of boundary k w is in F.

The negative form is what most phonological accounts use (forbidden bigrams, forbidden trigrams), since it is finite even when the alphabet is infinite.

Main definitions

• SLGrammar k α — a positive k-grammar over alphabet α.
• SLGrammar.lang — the Language α (mathlib type) it generates.
• SLGrammar.ofForbidden — convert a forbidden-factor set to the equivalent positive grammar.
• IsStrictlyLocal k L — the property that a Language α is strictly k-local for a given k.

structure Core.Computability.Subregular.SLGrammar (k : ℕ) (α : Type u_2) : Type u_2

A strictly k-local grammar over α: a set of permitted length-k factors over the boundary-augmented alphabet Option α (with none as the boundary).

• permitted : Set (Augmented α)

  The set of permitted k-factors. Factors not listed here are forbidden in any string of the language.

theorem Core.Computability.Subregular.SLGrammar.ext_iff {k : ℕ} {α : Type u_2} {x y : SLGrammar k α} : x = y ↔ x.permitted = y.permitted

theorem Core.Computability.Subregular.SLGrammar.ext {k : ℕ} {α : Type u_2} {x y : SLGrammar k α} (permitted : x.permitted = y.permitted) : x = y

@[implicit_reducible]

instance Core.Computability.Subregular.SLGrammar.instInhabited {α : Type u_1} {k : ℕ} : Inhabited (SLGrammar k α)

Equations

• Core.Computability.Subregular.SLGrammar.instInhabited = { default := { permitted := Set.univ } }

def Core.Computability.Subregular.SLGrammar.lang {α : Type u_1} {k : ℕ} (G : SLGrammar k α) : Language α

The language generated by an SL grammar: strings whose boundary-augmented form has every k-factor in permitted.

Equations

• G.lang w = ∀ f ∈ Core.Computability.Subregular.kFactors k (Core.Computability.Subregular.boundary k w), f ∈ G.permitted

@[simp]

theorem Core.Computability.Subregular.SLGrammar.mem_lang {α : Type u_1} {k : ℕ} (G : SLGrammar k α) (w : List α) : w ∈ G.lang ↔ ∀ f ∈ kFactors k (boundary k w), f ∈ G.permitted

def Core.Computability.Subregular.SLGrammar.ofForbidden {α : Type u_1} {k : ℕ} (forbidden : Set (Augmented α)) : SLGrammar k α

An SL grammar from a forbidden-factor set. The permitted set is the complement; equivalently, a string is accepted iff none of its k-factors are in forbidden.

Equations

• Core.Computability.Subregular.SLGrammar.ofForbidden forbidden = { permitted := forbiddenᶜ }

@[simp]

theorem Core.Computability.Subregular.SLGrammar.mem_ofForbidden_lang {α : Type u_1} {k : ℕ} (forbidden : Set (Augmented α)) (w : List α) : w ∈ (ofForbidden forbidden).lang ↔ ∀ f ∈ kFactors k (boundary k w), f ∉ forbidden

def Core.Computability.Subregular.IsStrictlyLocal {α : Type u_1} (k : ℕ) (L : Language α) : Prop

A language L is strictly k-local iff some SLGrammar k α generates exactly L. This is the witness-style definition (cf. "L is regular iff some DFA accepts L" in Mathlib.Computability.DFA).

Equations

• Core.Computability.Subregular.IsStrictlyLocal k L = ∃ (G : Core.Computability.Subregular.SLGrammar k α), G.lang = L

theorem Core.Computability.Subregular.SLGrammar.isStrictlyLocal_lang {α : Type u_1} {k : ℕ} (G : SLGrammar k α) : IsStrictlyLocal k G.lang

Every SL grammar witnesses IsStrictlyLocal for its language.