Tier-Based Strictly Local Languages (TSL_k)

A tier-based strictly k-local (TSL_k) language is one whose membership is determined by SL_k membership of its projection onto a tier — a designated decidable subset of the alphabet @cite{heinz-rawal-tanner-2011} @cite{lambert-2022}. Symbols outside the tier are erased before the SL test; this captures long-distance phonological dependencies (consonant harmony, vowel harmony with transparent vowels) where tier-adjacent substrings are constrained but the surface realisation may carry arbitrary intervening material on other tiers.

Connection to SL

A TSL grammar with the universal tier (every symbol on tier) reduces to an SL grammar — projection is the identity. This gives the inclusion IsStrictlyLocal ⊆ IsTierStrictlyLocal (proved in Hierarchy.lean).

Note on terminology

The tier here is the segmental tier in the sense of @cite{lambert-2022} Ch 3 (language-theoretic side, §3.2) — a subset of the alphabet, not an autosegmental melody floating above it. The TSL definition specializes to the case where projection is List.filter over a tier predicate (equivalently, an erasing string homomorphism that keeps tier symbols and deletes off-tier symbols, with no relabeling). For autosegmental tiers (high/low tone, nasal melody, register), see Theories/Phonology/Autosegmental/.

Single source of truth: Core.Tier

tierProject is the alias Core.Tier.apply (Core.Tier.byClass T) — the class-membership specialization of the autosegmental Kleisli morphism α → Option β. After the Tier.byClass migration to Prop+Decidable predicates, the alias contains no decide wrapper and the bridge to the autosegmental formalism is the identity, available either as rfl or via tierProject_eq_apply_byClass below.

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

Tier projection: the class-membership specialization of Core.Tier.apply to a Prop-valued predicate T. Keeps symbols satisfying T, erases the rest.

Defined as Core.Tier.apply (Core.Tier.byClass T) so the bridge to the autosegmental tier formalism is rfl. By Tier.apply_byClass this equals xs.filter (decide ∘ T).

Equations

• Core.Computability.Subregular.tierProject T xs = (Core.Tier.byClass T).apply xs

theorem Core.Computability.Subregular.tierProject_eq_apply_byClass {α : Type u_1} (T : α → Prop) [DecidablePred T] (xs : List α) : tierProject T xs = (Tier.byClass T).apply xs

Bridge identity to the autosegmental tier formalism: tierProject is by definition Tier.apply (Tier.byClass T). Since the migration of Tier.byClass to Prop+Decidable predicates, this is rfl with no decide plumbing.

theorem Core.Computability.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 Tier.apply_byClass. This is the canonical bridge to Lambert's filter-based formulation @cite{lambert-2022}.

@[simp]

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

theorem Core.Computability.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 Core.Computability.Subregular.tierProject_univ {α : Type u_1} (w : List α) : tierProject (fun (x : α) => True) w = w

Projection by the universal tier is the identity.

structure Core.Computability.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 : Set (Augmented α)

  The set of permitted k-factors of the projected string.

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

The language generated by a TSL grammar: project to the tier, then apply the SL test.

Equations

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

@[simp]

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

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

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

Equations

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

Inclusions

theorem Core.Computability.Subregular.IsStrictlyLocal.toIsTierStrictlyLocal {α : Type u_1} {k : ℕ} {L : Language α} (h : IsStrictlyLocal k L) : 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.