Morae

The mora (μ) — the base node of the prosodic hierarchy and the unit of syllable weight, following [Hay89]. A mora is an autosegmental node on the prosodic tier that dominates melodic material (segments). Weight is the number of morae; a syllable, foot, and word are each a structure dominating the level below (Syllable, Foot, Word), so weight aggregates up one uniform moraCount API.

A mora that dominates nothing (dominates = []) is stranded: the segment it dominated was deleted but the μ node survives. This is the engine of compensatory lengthening — the stranded μ is re-associated to an adjacent segment rather than a count being shuffled on a side channel.

Main definitions

• Mora — a prosodic-tier node dominating a (possibly empty) melody.
• Mora.of, Mora.stranded — the ordinary and floating morae.
• Mora.IsStranded — the mora dominates no melody.

structure Prosody.Mora : Type

A mora (μ): a prosodic-tier node dominating the melody linked to it. dominates = [] is a stranded/floating mora (its segment was deleted but the μ node survives). A long vowel is two morae dominating the same melody; a non-moraic coda rides on the preceding mora's dominates.

• dominates : List Phonology.Segment

  The melody this μ node dominates; [] is a stranded/floating mora.

@[implicit_reducible]

instance Prosody.instDecidableEqMora : DecidableEq Mora

Equations

• Prosody.instDecidableEqMora = Prosody.instDecidableEqMora.decEq

def Prosody.instDecidableEqMora.decEq (x✝ x✝¹ : Mora) : Decidable (x✝ = x✝¹)

Equations

• Prosody.instDecidableEqMora.decEq { dominates := a } { dominates := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Prosody.Mora.of (s : Phonology.Segment) : Mora

The mora dominating a single segment.

Equations

• Prosody.Mora.of s = { dominates := [s] }

def Prosody.Mora.stranded : Mora

A stranded (floating) mora, dominating no melody.

Equations

• Prosody.Mora.stranded = { dominates := [] }

@[reducible, inline]

abbrev Prosody.Mora.IsStranded (μ : Mora) : Prop

The mora is stranded — it dominates no melody.

Equations

• μ.IsStranded = (μ.dominates = [])

def Prosody.Mora.attach (μ : Mora) (segs : List Phonology.Segment) : Mora

Attach extra melody (e.g. a non-moraic coda) to a mora.

Equations

• μ.attach segs = { dominates := μ.dominates ++ segs }