Syllables

[Hay89] [Hym85] [Sel82] [Cle90]

The syllable (σ) — the level above the mora in the prosodic hierarchy: a headed moraic constituent ([Hay89]; [Hym85]). A non-moraic onset sits over a moraic spine whose head is the nucleus — the sonority peak ([Cle90]; the "nucleus = head of σ" reading follows dependency/government phonology). The nucleus mora is mandatory and structurally initial (a σ has ≥1 mora by construction; there is no head-direction parameter — unlike the foot); tail carries any further nuclear morae (long vowels) and a moraic coda.

The moraic structure is the carrier (weight is mora-based and load-bearing, so — unlike the foot — the tree and onset-rime are secondary). The rival onset-rime theory ([Sel82]) is a re-representation (toOnsetRime), proved to agree with the moraic carrier on weight; the segment string is the yield.

Main definitions

• Syllable — a headed moraic σ: onset, a nucleus head mora, and a tail of morae.
• Syllable.morae / nucleusMora / nucleusSegments / weight / moraCount.
• Syllable.IsHeavy / IsLight — the weight inventory (sonority/SSP well-formedness is a syllabification follow-up).
• Syllable.ofCV / mk' — smart constructors (a non-empty nucleus is required).
• Syllable.yield / toOnsetRime — re-representations; toOnsetRime_weight is the weight-correspondence between the moraic and onset-rime theories.
• Syllable.Weight — Nat (the mora count), with .light/.heavy/.superheavy.

Syllables

structure Prosody.Syllable : Type

σ — a headed moraic syllable ([Hay89]): a non-moraic onset, a nucleus head mora (the sonority peak; mandatory, so σ has ≥1 mora and the head is initial by construction), and a tail of further morae (long-vowel morae + a moraic coda).

• onset : List Phonology.Segment

  The non-moraic onset melody.

• head : Mora

  The nucleus mora — the sonority peak; mandatory, so σ has ≥ 1 mora.

• tail : List Mora

  Further morae: long-vowel morae and a moraic coda.

def Prosody.instDecidableEqSyllable.decEq (x✝ x✝¹ : Syllable) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Prosody.instDecidableEqSyllable : DecidableEq Syllable

Equations

• Prosody.instDecidableEqSyllable = Prosody.instDecidableEqSyllable.decEq

@[reducible, inline]

abbrev Prosody.Syllable.Weight : Type

Syllable weight is just the mora count — there is no separate weight type. .light (1μ), .heavy (2μ), .superheavy (3μ) name the common values for readable weight profiles in metrical and accentual computations.

Equations

• Prosody.Syllable.Weight = ℕ

@[reducible, inline]

abbrev Prosody.Syllable.Weight.light : Weight

Equations

• Prosody.Syllable.Weight.light = 1

@[reducible, inline]

abbrev Prosody.Syllable.Weight.heavy : Weight

Equations

• Prosody.Syllable.Weight.heavy = 2

@[reducible, inline]

abbrev Prosody.Syllable.Weight.superheavy : Weight

Equations

• Prosody.Syllable.Weight.superheavy = 3

def Prosody.Syllable.morae (σ : Syllable) : List Mora

The moraic spine, nucleus (peak) first.

Equations

• σ.morae = σ.head :: σ.tail

@[reducible, inline]

abbrev Prosody.Syllable.nucleusMora (σ : Syllable) : Mora

The nucleus — the head mora (the sonority peak).

Equations

• σ.nucleusMora = σ.head

def Prosody.Syllable.nucleusSegments (σ : Syllable) : List Phonology.Segment

The nucleus segment(s).

Equations

• σ.nucleusSegments = σ.head.dominates

def Prosody.Syllable.moraCount (σ : Syllable) : ℕ

The number of morae — the syllable's weight.

Equations

• σ.moraCount = σ.morae.length

@[reducible, inline]

abbrev Prosody.Syllable.weight (σ : Syllable) : Weight

The syllable's weight (= its mora count).

Equations

• σ.weight = σ.moraCount

def Prosody.Syllable.IsHeavy (σ : Syllable) : Prop

A heavy syllable: at least two morae.

Equations

• σ.IsHeavy = (Prosody.Syllable.Weight.heavy ≤ σ.weight)

def Prosody.Syllable.IsLight (σ : Syllable) : Prop

A light syllable: exactly one mora.

Equations

• σ.IsLight = (σ.weight = Prosody.Syllable.Weight.light)

@[implicit_reducible]

instance Prosody.Syllable.instDecidableIsHeavy (σ : Syllable) : Decidable σ.IsHeavy

Equations

• σ.instDecidableIsHeavy = id inferInstance

@[implicit_reducible]

instance Prosody.Syllable.instDecidableIsLight (σ : Syllable) : Decidable σ.IsLight

Equations

• σ.instDecidableIsLight = id inferInstance

def Prosody.Syllable.mk' (onset : List Phonology.Segment) (nucleus : Mora) (coda : List Mora := []) : Syllable

Build a syllable from an explicit nucleus mora (+ optional further/coda morae).

Equations

• Prosody.Syllable.mk' onset nucleus coda = { onset := onset, head := nucleus, tail := coda }

def Prosody.Syllable.ofMorae (onset : List Phonology.Segment) (ms : List Mora) (h : ms ≠ [] := by simp) : Syllable

Build a syllable from an onset and a non-empty mora spine (nucleus = first mora).

Equations

• Prosody.Syllable.ofMorae onset ms h = { onset := onset, head := ms.head h, tail := ms.tail }

def Prosody.Syllable.ofCV (onset nucleus coda : List Phonology.Segment) (wbp : Bool := true) (hn : nucleus ≠ [] := by simp) : Syllable

Build a syllable from a segmental onset–nucleus–coda string. Each nucleus segment projects a mora (the first is the nucleus head); a coda segment projects its own mora iff Weight-by-Position is active ([Hay89]), else it rides the last nucleus mora (a non-moraic coda). A non-empty nucleus is required.

Equations

• One or more equations did not get rendered due to their size.
• Prosody.Syllable.ofCV onset [] coda wbp h = ⋯.elim

def Prosody.Syllable.yield (σ : Syllable) : List Phonology.Segment

The segment string (yield) of a syllable: onset followed by the moraic melody.

Equations

• σ.yield = σ.onset ++ List.flatMap (fun (x : Prosody.Mora) => x.dominates) σ.morae

Moraic operations (stranding and re-licensing)

The moraic-syllabification operations of [Hay89]: segment deletion strands a μ (an empty prosodic position), which is then re-licensed by re-association ([Ito86]'s Prosodic Licensing) or else erased. This is the mechanism of compensatory lengthening — "CL" the phenomenon is a composition of these operations, documented per-language in Studies/Hayes1989. Mora count is conserved by construction (the μ survives deletion).

def Prosody.Syllable.strand (σ : Syllable) (i : ℕ) : Syllable

Delete the segment under mora i, leaving the μ stranded (it survives, dominating nothing) — the engine of compensatory lengthening.

Equations

• σ.strand 0 = { onset := σ.onset, head := Prosody.Mora.stranded, tail := σ.tail }
• σ.strand i_2.succ = { onset := σ.onset, head := σ.head, tail := σ.tail.set i_2 Prosody.Mora.stranded }

def Prosody.Syllable.deleteOnset (σ : Syllable) (i : ℕ) : Syllable

Delete an onset segment. Onsets are non-moraic, so this strands no μ — the onset-deletion asymmetry: it cannot feed compensatory lengthening ([Hay89]).

Equations

• σ.deleteOnset i = { onset := σ.onset.eraseIdx i, head := σ.head, tail := σ.tail }

def Prosody.Syllable.strandedCount (σ : Syllable) : ℕ

The number of stranded (segmentally unaffiliated) morae.

Equations

• σ.strandedCount = List.countP (fun (μ : Prosody.Mora) => decide μ.IsStranded) σ.morae

def Prosody.Syllable.relicense (σ : Syllable) : Syllable

Tautosyllabic re-licensing ([Ito86]): re-associate σ's stranded morae to the nucleus, within σ. Length-preserving on the spine, so weight is conserved.

Equations

• σ.relicense = Prosody.Syllable.rebuild✝ σ (Prosody.Syllable.relink✝ [] σ.morae) ⋯

def Prosody.Syllable.relicenseLeft (host target : Syllable) : Syllable × Option Syllable

Heterosyllabic re-licensing (Parasitic Delinking, [Hay89]): a stranded nucleus μ delinks — the syllable, now nucleus-less, is deleted (none), and its μ migrates onto the preceding host's nucleus, lengthening it (the host vowel spans two morae). A no-op if the target's nucleus is not stranded.

Equations

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

Mora conservation, by construction.

theorem Prosody.Syllable.strand_moraCount (σ : Syllable) (i : ℕ) : (σ.strand i).moraCount = σ.moraCount

theorem Prosody.Syllable.deleteOnset_moraCount (σ : Syllable) (i : ℕ) : (σ.deleteOnset i).moraCount = σ.moraCount

theorem Prosody.Syllable.deleteOnset_strandedCount (σ : Syllable) (i : ℕ) : (σ.deleteOnset i).strandedCount = σ.strandedCount

The onset-deletion asymmetry ([Hay89]): deleting an onset strands no μ.

theorem Prosody.Syllable.relicense_moraCount (σ : Syllable) : σ.relicense.moraCount = σ.moraCount

theorem Prosody.Syllable.relicenseLeft_conserves (host target : Syllable) (h : target.head.IsStranded) (hmono : target.tail = []) : (host.relicenseLeft target).1.moraCount + (Option.map moraCount (host.relicenseLeft target).2).getD 0 = host.moraCount + target.moraCount

Heterosyllabic re-licensing conserves the total mora count across the boundary: the migrated μ leaves the (deleted) target and is gained by the host.

Onset-rime re-representation

structure Prosody.OnsetRime : Type

The onset-rime structure ([Sel82]): a rival theory of σ structure, an onset over a rime. Here a re-representation of the canonical moraic Syllable.

• onset : List Phonology.Segment

  The non-moraic onset melody.

• rime : List Mora

  The rime: the moraic spine.

@[implicit_reducible]

instance Prosody.instDecidableEqOnsetRime : DecidableEq OnsetRime

Equations

• Prosody.instDecidableEqOnsetRime = Prosody.instDecidableEqOnsetRime.decEq

def Prosody.instDecidableEqOnsetRime.decEq (x✝ x✝¹ : OnsetRime) : Decidable (x✝ = x✝¹)

Equations

• Prosody.instDecidableEqOnsetRime.decEq { onset := a, rime := a_1 } { onset := b, rime := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def Prosody.Syllable.toOnsetRime (σ : Syllable) : OnsetRime

σ → onset-rime: the rime is the moraic spine ([Sel82]).

Equations

• σ.toOnsetRime = { onset := σ.onset, rime := σ.morae }

theorem Prosody.Syllable.toOnsetRime_weight (σ : Syllable) : σ.toOnsetRime.rime.length = σ.moraCount

Weight correspondence: the onset-rime rime's mora count equals σ's weight — the moraic and onset-rime theories agree on weight ([Sel82]; [Hay89]).

Yield

@[reducible, inline]

abbrev Prosody.Yield : Type

A yield: the terminal σ-weight string of a prosodic structure — the unparsed input, or the leaves of a prosodic Tree. Distinct from the prosodic word ω (an IsWord tree), which is a headed constituent: a yield is just the weight profile, with no head and no constituency.

Equations

• Prosody.Yield = List Prosody.Syllable.Weight

def Prosody.Yield.ofSyllables (σs : List Syllable) : Yield

The weight profile of fully-moraified syllables — the σ → yield bridge.

Equations

• Prosody.Yield.ofSyllables σs = List.map Prosody.Syllable.weight σs

def Prosody.Yield.moraCount (y : Yield) : ℕ

Total mora count (each weight is a mora count).

Equations

• y.moraCount = List.sum y

@[reducible, inline]

abbrev Prosody.Yield.satisfiesMinWord (y : Yield) (minMorae : ℕ := 2) : Prop

The minimal-word size constraint ([McCP93]): at least minMorae morae (default 2, the moraic-trochee minimum) — the moraic size floor on a prosodic word. Whether an ω must structurally contain a foot is a separate, non-presupposed matter (footless languages have ω directly over σ, [Dol20]).

Equations

• y.satisfiesMinWord minMorae = (minMorae ≤ y.moraCount)

The prosodic-tree carrier

The recursive prosodic constituent ([IM03]): the Core ordered rose tree RoseTree labeled by prosodic-level Constituents — the violable OT candidate carrier for ω/φ/… structures, including the ill-formed ones (a footless ω, a stray under φ) that IsWord rules out. Its OT constraints are Constraints.Constraint Tree values, defined alongside IsWord. Homed here because Constituent.weight/.syl need Syllable.Weight; it inherits DecidableEq/map from RoseTree.

inductive Prosody.Constituent : Type

A prosodic node — the level is the constructor: a σ carries its mora weight and isHead, every non-root level carries isHead (whether it heads its parent). Constructor defaults match the former smart constructors, so node literals are unchanged; illegal nodes (a weight on a foot, a head on the ι root) are unrepresentable.

• syl (weight : Syllable.Weight := 0) (isHead : Bool := false) : Constituent

  A syllable of the given weight, optionally the head of its foot.

• ft (isHead : Bool := false) : Constituent

  A foot, optionally the head foot of its word.

• om (isHead : Bool := false) : Constituent

  A prosodic word ω, optionally the head word of its phrase.

• ph (isHead : Bool := false) : Constituent

  A phonological phrase φ, optionally the head phrase of its intonational phrase.

• iota : Constituent

  An intonational phrase ι — the root of the utterance-level hierarchy, headless.

@[implicit_reducible]

instance Prosody.instDecidableEqConstituent : DecidableEq Constituent

Equations

• Prosody.instDecidableEqConstituent = Prosody.instDecidableEqConstituent.decEq

def Prosody.instDecidableEqConstituent.decEq (x✝ x✝¹ : Constituent) : Decidable (x✝ = x✝¹)

Equations

• Prosody.instDecidableEqConstituent.decEq (Prosody.Constituent.syl a a_1) (Prosody.Constituent.syl b b_1) = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯
• Prosody.instDecidableEqConstituent.decEq (Prosody.Constituent.syl weight isHead) (Prosody.Constituent.ft isHead_1) = isFalse ⋯
• Prosody.instDecidableEqConstituent.decEq (Prosody.Constituent.syl weight isHead) (Prosody.Constituent.om isHead_1) = isFalse ⋯
• Prosody.instDecidableEqConstituent.decEq (Prosody.Constituent.syl weight isHead) (Prosody.Constituent.ph isHead_1) = isFalse ⋯
• Prosody.instDecidableEqConstituent.decEq (Prosody.Constituent.syl weight isHead) Prosody.Constituent.iota = isFalse ⋯
• Prosody.instDecidableEqConstituent.decEq (Prosody.Constituent.ft isHead) (Prosody.Constituent.syl weight isHead_1) = isFalse ⋯
• Prosody.instDecidableEqConstituent.decEq (Prosody.Constituent.ft a) (Prosody.Constituent.ft b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Prosody.instDecidableEqConstituent.decEq (Prosody.Constituent.ft isHead) (Prosody.Constituent.om isHead_1) = isFalse ⋯
• Prosody.instDecidableEqConstituent.decEq (Prosody.Constituent.ft isHead) (Prosody.Constituent.ph isHead_1) = isFalse ⋯
• Prosody.instDecidableEqConstituent.decEq (Prosody.Constituent.ft isHead) Prosody.Constituent.iota = isFalse ⋯
• Prosody.instDecidableEqConstituent.decEq (Prosody.Constituent.om isHead) (Prosody.Constituent.syl weight isHead_1) = isFalse ⋯
• Prosody.instDecidableEqConstituent.decEq (Prosody.Constituent.om isHead) (Prosody.Constituent.ft isHead_1) = isFalse ⋯
• Prosody.instDecidableEqConstituent.decEq (Prosody.Constituent.om a) (Prosody.Constituent.om b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Prosody.instDecidableEqConstituent.decEq (Prosody.Constituent.om isHead) (Prosody.Constituent.ph isHead_1) = isFalse ⋯
• Prosody.instDecidableEqConstituent.decEq (Prosody.Constituent.om isHead) Prosody.Constituent.iota = isFalse ⋯
• Prosody.instDecidableEqConstituent.decEq (Prosody.Constituent.ph isHead) (Prosody.Constituent.syl weight isHead_1) = isFalse ⋯
• Prosody.instDecidableEqConstituent.decEq (Prosody.Constituent.ph isHead) (Prosody.Constituent.ft isHead_1) = isFalse ⋯
• Prosody.instDecidableEqConstituent.decEq (Prosody.Constituent.ph isHead) (Prosody.Constituent.om isHead_1) = isFalse ⋯
• Prosody.instDecidableEqConstituent.decEq (Prosody.Constituent.ph a) (Prosody.Constituent.ph b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Prosody.instDecidableEqConstituent.decEq (Prosody.Constituent.ph isHead) Prosody.Constituent.iota = isFalse ⋯
• Prosody.instDecidableEqConstituent.decEq Prosody.Constituent.iota (Prosody.Constituent.syl weight isHead) = isFalse ⋯
• Prosody.instDecidableEqConstituent.decEq Prosody.Constituent.iota (Prosody.Constituent.ft isHead) = isFalse ⋯
• Prosody.instDecidableEqConstituent.decEq Prosody.Constituent.iota (Prosody.Constituent.om isHead) = isFalse ⋯
• Prosody.instDecidableEqConstituent.decEq Prosody.Constituent.iota (Prosody.Constituent.ph isHead) = isFalse ⋯
• Prosody.instDecidableEqConstituent.decEq Prosody.Constituent.iota Prosody.Constituent.iota = isTrue ⋯

@[implicit_reducible]

instance Prosody.instReprConstituent : Repr Constituent

Equations

• Prosody.instReprConstituent = { reprPrec := Prosody.instReprConstituent.repr }

def Prosody.instReprConstituent.repr : Constituent → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Prosody.instReprConstituent.repr Prosody.Constituent.iota prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Prosody.Constituent.iota")).group prec✝

def Prosody.Constituent.isHead : Constituent → Bool

Whether a node heads its parent (a σ heads its foot, a foot heads its word, an ω its phrase, a φ its intonational phrase); false for the ι root.

Equations

• (Prosody.Constituent.syl a a_1).isHead = a_1
• (Prosody.Constituent.ft a).isHead = a
• (Prosody.Constituent.om a).isHead = a
• (Prosody.Constituent.ph a).isHead = a
• Prosody.Constituent.iota.isHead = false

def Prosody.Constituent.weight? : Constituent → Option Syllable.Weight

The mora weight of a σ node; none for non-σ nodes.

Equations

• (Prosody.Constituent.syl w isHead).weight? = some w
• x✝.weight? = none

def Prosody.Constituent.isSyl : Constituent → Bool

A syllable (σ) node.

Equations

• (Prosody.Constituent.syl w isHead).isSyl = true
• x✝.isSyl = false

def Prosody.Constituent.isFt : Constituent → Bool

A foot (f) node.

Equations

• (Prosody.Constituent.ft isHead).isFt = true
• x✝.isFt = false

def Prosody.Constituent.isOm : Constituent → Bool

A prosodic-word (ω) node.

Equations

• (Prosody.Constituent.om isHead).isOm = true
• x✝.isOm = false

def Prosody.Constituent.isPh : Constituent → Bool

A phonological-phrase (φ) node.

Equations

• (Prosody.Constituent.ph isHead).isPh = true
• x✝.isPh = false

def Prosody.Constituent.isIota : Constituent → Bool

An intonational-phrase (ι) node.

Equations

• Prosody.Constituent.iota.isIota = true
• x✝.isIota = false

def Prosody.Constituent.sameLevel : Constituent → Constituent → Bool

Two nodes at the same prosodic level (the same constructor, ignoring weight/head) — the same-category test the No-Recursion family reads off the carrier.

Equations

• (Prosody.Constituent.syl weight isHead).sameLevel (Prosody.Constituent.syl weight_1 isHead_1) = true
• (Prosody.Constituent.ft isHead).sameLevel (Prosody.Constituent.ft isHead_1) = true
• (Prosody.Constituent.om isHead).sameLevel (Prosody.Constituent.om isHead_1) = true
• (Prosody.Constituent.ph isHead).sameLevel (Prosody.Constituent.ph isHead_1) = true
• Prosody.Constituent.iota.sameLevel Prosody.Constituent.iota = true
• x✝¹.sameLevel x✝ = false

theorem Prosody.Constituent.isSyl_eq_false_of_isFt {x : Constituent} (h : x.isFt = true) : x.isSyl = false

The level family is exclusive: a foot is not a syllable.

theorem Prosody.Constituent.isSyl_eq_false_of_isOm {x : Constituent} (h : x.isOm = true) : x.isSyl = false

The level family is exclusive: a prosodic word is not a syllable.

@[reducible, inline]

abbrev Prosody.Tree : Type

A prosodic tree: the Core ordered rose tree RoseTree labeled by Constituents. Ordered children give No-Tangling by construction.

Equations

• Prosody.Tree = RoseTree Prosody.Constituent

@[reducible, inline]

abbrev Prosody.Tree.σ (w : Syllable.Weight := 0) (h : Bool := false) : Tree

A σ-leaf — the metrical terminal: a syllable of weight w, head-marked h.

Equations

• Prosody.Tree.σ w h = RoseTree.node (Prosody.Constituent.syl w h) []

@[reducible, inline]

abbrev Prosody.Tree.ft (h : Bool) (cs : List Tree) : Tree

A foot node over cs, optionally the head foot of its word.

Equations

• Prosody.Tree.ft h cs = RoseTree.node (Prosody.Constituent.ft h) cs

@[reducible, inline]

abbrev Prosody.Tree.om (cs : List Tree) : Tree

A prosodic-word (ω) node over cs.

Equations

• Prosody.Tree.om cs = RoseTree.node Prosody.Constituent.om cs

@[reducible, inline]

abbrev Prosody.Tree.ph (cs : List Tree) : Tree

A phonological-phrase (φ) node over cs — interim, until Prosody.Phrase lands.

Equations

• Prosody.Tree.ph cs = RoseTree.node Prosody.Constituent.ph cs

theorem Prosody.Tree.recLeafBranch {motive : Tree → Prop} (leaf : ∀ (a : Constituent), a.isSyl = true → motive (RoseTree.node a [])) (branch : ∀ (a : Constituent) (cs : List Tree), ¬(a.isSyl = true ∧ cs = []) → (∀ c ∈ cs, motive c) → motive (RoseTree.node a cs)) (t : Tree) : motive t

Leaf/branch induction on a prosodic tree. A σ-leaf is a base case; every other node — a foot, word, phrase, or degenerate/ill-formed node — is a branch, carrying the induction hypothesis over its children and the fact that it is not a σ-leaf. This is what lets proofs reduce the σ-leaf if the reader equations carry (via if_pos ⟨ha, rfl⟩ / if_neg hne) instead of splitting it.