Erasing String Homomorphisms and Tier Projections

A string homomorphism h : α* → β* is a monoid homomorphism on free monoids: it satisfies h(uv) = h(u) ++ h(v) and h(ε) = ε. Such a map is letterwise when it is determined by its action on single symbols, and erasing when each symbol maps to at most one output symbol.

A tier projection in autosegmental phonology (@cite{goldsmith-1976}) and in tier-based learning (@cite{belth-2026}) is exactly the letterwise erasing case: 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.

This module provides:

• StringHom α β := α → List β — the general letterwise homomorphism.
• Tier α β := α → Option β — the erasing case.
• Tier.apply — lift to List α → List β (the projection itself).
• Tier.id, Tier.empty, Tier.byClass, Tier.total — constructors.

The monoid-homomorphism law (Tier.apply_append) holds definitionally via List.filterMap_append; this is what licenses tier projections in OT and HG constraint evaluation (mkOCP in Phonology/Constraints.lean already takes a generic project : C → List α, so Tier.apply T plugs in directly).

@cite{goldsmith-1976} @cite{belth-2026}

@[reducible, inline]

abbrev Core.StringHom (α : Type u) (β : Type v) : Type (max u v)

A letterwise string homomorphism α* → β*: a per-symbol map sending each input symbol to a (possibly empty, possibly multi-symbol) output string. Lifted to lists via List.flatMap.

Equations

• Core.StringHom α β = (α → List β)

def Core.StringHom.apply {α : Type u} {β : Type v} (h : StringHom α β) : List α → List β

Lift a letterwise homomorphism to List α → List β.

Equations

• h.apply = List.flatMap h

@[simp]

theorem Core.StringHom.apply_append {α : Type u} {β : Type v} (h : StringHom α β) (xs ys : List α) : h.apply (xs ++ ys) = h.apply xs ++ h.apply ys

Monoid-hom law: h distributes over concatenation.

@[simp]

theorem Core.StringHom.apply_nil {α : Type u} {β : Type v} (h : StringHom α β) : h.apply [] = []

Monoid-hom law: h sends the empty word to the empty word.

def Core.StringHom.letterMap {α : Type u} {β : Type v} (f : α → β) : StringHom α β

The letter-to-letter homomorphism induced by f : α → β: each input symbol maps to a singleton output. The image of apply (letterMap f) coincides with List.map f; see apply_letterMap.

Equations

• Core.StringHom.letterMap f a = [f a]

@[simp]

theorem Core.StringHom.apply_letterMap {α : Type u} {β : Type v} (f : α → β) (xs : List α) : (letterMap f).apply xs = List.map f xs

Letter-to-letter homomorphism applied to a list is List.map.

@[reducible, inline]

abbrev Core.Tier (α : 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

• Core.Tier α β = (α → Option β)

def Core.Tier.id {α : Type u} : Tier α α

The identity tier: every symbol projects to itself.

Equations

• Core.Tier.id = some

def Core.Tier.empty {α : Type u} {β : Type v} : Tier α β

The empty tier: no symbol projects.

Equations

• Core.Tier.empty x✝ = none

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

Tier 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

• Core.Tier.byClass p x = if p x then some x else none

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

Tier defined by a total function: every symbol projects to its image.

Equations

• Core.Tier.total f = some ∘ f

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

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

Equations

• T.apply = List.filterMap T

@[simp]

theorem Core.Tier.apply_append {α : Type u} {β : Type v} (T : Tier α β) (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 Core.Tier.apply_nil {α : Type u} {β : Type v} (T : Tier α β) : T.apply [] = []

Tier projection sends the empty word to the empty word.

@[simp]

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

The identity tier is the identity on lists.

@[simp]

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

The empty tier projects every list to the empty list.

theorem Core.Tier.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 Core.Tier.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 Core.Tier.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 Core.Tier.lastWith {α : Type u} {β : Type v} (T : Tier α β) (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 @cite{belth-2026}'s Disagree(A, F) / C __ ∘ proj(·, T).

Equations

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

def Core.Tier.firstWith {α : Type u} {β : Type v} (T : Tier α β) (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?