Tier-based strictly local languages (TSL_k)

A language is tier-based strictly k-local when its membership is determined by SL_k membership of its projection onto a tier — a decidable subalphabet T. Off-tier symbols are erased before the SL_k test, so the constraint applies to tier-adjacent factors while arbitrary off-tier material may intervene.

Main definitions

• tierProject T — keep the symbols satisfying T, erase the rest. The byClass specialization of the keystone TierProjection.apply (Core/Computability/TierProjection.lean).
• TSLGrammar k α — a decidable tier together with an SL_k grammar read on the projection.
• IsTierStrictlyLocal k L — L is generated by some TSLGrammar k α.

Main results

• Language.IsStrictlyLocal.toIsTierStrictlyLocal — SL_k ⊆ TSL_k, via the universal tier (projection is the identity).

def Subregular.tierProject {α : Type u_1} (T : α → Prop) [DecidablePred T] (xs : List α) : List α

Tier projection: keep the symbols satisfying the tier predicate T, erase the rest. The single-alphabet byClass specialization of the keystone erasing string homomorphism TierProjection.apply (Core/Computability/TierProjection.lean), so the autosegmental and subregular tiers are one definition rather than two joined by a bridge.

Equations

• Subregular.tierProject T xs = (TierProjection.byClass T).apply xs

theorem Subregular.tierProject_eq_filter {α : Type u_1} (T : α → Prop) [DecidablePred T] (xs : List α) : tierProject T xs = List.filter (fun (x : α) => decide (T x)) xs

tierProject reduces to List.filter (via TierProjection.apply_byClass).

@[simp]

theorem Subregular.tierProject_nil {α : Type u_1} (T : α → Prop) [DecidablePred T] : tierProject T [] = []

theorem Subregular.tierProject_cons {α : Type u_1} (T : α → Prop) [DecidablePred T] (x : α) (xs : List α) : tierProject T (x :: xs) = if T x then x :: tierProject T xs else tierProject T xs

@[simp]

theorem Subregular.tierProject_univ {α : Type u_1} (w : List α) : tierProject (fun (x : α) => True) w = w

Projection by the universal tier is the identity.

structure Subregular.TSLGrammar (k : ℕ) (α : Type u_2) : Type u_2

A tier-based strictly k-local grammar: a decidable tier (subset of α) plus an SL grammar interpreted on the projected string. The tier predicate is carried as an instance field via [DecidablePred tier] so projection at use sites picks up the decidability automatically.

• tier : α → Prop

  The membership predicate selecting which symbols stay on the tier. Symbols failing tier are erased before the SL test.

• decTier : DecidablePred self.tier

  Decidability of tier, needed to define projection.

• permitted : SLGrammar α

  The SL grammar read on the projected string: its permitted factors.

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

The language generated by a TSL grammar: the preimage, under tier projection, of the SL_k language of permitted.

Equations

• G.lang = Subregular.tierProject G.tier ⁻¹' Subregular.SLGrammar.language k G.permitted

@[simp]

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

def Language.IsTierStrictlyLocal {α : Type u_1} (k : ℕ) (L : Language α) : Prop

A language is tier-based strictly k-local iff some TSLGrammar k α generates it.

Equations

• Language.IsTierStrictlyLocal k L = ∃ (G : Subregular.TSLGrammar k α), G.lang = L

Inclusions

theorem Language.IsStrictlyLocal.toIsTierStrictlyLocal {α : Type u_1} {k : ℕ} {L : Language α} (h : L.IsStrictlyLocal k) : IsTierStrictlyLocal k L

SL_k ⊆ TSL_k: take the universal tier (every symbol on tier), so projection is the identity and the TSL grammar's lang reduces to the underlying SL grammar's lang.