Syllable Structure

Syllable constituency (onset–nucleus–coda), sonority scale, the Sonority Sequencing Principle, moraic weight, and OT markedness constraints.

Source: @cite{goldsmith-2011} "The Syllable" in The Handbook of Phonological Theory (Ch 6, pp. 164–196). Cross-referenced with Hayes §4.6 and §15.

@cite{goldsmith-2011}

def Theories.Phonology.Syllable.sonorityOf (s : Segment) : Nat

Sonority rank (0 = least sonorous). Following @cite{hayes-2009}, the 5-level hierarchy is decomposed by four features:

Class	son	approx	cons	syll	Rank
Obstruent	−	−	+	−	0
Nasal	+	−	+	−	1
Liquid	+	+	+	−	2
Glide	+	+	−	−	3
Vowel	+	+	−	+	4

Within obstruents, [±continuant] further splits stops (rank 0) from fricatives (rank 1) per @cite{clements-1990}, yielding a 6-level scale.

Equations

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

structure Theories.Phonology.Syllable.Syllable : Type

A syllable: onset, nucleus, coda. The rhyme (nucleus ++ coda) groups naturally in phonological processes.

• onset : List Segment
• nucleus : List Segment
• coda : List Segment

def Theories.Phonology.Syllable.Syllable.rhyme (σ : Syllable) : List Segment

The rhyme (rime): nucleus + coda.

Equations

• σ.rhyme = σ.nucleus ++ σ.coda

def Theories.Phonology.Syllable.Syllable.segments (σ : Syllable) : List Segment

All segments in linear order.

Equations

• σ.segments = σ.onset ++ σ.nucleus ++ σ.coda

def Theories.Phonology.Syllable.Syllable.hasOnset (σ : Syllable) : Bool

Equations

• σ.hasOnset = !σ.onset.isEmpty

def Theories.Phonology.Syllable.Syllable.hasCoda (σ : Syllable) : Bool

Equations

• σ.hasCoda = !σ.coda.isEmpty

def Theories.Phonology.Syllable.Syllable.isOpen (σ : Syllable) : Bool

Equations

• σ.isOpen = σ.coda.isEmpty

def Theories.Phonology.Syllable.Syllable.isClosed (σ : Syllable) : Bool

Equations

• σ.isClosed = !σ.coda.isEmpty

def Theories.Phonology.Syllable.monotoneRising : List Nat → Bool

Is a list of Nats monotonically non-decreasing?

Equations

• Theories.Phonology.Syllable.monotoneRising [] = true
• Theories.Phonology.Syllable.monotoneRising [head] = true
• Theories.Phonology.Syllable.monotoneRising (a :: b :: rest) = (decide (a ≤ b) && Theories.Phonology.Syllable.monotoneRising (b :: rest))

def Theories.Phonology.Syllable.monotoneFalling : List Nat → Bool

Is a list of Nats monotonically non-increasing?

Equations

• Theories.Phonology.Syllable.monotoneFalling [] = true
• Theories.Phonology.Syllable.monotoneFalling [head] = true
• Theories.Phonology.Syllable.monotoneFalling (a :: b :: rest) = (decide (a ≥ b) && Theories.Phonology.Syllable.monotoneFalling (b :: rest))

def Theories.Phonology.Syllable.Syllable.sspOnset (σ : Syllable) : Bool

Does the onset obey SSP? Sonority rises toward the nucleus.

Equations

• σ.sspOnset = Theories.Phonology.Syllable.monotoneRising (List.map Theories.Phonology.Syllable.sonorityOf σ.onset)

def Theories.Phonology.Syllable.Syllable.sspCoda (σ : Syllable) : Bool

Does the coda obey SSP? Sonority falls from the nucleus.

Equations

• σ.sspCoda = Theories.Phonology.Syllable.monotoneFalling (List.map Theories.Phonology.Syllable.sonorityOf σ.coda)

def Theories.Phonology.Syllable.Syllable.sspValid (σ : Syllable) : Bool

Full SSP: onset rises, coda falls.

Equations

• σ.sspValid = (σ.sspOnset && σ.sspCoda)

structure Theories.Phonology.Syllable.SyllabifiedForm : Type

A syllabified form: a word parsed into syllables.

• syllables : List Syllable

def Theories.Phonology.Syllable.SyllabifiedForm.segmentCount (sf : SyllabifiedForm) : Nat

Total segment count.

Equations

• sf.segmentCount = List.foldl (fun (x1 : Nat) (x2 : Theories.Phonology.Syllable.Syllable) => x1 + x2.segments.length) 0 sf.syllables

def Theories.Phonology.Syllable.SyllabifiedForm.allSegments (sf : SyllabifiedForm) : List Segment

All segments in linear order.

Equations

• sf.allSegments = List.flatMap Theories.Phonology.Syllable.Syllable.segments sf.syllables

inductive Theories.Phonology.Syllable.SyllWeight : Type

Syllable weight classes.

• light : SyllWeight
• heavy : SyllWeight
• superheavy : SyllWeight

instance Theories.Phonology.Syllable.instDecidableEqSyllWeight : DecidableEq SyllWeight

Equations

• Theories.Phonology.Syllable.instDecidableEqSyllWeight x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Theories.Phonology.Syllable.instBEqSyllWeight.beq : SyllWeight → SyllWeight → Bool

Equations

• Theories.Phonology.Syllable.instBEqSyllWeight.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Theories.Phonology.Syllable.instBEqSyllWeight : BEq SyllWeight

Equations

• Theories.Phonology.Syllable.instBEqSyllWeight = { beq := Theories.Phonology.Syllable.instBEqSyllWeight.beq }

def Theories.Phonology.Syllable.instReprSyllWeight.repr : SyllWeight → Nat → Std.Format

Equations

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

instance Theories.Phonology.Syllable.instReprSyllWeight : Repr SyllWeight

Equations

• Theories.Phonology.Syllable.instReprSyllWeight = { reprPrec := Theories.Phonology.Syllable.instReprSyllWeight.repr }

def Theories.Phonology.Syllable.Syllable.moraCount (σ : Syllable) (codaMoraic : Bool := true) : Nat

Mora count. codaMoraic = true means coda consonants contribute weight (the "Weight-by-Position" parameter of @cite{hayes-1989}).

Equations

• σ.moraCount codaMoraic = σ.nucleus.length + if codaMoraic = true then σ.coda.length else 0

def Theories.Phonology.Syllable.Syllable.weight (σ : Syllable) (codaMoraic : Bool := true) : SyllWeight

Weight classification from mora count.

Equations

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

def Theories.Phonology.Syllable.onsetViolations (sf : SyllabifiedForm) : Nat

ONSET: every syllable must have an onset. Returns count of onsetless syllables.

Equations

• Theories.Phonology.Syllable.onsetViolations sf = (List.filter (fun (σ : Theories.Phonology.Syllable.Syllable) => !σ.hasOnset) sf.syllables).length

def Theories.Phonology.Syllable.noCodaViolations (sf : SyllabifiedForm) : Nat

NOCODA: syllables should not have codas. Returns count of syllables with codas.

Equations

• Theories.Phonology.Syllable.noCodaViolations sf = (List.filter Theories.Phonology.Syllable.Syllable.hasCoda sf.syllables).length

def Theories.Phonology.Syllable.complexOnsetViolations (sf : SyllabifiedForm) : Nat

*COMPLEXONSET: no complex (multi-segment) onsets. Returns count of syllables with onset length > 1.

Equations

• Theories.Phonology.Syllable.complexOnsetViolations sf = (List.filter (fun (σ : Theories.Phonology.Syllable.Syllable) => decide (σ.onset.length > 1)) sf.syllables).length

def Theories.Phonology.Syllable.complexCodaViolations (sf : SyllabifiedForm) : Nat

*COMPLEXCODA: no complex (multi-segment) codas. Returns count of syllables with coda length > 1.

Equations

• Theories.Phonology.Syllable.complexCodaViolations sf = (List.filter (fun (σ : Theories.Phonology.Syllable.Syllable) => decide (σ.coda.length > 1)) sf.syllables).length

def Theories.Phonology.Syllable.sspViolations (sf : SyllabifiedForm) : Nat

SSP: every syllable obeys the Sonority Sequencing Principle. Returns count of syllables violating SSP.

Equations

• Theories.Phonology.Syllable.sspViolations sf = (List.filter (fun (σ : Theories.Phonology.Syllable.Syllable) => !σ.sspValid) sf.syllables).length

theorem Theories.Phonology.Syllable.monotoneRising_singleton (n : Nat) : monotoneRising [n] = true

theorem Theories.Phonology.Syllable.monotoneFalling_singleton (n : Nat) : monotoneFalling [n] = true

theorem Theories.Phonology.Syllable.cv_is_light (σ : Syllable) (h1 : σ.nucleus.length = 1) (h2 : σ.coda = []) : σ.weight = SyllWeight.light

theorem Theories.Phonology.Syllable.cvc_is_heavy (σ : Syllable) (h1 : σ.nucleus.length = 1) (h2 : σ.coda.length = 1) : σ.weight = SyllWeight.heavy