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. The projection is erasure, w.filter (T ·): off-tier symbols are deleted before the SL_k test, so the constraint applies to tier-adjacent factors while arbitrary off-tier material may intervene.

Main definitions

• TierStrictlyLocalGrammar k α: a decidable tier together with an SL_k grammar read on the projection.
• IsTierStrictlyLocal k L: L is generated by some TierStrictlyLocalGrammar k α.
• Language.PreprojectiveSuffixSubstitutionClosed L T k: suffix substitution across middles with one projection to the tier T.

Main results

• Language.IsStrictlyLocal.toIsTierStrictlyLocal: SL_k ⊆ TSL_k, via the universal tier.
• Language.IsTierStrictlyLocal.isStarFree: TSL_k ⊆ SF over a finite alphabet.
• Language.IsTierStrictlyLocal.isStrictlyLocal: a TSL_k language in which every symbol is visible is SL_k.
• Language.isTierStrictlyLocal_iff_exists_tier: Lambert's characterization, that for 2 ≤ k a language is TSL_k exactly when some tier's off-tier symbols are freely insertable and deletable and the language is closed under preprojective suffix substitution along it.

Implementation notes

Tier projection is List.filter itself rather than a named wrapper. With the tier a Prop predicate carrying [DecidablePred] (the Finset.filter convention), w.filter (T ·) elaborates to the filter by fun x ↦ decide (T x), which is literally a Bool tier in the sense of Language.IsTierBased, so the two presentations meet without a conversion lemma. A relabelling projection g : α → Option β is List.filterMap g, the letterwise homomorphism List.flatMap fun x ↦ (g x).toList, hence 1-ISL (isLeftInputStrictlyLocal_one_iff).

References

• [HRT11]
• [McNP71]
• [Jar19]
• [Lam23]

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

A tier-based strictly k-local grammar is a decidable tier, a subset of α, together with 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 : StrictlyLocalGrammar α

  The permitted factors of the SL grammar read on the projected string.

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

The language generated by a TSL grammar is the preimage, under erasure of the off-tier symbols, of the SL_k language of permitted.

Equations

• G.language = {w : List α | List.filter (fun (x : α) => decide (G.tier x)) w ∈ StrictlyLocalGrammar.language k G.permitted}

@[simp]

theorem Subregular.TierStrictlyLocalGrammar.mem_language {α : Type u_1} {k : ℕ} (G : TierStrictlyLocalGrammar k α) (w : List α) : w ∈ G.language ↔ ∀ f ∈ List.kFactors k (boundary k (List.filter (fun (x : α) => decide (G.tier x)) w)), f ∈ G.permitted

theorem Subregular.TierStrictlyLocalGrammar.mem_language_append_cons_of_not_tier {α : Type u_1} {k : ℕ} (G : TierStrictlyLocalGrammar k α) {a : α} (ha : ¬G.tier a) (u v : List α) : u ++ a :: v ∈ G.language ↔ u ++ v ∈ G.language

Symbols off the tier are invisible to the grammar.

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

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

Equations

• Language.IsTierStrictlyLocal k L = ∃ (G : Subregular.TierStrictlyLocalGrammar k α), G.language = L

theorem Subregular.TierStrictlyLocalGrammar.isTierStrictlyLocal_language {α : Type u_1} {k : ℕ} (G : TierStrictlyLocalGrammar k α) : Language.IsTierStrictlyLocal k G.language

The language of a TierStrictlyLocalGrammar is tier-based strictly local, the introduction rule for Language.IsTierStrictlyLocal.

Inclusions

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

SL_k ⊆ TSL_k. Over the universal tier projection is the identity, so the TSL grammar's language reduces to the underlying SL grammar's language.

theorem Language.IsTierStrictlyLocal.isStrictlyLocal {α : Type u_1} {k : ℕ} {L : Language α} (h : IsTierStrictlyLocal k L) (hvis : ∀ (a : α), ∃ (u : List α) (v : List α), ¬(u ++ a :: v ∈ L ↔ u ++ v ∈ L)) : L.IsStrictlyLocal k

A tier-based strictly local language in which every symbol is visible somewhere, deleting it from some string changing membership, is strictly local, since its tier is the whole alphabet.

Lambert's characterization

def Language.PreprojectiveSuffixSubstitutionClosed {α : Type u_1} (L : Language α) (T : α → Prop) [DecidablePred T] (k : ℕ) : Prop

L is closed under T-preprojective suffix substitution at width k when two members whose middles project to one tier string of at least k - 1 symbols admit the crossover of their suffixes.

Equations

• One or more equations did not get rendered due to their size.

theorem Language.IsTierStrictlyLocal.exists_tier {α : Type u_1} {k : ℕ} {L : Language α} (h : IsTierStrictlyLocal k L) : ∃ (T : α → Prop) (x : DecidablePred T), (∀ (u v : List α) (a : α), ¬T a → (u ++ a :: v ∈ L ↔ u ++ v ∈ L)) ∧ L.PreprojectiveSuffixSubstitutionClosed T k

A tier-based strictly local language has a tier whose off-tier symbols are freely insertable and deletable and along which it is closed under preprojective suffix substitution.

theorem Language.isTierStrictlyLocal_iff_exists_tier {α : Type u_1} {k : ℕ} {L : Language α} (hk : 2 ≤ k) : IsTierStrictlyLocal k L ↔ ∃ (T : α → Prop) (x : DecidablePred T), (∀ (u v : List α) (a : α), ¬T a → (u ++ a :: v ∈ L ↔ u ++ v ∈ L)) ∧ L.PreprojectiveSuffixSubstitutionClosed T k

Lambert's characterization of the tier-based strictly local languages. For 2 ≤ k, a language is tier-based strictly k-local exactly when some tier has freely insertable and deletable off-tier symbols and closes the language under preprojective suffix substitution.

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

Tier-based strictly local languages are star-free ([HRT11]). Over a finite alphabet, a TSL language is the preimage of an SL_k language under erasure of the off-tier symbols, and star-freeness survives that preimage (IsStarFree.preimage_filter), so TSL_k ⊆ SF.