Beckman and Pierrehumbert (1986): Intonational structure in Japanese and English

[BP86] give Japanese and English one sparse-tone prosodic hierarchy: pitch accents group into accentual phrases with at most one accent each, accentual phrases into intermediate phrases, and those into intonation phrases, the phrase accent of [Pie80] becoming the terminal tone of the intermediate phrase and the boundary tone that of the intonation phrase. In both languages a bitonal accent triggers catathesis, the compression of the pitch range for everything that follows within the intermediate phrase, so chained accents descend a staircase and a phrase boundary resets the register; an unaccented phrase's phrasal H and boundary L do not trigger it, which separates catathesis from African downdrift. Both languages fix the accent's location in the lexicon; they differ in where its shape comes from, a lexically linked H*+L in Japanese against a choice made by the intonation system in English, in the inventory of shapes, one against six, and in whether the compression takes effect within the accent or after it. Final lowering and declination act above the intermediate phrase and are not catathesis.

Implementation notes

Catathesis is register downstep on the tonal register tier: each bitonal accent contributes a downstep node and Tone.realizePitch realizes the sequence as the running sum, so the staircase, the boundary reset, and the comparison with an unbroken chain are theorems of the register substrate rather than numbers read off figures. The Japanese accentual phrase is built from the prosodic fragment's word entries.

References

• [BP86]
• [Pie80]

Accentual phrases and catathesis

structure BeckmanPierrehumbert1986.AccentualPhrase : Type

An accentual phrase: the lowest level of the hierarchy, carrying at most one pitch accent (none when unaccented).

• accent : Option Prosody.PitchAccent
• nWords : ℕ

  The words grouped into the phrase.

@[instance_reducible]

instance BeckmanPierrehumbert1986.instReprAccentualPhrase : Repr AccentualPhrase

Equations

• BeckmanPierrehumbert1986.instReprAccentualPhrase = { reprPrec := BeckmanPierrehumbert1986.instReprAccentualPhrase.repr }

def BeckmanPierrehumbert1986.instReprAccentualPhrase.repr : AccentualPhrase → ℕ → Std.Format

Equations

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

def BeckmanPierrehumbert1986.instDecidableEqAccentualPhrase.decEq (x✝ x✝¹ : AccentualPhrase) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance BeckmanPierrehumbert1986.instDecidableEqAccentualPhrase : DecidableEq AccentualPhrase

Equations

• BeckmanPierrehumbert1986.instDecidableEqAccentualPhrase = BeckmanPierrehumbert1986.instDecidableEqAccentualPhrase.decEq

def BeckmanPierrehumbert1986.AccentualPhrase.TriggersCatathesis (ap : AccentualPhrase) : Prop

The phrase triggers catathesis: its accent is bitonal.

Equations

• ap.TriggersCatathesis = ∃ a ∈ ap.accent, a.IsBitonal

@[instance_reducible]

instance BeckmanPierrehumbert1986.instDecidablePredAccentualPhraseTriggersCatathesis : DecidablePred AccentualPhrase.TriggersCatathesis

Equations

• BeckmanPierrehumbert1986.instDecidablePredAccentualPhraseTriggersCatathesis ap = BeckmanPierrehumbert1986.instDecidablePredAccentualPhraseTriggersCatathesis._aux_1 ap

def BeckmanPierrehumbert1986.registerSpecs (aps : List AccentualPhrase) : List Tone.TRN

The register nodes of a sequence of accentual phrases: a downstep for each bitonal accent and nothing otherwise.

Equations

• BeckmanPierrehumbert1986.registerSpecs aps = List.map (fun (ap : BeckmanPierrehumbert1986.AccentualPhrase) => if ap.TriggersCatathesis then Tone.TRN.downstep else Tone.TRN.empty) aps

def BeckmanPierrehumbert1986.catathesisCount (aps : List AccentualPhrase) : ℕ

The number of catathesis triggers in a sequence.

Equations

• BeckmanPierrehumbert1986.catathesisCount aps = (List.filter (fun (x : BeckmanPierrehumbert1986.AccentualPhrase) => decide x.TriggersCatathesis) aps).length

@[simp]

theorem BeckmanPierrehumbert1986.catathesisCount_nil : catathesisCount [] = 0

theorem BeckmanPierrehumbert1986.catathesisCount_cons (aps : List AccentualPhrase) (ap : AccentualPhrase) : catathesisCount (ap :: aps) = (if ap.TriggersCatathesis then 1 else 0) + catathesisCount aps

theorem BeckmanPierrehumbert1986.catathesisCount_eq_zero_iff (aps : List AccentualPhrase) : catathesisCount aps = 0 ↔ ∀ ap ∈ aps, ¬ap.TriggersCatathesis

No bitonal accent, no catathesis.

theorem BeckmanPierrehumbert1986.pitchEffect_registerSpecs_nonpos (aps : List AccentualPhrase) {t : Tone.TRN} (h : t ∈ registerSpecs aps) : t.pitchEffect ≤ 0

Catathesis only compresses: no node of a sequence raises the register.

theorem BeckmanPierrehumbert1986.sum_pitchEffect_registerSpecs (aps : List AccentualPhrase) : (List.map Tone.TRN.pitchEffect (registerSpecs aps)).sum = -↑(catathesisCount aps)

The net shift of a sequence: one step down per bitonal accent.

theorem BeckmanPierrehumbert1986.realizePitch_registerSpecs (b : ℤ) (aps : List AccentualPhrase) {i : ℕ} (hi : i < aps.length) : (Tone.realizePitch b (registerSpecs aps))[i]? = some (b - ↑(catathesisCount (List.take (i + 1) aps)))

The staircase: each accentual phrase is realized one step below the baseline for every bitonal accent up to and including it.

theorem BeckmanPierrehumbert1986.realizePitch_registerSpecs_append (b : ℤ) (aps₁ aps₂ : List AccentualPhrase) : Tone.realizePitch b (registerSpecs (aps₁ ++ aps₂)) = Tone.realizePitch b (registerSpecs aps₁) ++ Tone.realizePitch (b - ↑(catathesisCount aps₁)) (registerSpecs aps₂)

One chain: a sequence followed by another is the first followed by the second continued from the compressed register.

theorem BeckmanPierrehumbert1986.boundary_raises (b : ℤ) (aps₁ aps₂ : List AccentualPhrase) : List.Forall₂ (fun (x1 x2 : ℤ) => x1 ≤ x2) (Tone.realizePitch (b - ↑(catathesisCount aps₁)) (registerSpecs aps₂)) (Tone.realizePitch b (registerSpecs aps₂))

An intermediate-phrase boundary resets the register, so every level after it is at least what continuing the chain would give.

Intermediate and intonation phrases

structure BeckmanPierrehumbert1986.IntermediatePhrase : Type

An intermediate phrase: accentual phrases closed by a phrase accent, the domain of catathesis.

• aps : List AccentualPhrase
• phraseAccent : Prosody.LevelTone
• aps_nonempty : self.aps ≠ []

def BeckmanPierrehumbert1986.instReprIntermediatePhrase.repr : IntermediatePhrase → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance BeckmanPierrehumbert1986.instReprIntermediatePhrase : Repr IntermediatePhrase

Equations

• BeckmanPierrehumbert1986.instReprIntermediatePhrase = { reprPrec := BeckmanPierrehumbert1986.instReprIntermediatePhrase.repr }

structure BeckmanPierrehumbert1986.IntonationPhrase : Type

An intonation phrase: intermediate phrases closed by a boundary tone.

• ips : List IntermediatePhrase
• boundaryTone : Prosody.LevelTone
• ips_nonempty : self.ips ≠ []

@[instance_reducible]

instance BeckmanPierrehumbert1986.instReprIntonationPhrase : Repr IntonationPhrase

Equations

• BeckmanPierrehumbert1986.instReprIntonationPhrase = { reprPrec := BeckmanPierrehumbert1986.instReprIntonationPhrase.repr }

def BeckmanPierrehumbert1986.instReprIntonationPhrase.repr : IntonationPhrase → ℕ → Std.Format

Equations

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

def BeckmanPierrehumbert1986.IntonationPhrase.terminalContour (ip : IntonationPhrase) : Prosody.TerminalContour

The terminal contour of an intonation phrase: the last intermediate phrase's phrase accent and the boundary tone, [Pie80]'s terminal sequence decomposed.

Equations

• ip.terminalContour = { phraseAccent := (ip.ips.getLast ⋯).phraseAccent, boundaryTone := ip.boundaryTone }

def BeckmanPierrehumbert1986.ipRegisterSpecs (ip : IntermediatePhrase) : List Tone.TRN

The register nodes of one intermediate phrase: a single chain.

Equations

• BeckmanPierrehumbert1986.ipRegisterSpecs ip = BeckmanPierrehumbert1986.registerSpecs ip.aps

def BeckmanPierrehumbert1986.ipRegisterSpecsAcrossIps (ips : List IntermediatePhrase) : List (List Tone.TRN)

The register nodes of an intonation phrase, one chain per intermediate phrase: each starts again from the baseline.

Equations

• BeckmanPierrehumbert1986.ipRegisterSpecsAcrossIps ips = List.map BeckmanPierrehumbert1986.ipRegisterSpecs ips

The two systems

theorem BeckmanPierrehumbert1986.card_pitchAccent : Fintype.card Prosody.PitchAccent = 10

The ten accents that the system permits in principle: two single-tone accents and eight two-tone ones (§3.2).

inductive BeckmanPierrehumbert1986.AccentSpecification : Type

Where a language's pitch-accent shapes come from (§2.1). With lexical a shape can be part of a word's phonological specification, as in the two accents of Stockholm Swedish; with intonational the shape never contrasts lexical items and instead contrasts intonational meanings, as in English. The accent locus is lexically specified in both English and Japanese (§2.5). Japanese has a single shape, so it allows neither contrast; B&P treat its accent as a lexically linked H.

• lexical : AccentSpecification
• intonational : AccentSpecification

def BeckmanPierrehumbert1986.instReprAccentSpecification.repr : AccentSpecification → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance BeckmanPierrehumbert1986.instReprAccentSpecification : Repr AccentSpecification

Equations

• BeckmanPierrehumbert1986.instReprAccentSpecification = { reprPrec := BeckmanPierrehumbert1986.instReprAccentSpecification.repr }

@[instance_reducible]

instance BeckmanPierrehumbert1986.instDecidableEqAccentSpecification : DecidableEq AccentSpecification

Equations

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

inductive BeckmanPierrehumbert1986.CatathesisTiming : Type

Where the compression takes effect relative to its trigger: within the accent itself (Japanese, whose trailing L is already compressed) or only after it (English).

• withinAccent : CatathesisTiming
• afterAccent : CatathesisTiming

def BeckmanPierrehumbert1986.instReprCatathesisTiming.repr : CatathesisTiming → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance BeckmanPierrehumbert1986.instReprCatathesisTiming : Repr CatathesisTiming

Equations

• BeckmanPierrehumbert1986.instReprCatathesisTiming = { reprPrec := BeckmanPierrehumbert1986.instReprCatathesisTiming.repr }

@[instance_reducible]

instance BeckmanPierrehumbert1986.instDecidableEqCatathesisTiming : DecidableEq CatathesisTiming

Equations

• BeckmanPierrehumbert1986.instDecidableEqCatathesisTiming x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure BeckmanPierrehumbert1986.IntonationSystem : Type

A language's intonation system: how accents are specified, the contrastive accent shapes, whether lexically unaccented words exist, whether the accentual-phrase boundary L is always present, and when catathesis takes effect.

• accentSpec : AccentSpecification
• accentShapes : List Prosody.PitchAccent
• hasUnaccented : Bool
• apBoundaryLAlwaysPresent : Bool
• catathesisTiming : CatathesisTiming

def BeckmanPierrehumbert1986.instReprIntonationSystem.repr : IntonationSystem → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance BeckmanPierrehumbert1986.instReprIntonationSystem : Repr IntonationSystem

Equations

• BeckmanPierrehumbert1986.instReprIntonationSystem = { reprPrec := BeckmanPierrehumbert1986.instReprIntonationSystem.repr }

def BeckmanPierrehumbert1986.japanese : IntonationSystem

Japanese: a lexically linked accent, the one shape H*+L, unaccented words, a boundary L in every accentual phrase, compression within the accent.

Equations

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

def BeckmanPierrehumbert1986.english : IntonationSystem

English: intonational accent shapes, the six H*, L*, H*+L, H+L*, L*+H and L+H* (§2.1), every content word accentable, no accentual-phrase boundary tone, compression after the accent.

Equations

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

theorem BeckmanPierrehumbert1986.mem_english_accentShapes_iff (a : Prosody.PitchAccent) : a ∈ english.accentShapes ↔ a.tones.Nodup

English uses exactly the accents whose tones differ: of the ten, the four two-tone accents L*+L, L+L*, H*+H and H+H* are missing, since the realisation rules would neutralise them with single-tone accents (§3.2).

theorem BeckmanPierrehumbert1986.triggers_differ : (∀ a ∈ japanese.accentShapes, registerSpecs [{ accent := some a, nWords := 1 }] = [Tone.TRN.downstep]) ∧ ∃ a ∈ english.accentShapes, registerSpecs [{ accent := some a, nWords := 1 }] = [Tone.TRN.empty]

Every Japanese accent triggers catathesis, since its one shape is bitonal; an English accent need not, since H* and L* are monotonal.

def BeckmanPierrehumbert1986.accentedAP : AccentualPhrase

An accented accentual phrase (uma'i, mo'riya-no).

Equations

• BeckmanPierrehumbert1986.accentedAP = { accent := some (Prosody.PitchAccent.trailing Prosody.LevelTone.H Prosody.LevelTone.L), nWords := 1 }

def BeckmanPierrehumbert1986.unaccentedAP : AccentualPhrase

An unaccented accentual phrase (amai, toriya-no mawari-no).

Equations

• BeckmanPierrehumbert1986.unaccentedAP = { accent := none, nWords := 1 }

Japanese accentual phrases from the lexicon

def BeckmanPierrehumbert1986.AccentualPhrase.ofWords (ws : List Japanese.Prosody.ProsodicEntry) : AccentualPhrase

The accentual phrase over grouped word entries: accented, always H*+L, iff some word is lexically accented, grouping deleting all but one accent.

Equations

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

theorem BeckmanPierrehumbert1986.ofWords_triggersCatathesis_iff (ws : List Japanese.Prosody.ProsodicEntry) : (AccentualPhrase.ofWords ws).TriggersCatathesis ↔ ∃ w ∈ ws, w.Accented

A phrase of words triggers catathesis iff some word is accented.