Tier Projections (erasing letterwise homomorphisms)

A tier projection in autosegmental phonology ([Gol76]) and in tier-based learning ([Bel26]) is a letterwise erasing string homomorphism: a per-symbol partial map α → Option β, lifted to α* → β* via List.filterMap. This is the morphism α → β in the Kleisli category of Option over the free-monoid functor.

General (non-erasing) string homomorphisms need no bespoke wrapper: a per-symbol map is just α → List β, and the string action is List.flatMap — which, since List α = FreeMonoid α, is the free-monoid lift FreeMonoid.lift. CFL closure under string homomorphism lives in Linglib.Core.Computability.ContextFreeGrammar.Map.

This module provides:

• TierProjection α β := α → Option β — the erasing case.
• TierProjection.apply — lift to List α → List β (the projection itself).
• TierProjection.applyHom — that lift bundled as a FreeMonoid α →* FreeMonoid β.
• id, empty, byClass, total — constructors.

The monoid-homomorphism law (TierProjection.apply_append) holds definitionally via List.filterMap_append; this is what licenses tier projections in OT and HG constraint evaluation (mkForbidPairsOnTier in Phonology/OptimalityTheory/Constraints.lean takes a generic TierProjection, so TierProjection.apply T plugs in directly).

Home: Core/Computability/ — the content is pure List/Option combinatorics (the Option-Kleisli morphism on free monoids), with no linguistic content in any type signature; the linguistic interpretation lives entirely in the Phonology/ and Studies/ consumers. The subregular projection Subregular.tierProject (List.filter) and its monoid-hom packaging Subregular.tierProjectHom, both in Core/Computability/Subregular/Language/, are the single-alphabet byClass specialization of this morphism; unifying the three onto this keystone (so they coincide by rfl) is a follow-up.

[Gol76] [Bel26]

@[reducible, inline]

abbrev TierProjection (α : Type u) (β : Type v) : Type (max u v)

A tier projection α* → β*: a per-symbol partial map. Each input symbol either projects to one tier symbol or is erased.

This is the morphism α → β in the Kleisli category of Option, and equivalently a letterwise erasing string homomorphism. The lift to List α → List β is List.filterMap.

Equations

• TierProjection α β = (α → Option β)

def TierProjection.id {α : Type u} : TierProjection α α

The identity tier: every symbol projects to itself.

Equations

• TierProjection.id = some

def TierProjection.empty {α : Type u} {β : Type v} : TierProjection α β

The empty tier: no symbol projects.

Equations

• TierProjection.empty x✝ = none

def TierProjection.byClass {α : Type u} (p : α → Prop) [DecidablePred p] : TierProjection α α

A tier projection defined by a class predicate: keep symbols satisfying p, erase the rest. The standard form for autosegmental tonal/featural tiers.

Following mathlib's Finset.filter / Multiset.filter convention, p is Prop-valued with [DecidablePred], so call sites can pass structural predicates (fun x => x = .l, fun x => IsCons x) without inserting decide wrappers.

Equations

• TierProjection.byClass p x = if p x then some x else none

def TierProjection.total {α : Type u} {β : Type v} (f : α → β) : TierProjection α β

A tier projection defined by a total function: every symbol projects to its image.

Equations

• TierProjection.total f = some ∘ f

def TierProjection.apply {α : Type u} {β : Type v} (T : TierProjection α β) : List α → List β

Lift a tier to List α → List β. This is the canonical projection.

Equations

• T.apply = List.filterMap T

@[simp]

theorem TierProjection.apply_append {α : Type u} {β : Type v} (T : TierProjection α β) (xs ys : List α) : T.apply (xs ++ ys) = T.apply xs ++ T.apply ys

Tier projection distributes over concatenation. This is the monoid-homomorphism property — load-bearing for compositional tier-based constraint evaluation.

@[simp]

theorem TierProjection.apply_nil {α : Type u} {β : Type v} (T : TierProjection α β) : T.apply [] = []

Tier projection sends the empty word to the empty word.

def TierProjection.applyHom {α : Type u} {β : Type v} (T : TierProjection α β) : FreeMonoid α →* FreeMonoid β

The tier projection bundled as a monoid homomorphism FreeMonoid α →* FreeMonoid β of strings: apply preserves 1 (apply_nil) and * (apply_append). Named specializations — e.g. Subregular.tierProjectHom — are defined as applyHom of a particular projection, inheriting the hom laws by construction rather than re-proving them.

Equations

• T.applyHom = { toFun := T.apply, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem TierProjection.applyHom_apply {α : Type u} {β : Type v} (T : TierProjection α β) (w : FreeMonoid α) : T.applyHom w = T.apply w

@[simp]

theorem TierProjection.apply_id {α : Type u} (xs : List α) : TierProjection.id.apply xs = xs

The identity tier is the identity on lists.

@[simp]

theorem TierProjection.apply_empty {α : Type u} {β : Type v} (xs : List α) : empty.apply xs = []

The empty tier projects every list to the empty list.

theorem TierProjection.apply_byClass {α : Type u} (p : α → Prop) [DecidablePred p] (xs : List α) : (byClass p).apply xs = List.filter (fun (x : α) => decide (p x)) xs

A class-predicate tier acts as List.filter. The right-hand side inserts decide because List.filter is Bool-valued; consumers that already work in Bool should use this lemma directly.

@[simp]

theorem TierProjection.apply_total {α : Type u} {β : Type v} (f : α → β) (xs : List α) : (total f).apply xs = List.map f xs

A total-function tier acts as List.map.

@[simp]

theorem TierProjection.length_apply_total {α : Type u} {β : Type v} (f : α → β) (xs : List α) : ((total f).apply xs).length = xs.length

total is length-preserving — all symbols survive.

def TierProjection.lastWith {α : Type u} {β : Type v} (T : TierProjection α β) (q : β → Prop) [DecidablePred q] (xs : List α) : Option β

The last (rightmost) projected symbol of xs satisfying q. The standard "preceding tier-adjacent context" lookup for rules like [Bel26]'s Disagree(A, F) / C __ ∘ proj(·, T).

Equations

• T.lastWith q xs = (List.filter (fun (y : β) => decide (q y)) (T.apply xs)).getLast?

def TierProjection.firstWith {α : Type u} {β : Type v} (T : TierProjection α β) (q : β → Prop) [DecidablePred q] (xs : List α) : Option β

The first (leftmost) projected symbol of xs satisfying q. The symmetric right-context lookup for C / __ C ∘ proj(·, T) rules.

Equations

• T.firstWith q xs = (List.filter (fun (y : β) => decide (q y)) (T.apply xs)).head?