Features.Prosody

@cite{pierrehumbert-1980} @cite{beckman-pierrehumbert-1986}

Theory-neutral prosodic types: pitch accents, phrase accents, boundary tones, and the prosodic hierarchy, following the autosegmental-metrical (AM) framework established by @cite{pierrehumbert-1980} for English and extended cross-linguistically by @cite{beckman-pierrehumbert-1986}.

@cite{steedman-2000} uses these types to connect prosodic structure to CCG derivations and information structure.

Overview

These types are used across multiple theories:

• CCG/Intonation: prosodic CCG derivations
• Information Structure: spellout constraints
• Focus theory: prosodic realization of focus/givenness
• Autosegmental phonology: tone and register systems

inductive Features.Prosody.PitchAccent : Type

Pitch accent types (@cite{pierrehumbert-1980}, ToBI conventions).

The full inventory of English pitch accents. A starred tone (*) is phonologically linked to the stressed syllable; an unstarred tone in a bitonal accent precedes or follows it at some given space in time.

@cite{pierrehumbert-1980} identified seven possible pitch accent shapes; the H*+H accent was eliminated as a possible pattern, leaving six (@cite{beckman-pierrehumbert-1986} §2.1).

In Japanese, by contrast, the single possible pitch accent shape is a lexically linked H, analyzed as H*+L. The accent location is lexically distinctive, but the shape is fixed. English uses the full inventory to contrast different intonational meanings (e.g., declarative vs. surprise-redundancy vs. impatient reassertion on the same word orange in an orange ballgown; @cite{beckman-pierrehumbert-1986} Fig. 1).

• H_star : PitchAccent
• L_star : PitchAccent
• H_star_plus_L : PitchAccent
• H_plus_L_star : PitchAccent
• L_star_plus_H : PitchAccent
• L_plus_H_star : PitchAccent
• null : PitchAccent

def Features.Prosody.instReprPitchAccent.repr : PitchAccent → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Features.Prosody.instReprPitchAccent : Repr PitchAccent

Equations

• Features.Prosody.instReprPitchAccent = { reprPrec := Features.Prosody.instReprPitchAccent.repr }

@[implicit_reducible]

instance Features.Prosody.instDecidableEqPitchAccent : DecidableEq PitchAccent

Equations

• Features.Prosody.instDecidableEqPitchAccent x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Features.Prosody.instInhabitedPitchAccent : Inhabited PitchAccent

Equations

• Features.Prosody.instInhabitedPitchAccent = { default := Features.Prosody.instInhabitedPitchAccent.default }

def Features.Prosody.instInhabitedPitchAccent.default : PitchAccent

Equations

• Features.Prosody.instInhabitedPitchAccent.default = Features.Prosody.PitchAccent.H_star

def Features.Prosody.PitchAccent.isBitonal : PitchAccent → Bool

Is this a bitonal accent (two tones)? Bitonal accents trigger catathesis (@cite{beckman-pierrehumbert-1986} §3.2).

Equations

• Features.Prosody.PitchAccent.H_star_plus_L.isBitonal = true
• Features.Prosody.PitchAccent.H_plus_L_star.isBitonal = true
• Features.Prosody.PitchAccent.L_star_plus_H.isBitonal = true
• Features.Prosody.PitchAccent.L_plus_H_star.isBitonal = true
• x✝.isBitonal = false

inductive Features.Prosody.PhraseAccent : Type

Phrase accent: terminal tone of the intermediate phrase.

@cite{beckman-pierrehumbert-1986} §4.2–4.3 decompose what @cite{pierrehumbert-1980} called the "phrase accent" into a tone that spreads from the last pitch accent to the edge of the intermediate phrase. The phrase accent is H or L, independent of the boundary tone.

In Japanese, the accentual phrase boundary L is always L; the only variation is whether an optional H boundary tone follows at the intonation phrase edge.

• H : PhraseAccent
• L : PhraseAccent

def Features.Prosody.instReprPhraseAccent.repr : PhraseAccent → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Features.Prosody.instReprPhraseAccent : Repr PhraseAccent

Equations

• Features.Prosody.instReprPhraseAccent = { reprPrec := Features.Prosody.instReprPhraseAccent.repr }

@[implicit_reducible]

instance Features.Prosody.instDecidableEqPhraseAccent : DecidableEq PhraseAccent

Equations

• Features.Prosody.instDecidableEqPhraseAccent x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Features.Prosody.instInhabitedPhraseAccent : Inhabited PhraseAccent

Equations

• Features.Prosody.instInhabitedPhraseAccent = { default := Features.Prosody.instInhabitedPhraseAccent.default }

def Features.Prosody.instInhabitedPhraseAccent.default : PhraseAccent

Equations

• Features.Prosody.instInhabitedPhraseAccent.default = Features.Prosody.PhraseAccent.H

inductive Features.Prosody.BoundaryTone : Type

Boundary tone: terminal tone of the intonation phrase.

@cite{beckman-pierrehumbert-1986} distinguish the boundary tone (edge of the intonation phrase) from the phrase accent (edge of the intermediate phrase). Together, the phrase accent and boundary tone produce four terminal configurations: LL%, LH%, HL%, HH%.

In Japanese, the boundary tone at an intonation phrase edge is always L except in yes/no questions, where H is optional (@cite{beckman-pierrehumbert-1986} §4.2).

• L_pct : BoundaryTone
• H_pct : BoundaryTone

@[implicit_reducible]

instance Features.Prosody.instReprBoundaryTone : Repr BoundaryTone

Equations

• Features.Prosody.instReprBoundaryTone = { reprPrec := Features.Prosody.instReprBoundaryTone.repr }

def Features.Prosody.instReprBoundaryTone.repr : BoundaryTone → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Features.Prosody.instDecidableEqBoundaryTone : DecidableEq BoundaryTone

Equations

• Features.Prosody.instDecidableEqBoundaryTone x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Features.Prosody.instInhabitedBoundaryTone : Inhabited BoundaryTone

Equations

• Features.Prosody.instInhabitedBoundaryTone = { default := Features.Prosody.instInhabitedBoundaryTone.default }

def Features.Prosody.instInhabitedBoundaryTone.default : BoundaryTone

Equations

• Features.Prosody.instInhabitedBoundaryTone.default = Features.Prosody.BoundaryTone.L_pct

structure Features.Prosody.TerminalContour : Type

Full terminal contour of an intonation phrase: phrase accent + boundary tone. @cite{pierrehumbert-1980}: four possible combinations.

• phraseAccent : PhraseAccent
• boundaryTone : BoundaryTone

def Features.Prosody.instReprTerminalContour.repr : TerminalContour → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Features.Prosody.instReprTerminalContour : Repr TerminalContour

Equations

• Features.Prosody.instReprTerminalContour = { reprPrec := Features.Prosody.instReprTerminalContour.repr }

@[implicit_reducible]

instance Features.Prosody.instDecidableEqTerminalContour : DecidableEq TerminalContour

Equations

• Features.Prosody.instDecidableEqTerminalContour = Features.Prosody.instDecidableEqTerminalContour.decEq

def Features.Prosody.instDecidableEqTerminalContour.decEq (x✝ x✝¹ : TerminalContour) : Decidable (x✝ = x✝¹)

Equations

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

def Features.Prosody.TerminalContour.declarative : TerminalContour

Standard declarative terminal: L L%

Equations

• Features.Prosody.TerminalContour.declarative = { phraseAccent := Features.Prosody.PhraseAccent.L, boundaryTone := Features.Prosody.BoundaryTone.L_pct }

def Features.Prosody.TerminalContour.continuation : TerminalContour

Continuation rise terminal: L H% (theme boundary)

Equations

• Features.Prosody.TerminalContour.continuation = { phraseAccent := Features.Prosody.PhraseAccent.L, boundaryTone := Features.Prosody.BoundaryTone.H_pct }

def Features.Prosody.TerminalContour.ynQuestion : TerminalContour

Yes/no question terminal: H H%

Equations

• Features.Prosody.TerminalContour.ynQuestion = { phraseAccent := Features.Prosody.PhraseAccent.H, boundaryTone := Features.Prosody.BoundaryTone.H_pct }

def Features.Prosody.TerminalContour.calling : TerminalContour

Calling contour / plateau terminal: H L%

Equations

• Features.Prosody.TerminalContour.calling = { phraseAccent := Features.Prosody.PhraseAccent.H, boundaryTone := Features.Prosody.BoundaryTone.L_pct }

inductive Features.Prosody.ProsodicLevel : Type

Prosodic hierarchy levels.

σ < f < ω < AP < φ < ι

@cite{beckman-pierrehumbert-1986} establish the accentual phrase (AP) as the domain of pitch accent distribution (at most one accent per AP, §2.2) and the phonological phrase (φ, equivalent to the intermediate phrase / ip in ToBI notation) as the domain of catathesis (§3–4).

Used by @cite{kratzer-selkirk-2020} spellout constraints.

• σ : ProsodicLevel
• f : ProsodicLevel
• ω : ProsodicLevel
• AP : ProsodicLevel
• φ : ProsodicLevel
• ι : ProsodicLevel

@[implicit_reducible]

instance Features.Prosody.instDecidableEqProsodicLevel : DecidableEq ProsodicLevel

Equations

• Features.Prosody.instDecidableEqProsodicLevel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Features.Prosody.instReprProsodicLevel : Repr ProsodicLevel

Equations

• Features.Prosody.instReprProsodicLevel = { reprPrec := Features.Prosody.instReprProsodicLevel.repr }

def Features.Prosody.instReprProsodicLevel.repr : ProsodicLevel → ℕ → Std.Format

Equations

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

def Features.Prosody.ProsodicLevel.toNat : ProsodicLevel → ℕ

Numeric encoding for the prosodic hierarchy ordering.

Equations

• Features.Prosody.ProsodicLevel.σ.toNat = 0
• Features.Prosody.ProsodicLevel.f.toNat = 1
• Features.Prosody.ProsodicLevel.ω.toNat = 2
• Features.Prosody.ProsodicLevel.AP.toNat = 3
• Features.Prosody.ProsodicLevel.φ.toNat = 4
• Features.Prosody.ProsodicLevel.ι.toNat = 5

@[implicit_reducible]

instance Features.Prosody.instLinearOrderProsodicLevel : LinearOrder ProsodicLevel

Equations

• Features.Prosody.instLinearOrderProsodicLevel = LinearOrder.lift' Features.Prosody.ProsodicLevel.toNat Features.Prosody.instLinearOrderProsodicLevel._proof_1

structure Features.Prosody.ProsodicConstituent : Type

Head-prominence: each prosodic constituent has exactly one prominent daughter (its head). K&S (32).

• level : ProsodicLevel
• isHead : Bool

  Whether this constituent is the head (most prominent) of its parent

@[implicit_reducible]

instance Features.Prosody.instReprProsodicConstituent : Repr ProsodicConstituent

Equations

• Features.Prosody.instReprProsodicConstituent = { reprPrec := Features.Prosody.instReprProsodicConstituent.repr }

def Features.Prosody.instReprProsodicConstituent.repr : ProsodicConstituent → ℕ → Std.Format

Equations

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

inductive Features.Prosody.AccentSpecification : Type

How pitch accents relate to the lexicon (@cite{beckman-pierrehumbert-1986} §2.5).

• lexical: accent location specified in lexicon, shape fixed. Japanese: H*+L at lexically specified mora. Swedish: accent 1 vs 2. The accent shape cannot signal different intonational meanings.
• postlexical: accent shape chosen by intonation, location by prominence. English: 6 pitch accent shapes, location determined by focus/stress. The shape contrasts different intonational meanings (declarative, surprise, impatience, etc.).

• lexical : AccentSpecification
• postlexical : AccentSpecification

@[implicit_reducible]

instance Features.Prosody.instReprAccentSpecification : Repr AccentSpecification

Equations

• Features.Prosody.instReprAccentSpecification = { reprPrec := Features.Prosody.instReprAccentSpecification.repr }

def Features.Prosody.instReprAccentSpecification.repr : AccentSpecification → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Features.Prosody.instDecidableEqAccentSpecification : DecidableEq AccentSpecification

Equations

• Features.Prosody.instDecidableEqAccentSpecification x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Features.Prosody.ProsodicDominance : Type

How a morpheme interacts with the prosodic specification of its base. @cite{kiparsky-halle-1977} @cite{rolle-2018}

Orthogonal to AccentSpecification, which classifies word-level accent determination (how is the accent location decided?). ProsodicDominance classifies morpheme-level prosodic interaction (does this morpheme override the base's accent/tone, or respect it?).

The dominant/recessive distinction originates in the accentual morpheme classes of @cite{kiparsky-halle-1977} (deaccenting vs non-deaccenting suffixes in IE) and was generalized to tonal morphology by @cite{rolle-2018} as the GT dominance typology.

• dominant: overrides the prosodic specification of the base. Accent: Japanese -teki removes stem accent (@cite{kawahara-2015}). Tone: Mwaghavul verbalisers replace base melody (@cite{akinbo-fwangwar-2026}).
• recessive: applies only when the base is prosodically unmarked. Accent: Japanese -si 'Mr.' preserves stem accent. Tone: Giphende floating tones dock only to unvalued TBUs.
• neutral: concatenates without prosodic interaction; the general phonological grammar determines the output. Tone: Hausa referential -ⁿn (@cite{rolle-2018}).

• dominant : ProsodicDominance
• recessive : ProsodicDominance
• neutral : ProsodicDominance

@[implicit_reducible]

instance Features.Prosody.instReprProsodicDominance : Repr ProsodicDominance

Equations

• Features.Prosody.instReprProsodicDominance = { reprPrec := Features.Prosody.instReprProsodicDominance.repr }

def Features.Prosody.instReprProsodicDominance.repr : ProsodicDominance → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Features.Prosody.instDecidableEqProsodicDominance : DecidableEq ProsodicDominance

Equations

• Features.Prosody.instDecidableEqProsodicDominance x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Features.Prosody.ProsodicDominance.IsDominant (d : ProsodicDominance) : Prop

Dominant morphemes override the prosodic specification of their base.

Equations

• d.IsDominant = (d = Features.Prosody.ProsodicDominance.dominant)

@[implicit_reducible]

instance Features.Prosody.instDecidablePredProsodicDominanceIsDominant : DecidablePred ProsodicDominance.IsDominant

Equations

• Features.Prosody.instDecidablePredProsodicDominanceIsDominant x✝ = Features.Prosody.instDecidablePredProsodicDominanceIsDominant._aux_1 x✝

def Features.Prosody.ProsodicDominance.combineAccent (baseAccent : Option ℕ) : ProsodicDominance → Option ℕ

Combine a base accent with a suffix's prosodic dominance.

The accent position (Option Nat) represents a mora- or syllable-indexed accent; none = unaccented.

• dominant: accent is removed regardless of input.
• recessive / neutral: base accent is preserved.

Equations

• Features.Prosody.ProsodicDominance.combineAccent baseAccent Features.Prosody.ProsodicDominance.dominant = none
• Features.Prosody.ProsodicDominance.combineAccent baseAccent Features.Prosody.ProsodicDominance.recessive = baseAccent
• Features.Prosody.ProsodicDominance.combineAccent baseAccent Features.Prosody.ProsodicDominance.neutral = baseAccent

theorem Features.Prosody.ProsodicDominance.dominant_neutralizes (a₁ a₂ : Option ℕ) : combineAccent a₁ dominant = combineAccent a₂ dominant

Transparadigmatic uniformity (@cite{rolle-2018}): dominant morphemes produce the same output regardless of whether the base is accented or unaccented. This is the defining property of dominance — it neutralizes the base contrast.

theorem Features.Prosody.ProsodicDominance.recessive_preserves (a : Option ℕ) : combineAccent a recessive = a

Recessive morphemes preserve the base contrast: an accented base stays accented, an unaccented base stays unaccented.

inductive Features.Prosody.AffixAccentType : Type

Fine-grained affix accent classification (@cite{kawahara-2015} §6).

The 3-way ProsodicDominance (dominant/recessive/neutral) captures only one axis of morpheme–accent interaction. @cite{kawahara-2015}, building on @cite{poser-1984} and @cite{vance-1987}, identifies eight distinct affix accent behaviors in Japanese, differing in whether the affix carries its own accent, whether it deletes or preserves root accent, and whether it inserts a new accent at a particular position.

toProsodicDominance projects back to the coarser 3-way classification: types that preserve root accent when present map to recessive; types that override root accent map to dominant.

• recessive : AffixAccentType

  Suffix bears accent; loses to root accent when root is accented. E.g., Japanese -tara (conditional): accented root → root accent preserved; unaccented root → suffix accent surfaces.

• dominant : AffixAccentType

  Suffix bears accent; always overrides root accent. E.g., Japanese -ppoi (-ish): root accent deleted, suffix accent surfaces regardless.

• recessivePreAccent : AffixAccentType

  No own accent; inserts accent on root-final syllable only when root is unaccented. Preserves root accent when present. E.g., Japanese -si (Mr.): ono → ono'+si; u'ra → u'ra+si.

• dominantPreAccent : AffixAccentType

  No own accent; always inserts accent on root-final syllable, deleting root accent. E.g., Japanese -ke (family of): ono → ono'+ke; mu'raki → muraki'+ke.

• accentShifting : AffixAccentType

  No own accent; shifts existing root accent to pre-suffix position. Unaccented roots remain unaccented. E.g., Japanese -mono (thing): ka'k(+u) → kaki'+mono; nor(+u) → nori+mono.

• postAccenting : AffixAccentType

  Inserts accent immediately after the affix (typically a prefix). E.g., Japanese o- (honorific): huro' → o+hu'ro.

• deaccenting : AffixAccentType

  No own accent; deletes root accent. Output is unaccented. E.g., Japanese -teki (的 -like): ke'izai → keizai+teki.

• initialAccenting : AffixAccentType

  No own accent; inserts accent on root-initial syllable. E.g., Japanese -zu (group/plural): okamoto → o'kamoto+zu.

@[implicit_reducible]

instance Features.Prosody.instDecidableEqAffixAccentType : DecidableEq AffixAccentType

Equations

• Features.Prosody.instDecidableEqAffixAccentType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Features.Prosody.instReprAffixAccentType : Repr AffixAccentType

Equations

• Features.Prosody.instReprAffixAccentType = { reprPrec := Features.Prosody.instReprAffixAccentType.repr }

def Features.Prosody.instReprAffixAccentType.repr : AffixAccentType → ℕ → Std.Format

Equations

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

def Features.Prosody.AffixAccentType.toProsodicDominance : AffixAccentType → ProsodicDominance

Project the fine-grained 8-way classification to the coarser 3-way ProsodicDominance. Types that preserve root accent when present map to recessive; types that override it map to dominant.

Equations

• Features.Prosody.AffixAccentType.recessive.toProsodicDominance = Features.Prosody.ProsodicDominance.recessive
• Features.Prosody.AffixAccentType.recessivePreAccent.toProsodicDominance = Features.Prosody.ProsodicDominance.recessive
• Features.Prosody.AffixAccentType.accentShifting.toProsodicDominance = Features.Prosody.ProsodicDominance.recessive
• Features.Prosody.AffixAccentType.dominant.toProsodicDominance = Features.Prosody.ProsodicDominance.dominant
• Features.Prosody.AffixAccentType.dominantPreAccent.toProsodicDominance = Features.Prosody.ProsodicDominance.dominant
• Features.Prosody.AffixAccentType.postAccenting.toProsodicDominance = Features.Prosody.ProsodicDominance.dominant
• Features.Prosody.AffixAccentType.deaccenting.toProsodicDominance = Features.Prosody.ProsodicDominance.dominant
• Features.Prosody.AffixAccentType.initialAccenting.toProsodicDominance = Features.Prosody.ProsodicDominance.dominant

theorem Features.Prosody.AffixAccentType.recessive_preserves_root : recessive.toProsodicDominance = ProsodicDominance.recessive

All recessive-class affixes preserve root accent when present.

theorem Features.Prosody.AffixAccentType.dominant_overrides_root : dominant.toProsodicDominance = ProsodicDominance.dominant

All dominant-class affixes override root accent.

theorem Features.Prosody.AffixAccentType.deaccenting_is_dominant : deaccenting.toProsodicDominance = ProsodicDominance.dominant

Deaccenting is a special case of dominance (overrides root accent).