CV templates and template association

The skeletal species of template — [McC81]'s prosodic template, also called the CV-skeleton — as the sibling of the position-class AffixTemplate: an ordered sequence of consonantal and vocalic timing slots. A TemplateMatch pairs a consonantal root, a vocalism, and affixal material with a template and a list of association lines; spellout reads off the surface segments. Gemination is a one-to-many association from one melody element to several slots ([McC81]); a slot with no association line receives no phonetic realization.

Association conventions — one-to-one left-to-right, spreading, erasure rules — are derivational recipes and live with the studies that state them (Studies/McCarthy1981.lean, Studies/Faust2026.lean); this file provides the representations they manipulate.

Main declarations

• CVSlot, CVTemplate — skeletal slots and templates.
• Association — a sourced melody-to-slot association line.
• TemplateMatch — a root, vocalism, and affix matched to a template.
• TemplateMatch.spellout — the surface segments of a match.
• TemplateMatch.OrderedOn — the tier-internal well-formedness condition.
• TemplateMatch.links — the per-tier link sets, in the coordinates of the autosegmental substrate.

Main results

• TemplateMatch.orderedOn_iff — OrderedOn decomposes into the substrate's Autosegmental.IsNonCrossing plus [McC81]'s prohibition against many-to-one associations (SlotUnique), so the list-level representation here interprets into Phonology/Autosegmental/NonCrossing.lean rather than duplicating it.

inductive Morphology.CVSlot : Type

A slot in a CV-skeletal template ([McC81], [Low96]): a bare consonantal timing slot, a vowel timing slot, or a C-slot bearing [+consonantal], which blocks association from glides ([Fau26]).

• C : CVSlot

  A bare consonantal timing slot.

• V : CVSlot

  A vowel timing slot.

• Cspec : CVSlot

  A C-slot specified [+consonantal].

@[implicit_reducible]

instance Morphology.instDecidableEqCVSlot : DecidableEq CVSlot

Equations

• Morphology.instDecidableEqCVSlot x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Morphology.instReprCVSlot.repr : CVSlot → ℕ → Std.Format

Equations

• Morphology.instReprCVSlot.repr Morphology.CVSlot.C prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Morphology.CVSlot.C")).group prec✝
• Morphology.instReprCVSlot.repr Morphology.CVSlot.V prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Morphology.CVSlot.V")).group prec✝
• Morphology.instReprCVSlot.repr Morphology.CVSlot.Cspec prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Morphology.CVSlot.Cspec")).group prec✝

@[implicit_reducible]

instance Morphology.instReprCVSlot : Repr CVSlot

Equations

• Morphology.instReprCVSlot = { reprPrec := Morphology.instReprCVSlot.repr }

def Morphology.CVSlot.IsC : CVSlot → Prop

IsC s asserts that s is a C-slot, bare or [+consonantal].

Equations

• Morphology.CVSlot.C.IsC = True
• Morphology.CVSlot.Cspec.IsC = True
• Morphology.CVSlot.V.IsC = False

@[implicit_reducible]

instance Morphology.CVSlot.instDecidablePredIsC : DecidablePred IsC

Equations

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

def Morphology.CVSlot.IsV : CVSlot → Prop

IsV s asserts that s is a V-slot.

Equations

• Morphology.CVSlot.V.IsV = True
• x✝.IsV = False

@[implicit_reducible]

instance Morphology.CVSlot.instDecidablePredIsV : DecidablePred IsV

Equations

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

def Morphology.CVSlot.RequiresConsonantal : CVSlot → Prop

RequiresConsonantal s asserts that s demands a [+consonantal] segment.

Equations

• Morphology.CVSlot.Cspec.RequiresConsonantal = True
• x✝.RequiresConsonantal = False

@[implicit_reducible]

instance Morphology.CVSlot.instDecidablePredRequiresConsonantal : DecidablePred RequiresConsonantal

Equations

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

structure Morphology.CVTemplate : Type

A CV-skeletal template: an ordered sequence of timing slots.

• slots : List CVSlot

  The slots, in order.

def Morphology.instReprCVTemplate.repr : CVTemplate → ℕ → Std.Format

Equations

• Morphology.instReprCVTemplate.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "slots" ++ Std.Format.text " := " ++ (Std.Format.nest 9 (repr x✝.slots)).group) " }"

@[implicit_reducible]

instance Morphology.instReprCVTemplate : Repr CVTemplate

Equations

• Morphology.instReprCVTemplate = { reprPrec := Morphology.instReprCVTemplate.repr }

def Morphology.instDecidableEqCVTemplate.decEq (x✝ x✝¹ : CVTemplate) : Decidable (x✝ = x✝¹)

Equations

• Morphology.instDecidableEqCVTemplate.decEq { slots := a } { slots := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Morphology.instDecidableEqCVTemplate : DecidableEq CVTemplate

Equations

• Morphology.instDecidableEqCVTemplate = Morphology.instDecidableEqCVTemplate.decEq

def Morphology.CVTemplate.length (t : CVTemplate) : ℕ

The number of slots.

Equations

• t.length = t.slots.length

def Morphology.CVTemplate.cCount (t : CVTemplate) : ℕ

The number of C-slots.

Equations

• t.cCount = (List.filter (fun (s : Morphology.CVSlot) => decide s.IsC) t.slots).length

@[reducible, inline]

abbrev Morphology.CVTemplate.isFinalSlot (t : CVTemplate) (i : ℕ) : Prop

t.isFinalSlot i asserts that i is the final slot position.

Equations

• t.isFinalSlot i = (i + 1 = t.length)

def Morphology.CVTemplate.slotAt (t : CVTemplate) (i : ℕ) : Option CVSlot

The slot at position i, if in range.

Equations

• t.slotAt i = t.slots[i]?

def Morphology.CVTemplate.cSlots (t : CVTemplate) : List ℕ

The positions of the C-slots, in order.

Equations

• t.cSlots = List.filter (fun (i : ℕ) => match t.slots[i]? with | some s => decide s.IsC | none => false) (List.range t.length)

def Morphology.CVTemplate.vSlots (t : CVTemplate) : List ℕ

The positions of the V-slots, in order.

Equations

• t.vSlots = List.filter (fun (i : ℕ) => match t.slots[i]? with | some s => decide s.IsV | none => false) (List.range t.length)

inductive Morphology.AssocSource : Type

The tier a melody element on one end of an association line belongs to: the consonantal root, the vocalism, or affixal material. Tiers are morphologically defined ([McC81]) — one melody per morpheme class.

• root : AssocSource

  The consonantal root tier.

• vocalism : AssocSource

  The vocalic melody tier.

• affix : AssocSource

  An affixal tier ([Fau26]'s intruders are sister-exponent affixal material in this sense).

@[implicit_reducible]

instance Morphology.instDecidableEqAssocSource : DecidableEq AssocSource

Equations

• Morphology.instDecidableEqAssocSource x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Morphology.instReprAssocSource.repr : AssocSource → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Morphology.instReprAssocSource : Repr AssocSource

Equations

• Morphology.instReprAssocSource = { reprPrec := Morphology.instReprAssocSource.repr }

structure Morphology.Association : Type

A single melody-to-slot association line ([McC81]). melodyIndex indexes into the melody named by source; defaults to .root so ordinary root associations stay terse.

• source : AssocSource

  The tier the associated melody element lives on.

• melodyIndex : ℕ

  The index of the melody element on its tier.

• slotIndex : ℕ

  The index of the template slot.

@[implicit_reducible]

instance Morphology.instDecidableEqAssociation : DecidableEq Association

Equations

• Morphology.instDecidableEqAssociation = Morphology.instDecidableEqAssociation.decEq

def Morphology.instDecidableEqAssociation.decEq (x✝ x✝¹ : Association) : Decidable (x✝ = x✝¹)

Equations

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

def Morphology.instReprAssociation.repr : Association → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Morphology.instReprAssociation : Repr Association

Equations

• Morphology.instReprAssociation = { reprPrec := Morphology.instReprAssociation.repr }

structure Morphology.TemplateMatch (α : Type u_1) : Type u_1

A consonantal root, a vocalism, and affixal material matched to a template by a list of association lines. Different candidate realizations of the same morpheme combination are different TemplateMatch values sharing everything but associations; gemination is one melody index associated to several slots.

• root : ConsonantalRoot α

  The consonantal root.

• vocalism : List α

  The vocalic melody.

• affix : List α

  The affixal material.

• template : CVTemplate

  The template.

• associations : List Association

  The association lines.

@[implicit_reducible]

instance Morphology.instReprTemplateMatch {α✝ : Type u_1} [Repr α✝] : Repr (TemplateMatch α✝)

Equations

• Morphology.instReprTemplateMatch = { reprPrec := Morphology.instReprTemplateMatch.repr }

def Morphology.instReprTemplateMatch.repr {α✝ : Type u_1} [Repr α✝] : TemplateMatch α✝ → ℕ → Std.Format

Equations

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

def Morphology.instDecidableEqTemplateMatch.decEq {α✝ : Type u_1} [DecidableEq α✝] (x✝ x✝¹ : TemplateMatch α✝) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Morphology.instDecidableEqTemplateMatch {α✝ : Type u_1} [DecidableEq α✝] : DecidableEq (TemplateMatch α✝)

Equations

• Morphology.instDecidableEqTemplateMatch = Morphology.instDecidableEqTemplateMatch.decEq

def Morphology.TemplateMatch.melody {α : Type u_1} (m : TemplateMatch α) : AssocSource → List α

The melody of a tier.

Equations

• m.melody Morphology.AssocSource.root = m.root.segments
• m.melody Morphology.AssocSource.vocalism = m.vocalism
• m.melody Morphology.AssocSource.affix = m.affix

def Morphology.TemplateMatch.segmentAt {α : Type u_1} (m : TemplateMatch α) (a : Association) : Option α

The segment an association line contributes, if its index is in range.

Equations

• m.segmentAt a = (m.melody a.source)[a.melodyIndex]?

def Morphology.TemplateMatch.spellout {α : Type u_1} (m : TemplateMatch α) : List α

The surface segments of the match: each slot contributes the segment of its first association line; a slot with no association receives no phonetic realization ([McC81]).

Equations

• m.spellout = List.filterMap (fun (i : ℕ) => (List.find? (fun (x : Morphology.Association) => x.slotIndex == i) m.associations).bind m.segmentAt) (List.range m.template.length)

def Morphology.TemplateMatch.unfilledCSlots {α : Type u_1} (m : TemplateMatch α) : List ℕ

The C-slot positions not filled by any association.

Equations

• m.unfilledCSlots = List.filter (fun (i : ℕ) => !m.associations.any fun (x : Morphology.Association) => x.slotIndex == i) m.template.cSlots

@[reducible, inline]

abbrev Morphology.TemplateMatch.allCSlotsFilled {α : Type u_1} (m : TemplateMatch α) : Prop

m.allCSlotsFilled asserts that every C-slot is filled by some association line.

Equations

• m.allCSlotsFilled = (m.unfilledCSlots = [])

@[reducible, inline]

abbrev Morphology.TemplateMatch.inBounds {α : Type u_1} (m : TemplateMatch α) : Prop

m.inBounds asserts that every association line points to an in-range melody element and slot.

Equations

• m.inBounds = ∀ a ∈ m.associations, a.slotIndex < m.template.length ∧ a.melodyIndex < (m.melody a.source).length

def Morphology.TemplateMatch.OrderedOn {α : Type u_1} (m : TemplateMatch α) (s : AssocSource) : Prop

m.OrderedOn s asserts that the association lines from tier s do not cross: distinct melody elements associate to slots in melody order ([Gol76]'s no-crossing condition, within one tier).

Equations

• m.OrderedOn s = ∀ a ∈ m.associations, ∀ b ∈ m.associations, a.source = s → b.source = s → a.melodyIndex < b.melodyIndex → a.slotIndex < b.slotIndex

@[implicit_reducible]

instance Morphology.TemplateMatch.instDecidableAllCSlotsFilled {α : Type u_1} (m : TemplateMatch α) : Decidable m.allCSlotsFilled

Equations

• m.instDecidableAllCSlotsFilled = m.unfilledCSlots.instDecidableEqNil

@[implicit_reducible]

instance Morphology.TemplateMatch.instDecidableInBounds {α : Type u_1} (m : TemplateMatch α) : Decidable m.inBounds

Equations

• m.instDecidableInBounds = List.decidableBAll (fun (a : Morphology.Association) => a.slotIndex < m.template.length ∧ a.melodyIndex < (m.melody a.source).length) m.associations

@[implicit_reducible]

instance Morphology.TemplateMatch.instDecidableOrderedOn {α : Type u_1} (m : TemplateMatch α) (s : AssocSource) : Decidable (m.OrderedOn s)

Equations

• m.instDecidableOrderedOn s = Morphology.TemplateMatch.instDecidableOrderedOn._aux_1 m s

theorem Morphology.TemplateMatch.spellout_nil {α : Type u_1} (r : ConsonantalRoot α) (t : CVTemplate) : { root := r, template := t, associations := [] }.spellout = []

A match with no associations spells out to nothing.

Interpretation into the autosegmental substrate

def Morphology.TemplateMatch.links {α : Type u_1} (m : TemplateMatch α) (s : AssocSource) : Finset (ℕ × ℕ)

The link set of tier s, in the two-layer coordinates of Phonology/Autosegmental/NonCrossing.lean: one (melodyIndex, slotIndex) pair per association line from s.

Equations

• m.links s = (List.map (fun (a : Morphology.Association) => (a.melodyIndex, a.slotIndex)) (List.filter (fun (x : Morphology.Association) => x.source == s) m.associations)).toFinset

def Morphology.TemplateMatch.SlotUnique {α : Type u_1} (m : TemplateMatch α) (s : AssocSource) : Prop

m.SlotUnique s asserts that no slot hosts two distinct melody elements of tier s — [McC81]'s prohibition against many-to-one associations.

Equations

• m.SlotUnique s = ∀ a ∈ m.associations, ∀ b ∈ m.associations, a.source = s → b.source = s → a.slotIndex = b.slotIndex → a.melodyIndex = b.melodyIndex

@[implicit_reducible]

instance Morphology.TemplateMatch.instDecidableSlotUnique {α : Type u_1} (m : TemplateMatch α) (s : AssocSource) : Decidable (m.SlotUnique s)

Equations

• m.instDecidableSlotUnique s = Morphology.TemplateMatch.instDecidableSlotUnique._aux_1 m s

theorem Morphology.TemplateMatch.mem_links {α : Type u_1} (m : TemplateMatch α) (p : ℕ × ℕ) (s : AssocSource) : p ∈ m.links s ↔ ∃ a ∈ m.associations, a.source = s ∧ a.melodyIndex = p.1 ∧ a.slotIndex = p.2

theorem Morphology.TemplateMatch.orderedOn_iff {α : Type u_1} (m : TemplateMatch α) (s : AssocSource) : m.OrderedOn s ↔ Autosegmental.IsNonCrossing (m.links s) ∧ m.SlotUnique s

A tier is OrderedOn iff its link set is non-crossing in the sense of the autosegmental substrate and one-to-one per slot: [Gol76]'s No-Crossing Constraint plus [McC81]'s prohibition against many-to-one associations.