Docs / Morphology / Morphotactics / TemplateMatch

Template matches

import Linglib.Morphology.Morphotactics.TemplateMatch · namespace Morphology

In McCarthy's prosodic theory of nonconcatenative morphology, a word is built by associating melodies on separate morphemic tiers, a consonantal root, a vocalism, and affixal material, with the slots of a prosodic template, a CV skeleton. A TemplateMatch records the three melodies, the template, and the association lines, and spellout reads off the surface segments. Gemination is one melody element associated to several slots, and a slot with no association line receives no phonetic realization. The association conventions that draw the lines are in Morphology/Morphotactics/Association.lean.

Main definitions

AssocSource: the morphemic tier of a melody.
Association: an association line from a melody element to a template slot.
TemplateMatch: a root, vocalism, and affix associated with a template.
TemplateMatch.spellout, TemplateMatch.map: the surface segments of a match, and the relabelling of its melodies.
TemplateMatch.OrderedOn: the association lines of a tier do not cross.
TemplateMatch.links, TemplateMatch.linkCount: the lines of a tier as pairs of positions, and the number of lines from one of its elements.

Main results

TemplateMatch.orderedOn_iff: OrderedOn is Autosegmental.IsNonCrossing with each slot hosting at most one element of the tier.
TemplateMatch.spellout_map: relabelling the melodies relabels the surface segments.

References

McCarthy 1981, A Prosodic Theory of Nonconcatenative Morphology formalized
Faust 2026, Intrusion as Template Satisfaction and the QaTaT–QaTa Problem in Semitic formalized
Goldsmith 1976, Autosegmental Phonology

Declarations

The morphemic tier that the melody element at one end of an association line belongs to, which is the consonantal root, the vocalism, or affixal material (McCarthy 1981).

inductive AssocSource L53–63

Type

root : AssocSource
The consonantal root tier.
vocalism : AssocSource
The vocalic melody tier.
affix : AssocSource
An affixal tier (Faust 2026's intruders are sister-exponent affixal material in this sense).

Derives DecidableEq, Repr.

Used by Association, TemplateMatch.melody, TemplateMatch.OrderedOn, TemplateMatch.instDecidableOrderedOn, TemplateMatch.melody_map, TemplateMatch.links, TemplateMatch.linkCount, TemplateMatch.linkCount_map, TemplateMatch.mem_links, TemplateMatch.orderedOn_iff

Used in Morphology/Morphotactics/Association, McCarthy1981

An association line from element melodyIndex of the melody of source to slot slotIndex of the template (McCarthy 1981). The source defaults to .root.

structure Association L65–74

Type

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.

Derives DecidableEq, Repr.

Built from

Used by TemplateMatch, TemplateMatch.segmentAt, TemplateMatch.spellout, TemplateMatch.unfilledCSlots, TemplateMatch.segmentAt_map, TemplateMatch.links, TemplateMatch.linkCount

Used in Morphology/Morphotactics/Association, Arad2005, Faust2026

A consonantal root, a vocalism, and affixal material associated with a template. Candidate realizations of the same morphemes differ only in their association lines.

structure TemplateMatch L76–89

(α : Type u_1) :

Type u_1

root : ConsonantalRoot α
The consonantal root.
vocalism : List α
The vocalic melody.
affix : List α
The affixal material.
template : Autosegmental.Skeleton
The template.
associations : List Association
The association lines.

Derives Repr, DecidableEq.

Built from

Used by TemplateMatch.melody, TemplateMatch.segmentAt, TemplateMatch.spellout, TemplateMatch.unfilledCSlots, TemplateMatch.allCSlotsFilled, TemplateMatch.OrderedOn, TemplateMatch.instDecidableAllCSlotsFilled, TemplateMatch.instDecidableOrderedOn, TemplateMatch.map, TemplateMatch.associations_map, TemplateMatch.template_map, TemplateMatch.melody_map, TemplateMatch.segmentAt_map, TemplateMatch.spellout_map, TemplateMatch.links, TemplateMatch.linkCount, TemplateMatch.linkCount_map, TemplateMatch.mem_links, TemplateMatch.orderedOn_iff

Used in Morphology/Morphotactics/Association, AfkirZellou2025, Arad2005, Faust2026, McCarthy1981

L95–99

L101–102

The surface segments of the match. Each slot contributes the segment of its first association line, and a slot with no association receives no phonetic realization (McCarthy 1981).

def TemplateMatch.spellout L104–109

{α : Type u_1} (m : TemplateMatch α) :

List α

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

Built from , ,

Used by TemplateMatch.spellout_map

Used in AfkirZellou2025, Arad2005, McCarthy1981

L111–113

L115–117

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

def TemplateMatch.OrderedOn L119–125

{α : Type u_1} (m : TemplateMatch α) (s : AssocSource) :

Prop

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

Built from ,

Used by TemplateMatch.instDecidableOrderedOn, TemplateMatch.orderedOn_iff

Used in McCarthy1981

L127

L129–139

The match with each melodic element relabeled.

def TemplateMatch.map L141–144

{α : Type u_1} (m : TemplateMatch α) {β : Type u_2} (f : α → β) :

TemplateMatch β

m.map f = { root := ConsonantalRoot.map f m.root, vocalism := List.map f m.vocalism, affix := List.map f m.affix, template := m.template, associations := m.associations }

Built from

Used by TemplateMatch.associations_map, TemplateMatch.template_map, TemplateMatch.melody_map, TemplateMatch.segmentAt_map, TemplateMatch.spellout_map, TemplateMatch.linkCount_map

Used in Morphology/Morphotactics/Association, AfkirZellou2025, Arad2005, McCarthy1981

Relabeling the melodic elements relabels the surface segments.

theorem TemplateMatch.spellout_map L160–165

{α : Type u_1} (m : TemplateMatch α) {β : Type u_2} (f : α → β) :

(m.map f).spellout = List.map f m.spellout

Built from , ,

Interpretation into the autosegmental substrate

The lines of tier s as (melodyIndex, slotIndex) pairs.

def TemplateMatch.links L171–173

{α : Type u_1} (m : TemplateMatch α) (s : AssocSource) :

Finset (ℕ × ℕ)

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

Built from , ,

Used by TemplateMatch.mem_links, TemplateMatch.orderedOn_iff

Used in Faust2026

The number of lines from element k of tier s; a geminate is an element with two.

def TemplateMatch.linkCount L175–177

{α : Type u_1} (m : TemplateMatch α) (s : AssocSource) (k : ℕ) :

ℕ

m.linkCount s k = List.countP (fun (a : Association) => a.source == s && a.melodyIndex == k) m.associations

Built from , ,

Used by TemplateMatch.linkCount_map

Used in Arad2005, McCarthy1981

L179–180

L182–184

A tier is OrderedOn iff its lines are non-crossing and each slot hosts at most one element of the tier, which is Goldsmith 1976's No-Crossing Constraint plus McCarthy 1981's prohibition against many-to-one associations.

theorem TemplateMatch.orderedOn_iff L186–206

{α : Type u_1} (m : TemplateMatch α) (s : AssocSource) :

m.OrderedOn s ↔ Autosegmental.IsNonCrossing ↑(m.links s) ∧ Set.InjOn Prod.snd ↑(m.links s)

Built from , , ,