Moraic Phonology

Moraic representations following @cite{hayes-1989}: the mora (μ) as the fundamental unit of prosodic structure. Segments associate to morae, morae associate to syllables. This replaces the segmental prosodic tier (X theory, CV theory) with a prosodic tier whose elements directly encode weight.

Key design decisions from @cite{hayes-1989}:

• Onset consonants are non-moraic (universally)
• Short consonants are underlyingly moraless; coda consonants may receive a mora via Weight by Position (language-specific)
• Long vowels link to two morae; geminates link one segment to two morae
• Glides are moraless (zero morae)

The moraic tier σ → μ → segment replaces the List Segment representation in Syllable.Defs, which is essentially a segmental (X-theory) view.

@cite{hayes-1989}

inductive Phonology.Moraic.MoraCount : Type

A segment's underlying moraic specification.

Following @cite{hayes-1989}:

• 0 morae: glides, onset consonants
• 1 mora: short vowels, short consonants (when moraic by WBP)
• 2 morae: long vowels, geminates, long syllabic consonants

• zero : MoraCount
• one : MoraCount
• two : MoraCount

@[implicit_reducible]

instance Phonology.Moraic.instDecidableEqMoraCount : DecidableEq MoraCount

Equations

• Phonology.Moraic.instDecidableEqMoraCount x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phonology.Moraic.instReprMoraCount.repr : MoraCount → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phonology.Moraic.instReprMoraCount : Repr MoraCount

Equations

• Phonology.Moraic.instReprMoraCount = { reprPrec := Phonology.Moraic.instReprMoraCount.repr }

def Phonology.Moraic.MoraCount.toNat : MoraCount → ℕ

Equations

• Phonology.Moraic.MoraCount.zero.toNat = 0
• Phonology.Moraic.MoraCount.one.toNat = 1
• Phonology.Moraic.MoraCount.two.toNat = 2

def Phonology.Moraic.MoraCount.succ : MoraCount → MoraCount

Increment a mora count by one (capped at two).

Equations

• Phonology.Moraic.MoraCount.zero.succ = Phonology.Moraic.MoraCount.one
• Phonology.Moraic.MoraCount.one.succ = Phonology.Moraic.MoraCount.two
• Phonology.Moraic.MoraCount.two.succ = Phonology.Moraic.MoraCount.two

structure Phonology.Moraic.MoraicSeg : Type

A segment on the moraic tier, carrying its mora count.

This captures the association between the segmental and prosodic tiers: the segment seg is linked to morae morae dominated by a syllable node.

• seg : Segment
• morae : MoraCount

structure Phonology.Moraic.MoraicSyllable : Type

A syllable in moraic theory.

Following @cite{hayes-1989}: the syllable node σ directly dominates morae, which in turn dominate segments. Onset consonants adjoin directly to σ without intervening morae (they are weight-irrelevant).

The split between onset (non-moraic) and moraic (mora-bearing) segments is the structural core of moraic theory — it is this split that derives the onset deletion asymmetry.

• onset : List Segment

  Onset consonants: directly adjoined to σ, no mora.

• moraic : List MoraicSeg

  Mora-bearing segments: nucleus vowels and (optionally) coda consonants. Ordered left to right; nucleus segments precede coda segments.

structure Phonology.Moraic.MoraicForm : Type

A moraic form: a word parsed into moraic syllables.

• syllables : List MoraicSyllable

structure Phonology.Moraic.MoraicParams : Type

Language-specific parameters for moraic structure assignment.

Following @cite{hayes-1989}, Rule (10): moraic structure is partly language-specific. The key parameter is Weight by Position: whether coda consonants receive a mora. Languages like Latin have WBP (CVC = heavy); languages like Lardil lack it (CVC = light).

• wbp : Bool

  Does this language assign morae to coda consonants?

def Phonology.Moraic.syllableToMoraic (params : MoraicParams) (σ : Syllable.Syllable) : MoraicSyllable

Assign moraic structure to a Syllable according to MoraicParams.

Following @cite{hayes-1989}, §2: the moraic structure assignment rules are:

1. Nucleus segments receive one mora each
2. Coda consonants receive a mora iff WBP is active
3. Onset consonants are non-moraic

This is the key function that derives moraic syllables from the existing segmental Syllable representation + language-specific params, rather than stipulating mora counts by hand.

Equations

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

def Phonology.Moraic.syllabifiedToMoraic (params : MoraicParams) (sf : Syllable.SyllabifiedForm) : MoraicForm

Convert an entire SyllabifiedForm to a MoraicForm.

Equations

• Phonology.Moraic.syllabifiedToMoraic params sf = { syllables := List.map (Phonology.Moraic.syllableToMoraic params) sf.syllables }

def Phonology.Moraic.MoraicSyllable.moraCount (σ : MoraicSyllable) : ℕ

Total mora count of a moraic syllable.

Equations

• σ.moraCount = List.foldl (fun (x1 : ℕ) (x2 : Phonology.Moraic.MoraicSeg) => x1 + x2.morae.toNat) 0 σ.moraic

def Phonology.Moraic.MoraicForm.totalMorae (f : MoraicForm) : ℕ

Total mora count of a moraic form.

Equations

• f.totalMorae = List.foldl (fun (x1 : ℕ) (x2 : Phonology.Moraic.MoraicSyllable) => x1 + x2.moraCount) 0 f.syllables

def Phonology.Moraic.MoraicSyllable.toSyllWeight (σ : MoraicSyllable) : Syllable.SyllWeight

Convert moraic syllable to SyllWeight by extracting the mora count.

This is lossless: σ.toSyllWeight.morae = σ.moraCount by definition. No classification into light/heavy/superheavy bins — the exact mora count passes through.

Equations

• σ.toSyllWeight = { morae := σ.moraCount }

def Phonology.Moraic.MoraicForm.toPrWd (f : MoraicForm) : ProsodicWord.PrWd

Convert a moraic form to a PrWd (prosodic word) weight profile.

This connects moraic representations to the prosodic word layer, enabling minimal word constraints, metrical parsing, and stress assignment to operate on moraically-derived weight profiles.

Equations

• f.toPrWd = { syllables := List.map Phonology.Moraic.MoraicSyllable.toSyllWeight f.syllables }

theorem Phonology.Moraic.foldl_morae_map (mc : MoraCount) (xs : List Segment) (init : ℕ) : List.foldl (fun (x1 : ℕ) (x2 : MoraicSeg) => x1 + x2.morae.toNat) init (List.map (fun (s : Segment) => { seg := s, morae := mc }) xs) = init + xs.length * mc.toNat

Helper: folding mora counts over a list of segments all mapped to the same MoraCount equals init + length * moraCount.

theorem Phonology.Moraic.syllableToMoraic_moraCount_wbp (σ : Syllable.Syllable) : (syllableToMoraic { wbp := true } σ).moraCount = σ.moraCount

General bridge: syllableToMoraic with WBP produces the same mora count as Syllable.moraCount codaMoraic=true. Fully general over all syllables.

theorem Phonology.Moraic.syllableToMoraic_moraCount_no_wbp (σ : Syllable.Syllable) : (syllableToMoraic { wbp := false } σ).moraCount = σ.moraCount false

General bridge: syllableToMoraic without WBP produces the same mora count as Syllable.moraCount codaMoraic=false.

theorem Phonology.Moraic.syllableToMoraic_weight_wbp (σ : Syllable.Syllable) : (syllableToMoraic { wbp := true } σ).toSyllWeight = σ.weight

General bridge: moraic weight classification agrees with segmental weight classification for WBP languages. This connects MoraicSyllable.toSyllWeight to Syllable.weight — two independently defined weight functions that must agree for the moraic theory to be consistent with the segmental view.

theorem Phonology.Moraic.syllableToMoraic_weight_no_wbp (σ : Syllable.Syllable) : (syllableToMoraic { wbp := false } σ).toSyllWeight = σ.weight false

General bridge for non-WBP languages.

theorem Phonology.Moraic.syllableToMoraic_cv_light (params : MoraicParams) (o n : Segment) : (syllableToMoraic params { onset := [o], nucleus := [n], coda := [] }).toSyllWeight = Syllable.SyllWeight.light

syllableToMoraic preserves CV = light regardless of WBP.

theorem Phonology.Moraic.cv_moraic_light (v : Segment) : { onset := [], moraic := [{ seg := v, morae := MoraCount.one }] }.toSyllWeight = Syllable.SyllWeight.light

A CV syllable (one monomoraic vowel, no coda) is light.

theorem Phonology.Moraic.cvv_moraic_heavy (v : Segment) : { onset := [], moraic := [{ seg := v, morae := MoraCount.two }] }.toSyllWeight = Syllable.SyllWeight.heavy

A CVV syllable (one bimoraic vowel) is heavy.

theorem Phonology.Moraic.cvc_wbp_heavy (v c₁ c₂ : Segment) : { onset := [c₁], moraic := [{ seg := v, morae := MoraCount.one }, { seg := c₂, morae := MoraCount.one }] }.toSyllWeight = Syllable.SyllWeight.heavy

A CVC syllable with WBP (coda has one mora) is heavy.

theorem Phonology.Moraic.cvc_no_wbp_light (v c₁ c₂ : Segment) : { onset := [c₁], moraic := [{ seg := v, morae := MoraCount.one }, { seg := c₂, morae := MoraCount.zero }] }.toSyllWeight = Syllable.SyllWeight.light

A CVC syllable without WBP (coda has zero morae) is light.

theorem Phonology.Moraic.cvvc_superheavy (v c₁ c₂ : Segment) : { onset := [c₁], moraic := [{ seg := v, morae := MoraCount.two }, { seg := c₂, morae := MoraCount.one }] }.toSyllWeight = Syllable.SyllWeight.superheavy

A CVVC syllable (long vowel + moraic coda) is superheavy.

theorem Phonology.Moraic.geminate_makes_heavy (v seg : Segment) : { onset := [], moraic := [{ seg := v, morae := MoraCount.one }, { seg := seg, morae := MoraCount.one }] }.toSyllWeight = Syllable.SyllWeight.heavy

Geminate: one segment linked to two morae, straddling a syllable boundary. The first half contributes its mora(e) to the coda of σ₁.

theorem Phonology.Moraic.moraic_minword (f : MoraicForm) : f.toPrWd.satisfiesMinWord = decide (f.toPrWd.moraCount ≥ 2)

The moraic minimal word: satisfiesMinWord checks ≥ 2 morae by default. This connects moraic representations to PrWd's bimoraic minimum.

theorem Phonology.Moraic.toSyllWeight_morae_faithful (σ : MoraicSyllable) : σ.toSyllWeight.morae = σ.moraCount

Round-trip fidelity: toSyllWeight.morae recovers the exact mora count. No bounds needed — SyllWeight is now a Nat wrapper, not a lossy enum.