CCG intonation and information structure

Steedman aligns prosodic structure with CCG derivations through an INFORMATION feature, theme or rheme, that pitch accents mark on words and that combination unifies up the derivation. CCG's spurious ambiguity is the engine: alternative derivations of one string are alternative information structures, disambiguated by intonation, so "Anna married Manny" derives both [Anna][married Manny] and, by composition, [Anna married][Manny], and the theme tune on "ANNA married" selects the latter. Because a ProsodicPhrase carries a Derivation, only CCG constituents can be prosodic phrases, which is Selkirk's Sense Unit Condition by construction.

Main definitions

• CCG.Intonation.InfoFeature: the INFORMATION feature, with InfoFeature.unify its partial join, a PartialUnify instance.
• CCG.Intonation.accentInfo: the marking an accent slot contributes.
• CCG.Derivation.infoFeature: the feature a derivation projects under an accent assignment, none on a theme/rheme clash.
• CCG.Intonation.Tune, CCG.Intonation.themeTune, CCG.Intonation.rhemeTune: pitch accent plus terminal contour.
• CCG.Intonation.ProsodicPhrase, CCG.Intonation.extractInfoStructure: tune-marked constituents and the theme/rheme partition of an utterance.

Implementation notes

The prosodic vocabulary comes from Prosody's autosegmental-metrical types. Relating these phrases to the phonology-side prosodic hierarchy (Phonology/Prosody/Phrase) is left to study-level work.

References

• [Ste00a]
• [Sel84]
• [PH90]
• [Car92]
• [Kur72]

The INFORMATION feature

inductive CCG.Intonation.InfoFeature : Type

The INFORMATION feature of [Ste00a].

• θ : InfoFeature

  Theme.

• ρ : InfoFeature

  Rheme.

• unmarked : InfoFeature

  Unspecified, unifying with either theme or rheme.

• φ : InfoFeature

  Phrasal, after a boundary has applied.

@[instance_reducible]

instance CCG.Intonation.instReprInfoFeature : Repr InfoFeature

Equations

• CCG.Intonation.instReprInfoFeature = { reprPrec := CCG.Intonation.instReprInfoFeature.repr }

def CCG.Intonation.instReprInfoFeature.repr : InfoFeature → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance CCG.Intonation.instDecidableEqInfoFeature : DecidableEq InfoFeature

Equations

• CCG.Intonation.instDecidableEqInfoFeature x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance CCG.Intonation.instInhabitedInfoFeature : Inhabited InfoFeature

Equations

• CCG.Intonation.instInhabitedInfoFeature = { default := CCG.Intonation.instInhabitedInfoFeature.default }

@[instance_reducible]

instance CCG.Intonation.instFintypeInfoFeature : Fintype InfoFeature

Equations

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

def CCG.Intonation.InfoFeature.unify : InfoFeature → InfoFeature → WithTop InfoFeature

The unification of two info features, their partial join in the subsumption order below (PartialUnify).

Equations

• CCG.Intonation.InfoFeature.unmarked.unify x✝ = ↑x✝
• x✝.unify CCG.Intonation.InfoFeature.unmarked = ↑x✝
• CCG.Intonation.InfoFeature.θ.unify CCG.Intonation.InfoFeature.θ = ↑CCG.Intonation.InfoFeature.θ
• CCG.Intonation.InfoFeature.ρ.unify CCG.Intonation.InfoFeature.ρ = ↑CCG.Intonation.InfoFeature.ρ
• CCG.Intonation.InfoFeature.φ.unify CCG.Intonation.InfoFeature.φ = ↑CCG.Intonation.InfoFeature.φ
• x✝¹.unify x✝ = ⊤

The information feature as a subsumption order

unmarked is Steedman's underspecified feature — the category that "can unify with either" theme or rheme — so it is ⊥; θ, ρ, φ are pairwise-incomparable atoms above it. This is the flat order of feature unification ([Car92]) carried on the information feature: InfoFeature.unify is its partial join (PartialUnify) and the total meet is generalization (anti-unification).

@[instance_reducible]

instance CCG.Intonation.instLEInfoFeature : LE InfoFeature

Equations

• CCG.Intonation.instLEInfoFeature = { le := fun (a b : CCG.Intonation.InfoFeature) => a = CCG.Intonation.InfoFeature.unmarked ∨ a = b }

theorem CCG.Intonation.InfoFeature.le_def {a b : InfoFeature} : a ≤ b ↔ a = unmarked ∨ a = b

@[instance_reducible]

instance CCG.Intonation.instDecidableLeInfoFeature (a b : InfoFeature) : Decidable (a ≤ b)

Equations

• CCG.Intonation.instDecidableLeInfoFeature a b = decidable_of_iff (a = CCG.Intonation.InfoFeature.unmarked ∨ a = b) ⋯

@[instance_reducible]

instance CCG.Intonation.instPartialOrderInfoFeature : PartialOrder InfoFeature

Equations

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

@[instance_reducible]

instance CCG.Intonation.instOrderBotInfoFeature : OrderBot InfoFeature

Equations

• CCG.Intonation.instOrderBotInfoFeature = { bot := CCG.Intonation.InfoFeature.unmarked, bot_le := CCG.Intonation.instOrderBotInfoFeature._proof_1 }

@[instance_reducible]

instance CCG.Intonation.instMinInfoFeature : Min InfoFeature

Equations

• CCG.Intonation.instMinInfoFeature = { min := fun (a b : CCG.Intonation.InfoFeature) => if a = b then a else CCG.Intonation.InfoFeature.unmarked }

@[instance_reducible]

instance CCG.Intonation.instSemilatticeInfInfoFeature : SemilatticeInf InfoFeature

Equations

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

@[instance_reducible]

instance CCG.Intonation.instPartialUnifyInfoFeature : PartialUnify InfoFeature

Equations

• CCG.Intonation.instPartialUnifyInfoFeature = { unify := CCG.Intonation.InfoFeature.unify, isLUB_of_unify_eq_coe := ⋯, unify_ne_top_of_bddAbove := ⋯ }

Projecting information structure through a derivation

def CCG.Intonation.accentInfo : Option Prosody.PitchAccent → InfoFeature

The information marking an accent slot contributes. In [Ste00a] L+H* marks the theme and H* and H*+L the rheme, and unaccented material is unmarked. The book classes no other accent, and the rest are grouped with the rheme here.

Equations

• CCG.Intonation.accentInfo (some (Prosody.PitchAccent.leading Prosody.LevelTone.L Prosody.LevelTone.H)) = CCG.Intonation.InfoFeature.θ
• CCG.Intonation.accentInfo none = CCG.Intonation.InfoFeature.unmarked
• CCG.Intonation.accentInfo (some val) = CCG.Intonation.InfoFeature.ρ

def CCG.Intonation.AccentAssignment (T : Type u_1) : Type u_1

An assignment of pitch accents to the tokens of a derivation, none for an unaccented token.

Equations

• CCG.Intonation.AccentAssignment T = (T → Option Prosody.PitchAccent)

def CCG.Derivation.infoFeature {T : Type u_1} {α : Type u_2} {R : RuleSystem α} (acc : Intonation.AccentAssignment T) {c : Cat α} : Derivation T R c → Option Intonation.InfoFeature

The INFORMATION feature a derivation projects under an accent assignment. Leaves contribute the accentInfo of their accent and combination unifies the daughters' features, with none on a theme/rheme clash, the prosodic analogue of Derivation.interp's reading of the same tree.

Equations

• One or more equations did not get rendered due to their size.
• CCG.Derivation.infoFeature acc (CCG.Derivation.lex f x✝) = some (CCG.Intonation.accentInfo (acc f))

Tunes and prosodic phrases

structure CCG.Intonation.Tune : Type

An intonational tune is a pitch accent plus a terminal contour. Of the two main tunes of English in [Ste00a], L+H* LH% marks the theme and H* LL% the rheme.

• accent : Prosody.PitchAccent

  The pitch accent.

• terminal : Prosody.TerminalContour

  The phrase accent and boundary tone.

def CCG.Intonation.instReprTune.repr : Tune → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance CCG.Intonation.instReprTune : Repr Tune

Equations

• CCG.Intonation.instReprTune = { reprPrec := CCG.Intonation.instReprTune.repr }

def CCG.Intonation.instDecidableEqTune.decEq (x✝ x✝¹ : Tune) : Decidable (x✝ = x✝¹)

Equations

• CCG.Intonation.instDecidableEqTune.decEq { accent := a, terminal := a_1 } { accent := b, terminal := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance CCG.Intonation.instDecidableEqTune : DecidableEq Tune

Equations

• CCG.Intonation.instDecidableEqTune = CCG.Intonation.instDecidableEqTune.decEq

def CCG.Intonation.themeTune : Tune

The theme tune, L+H* with the rise LH%.

Equations

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

def CCG.Intonation.rhemeTune : Tune

The rheme tune, H* with the fall LL%.

Equations

• CCG.Intonation.rhemeTune = { accent := Prosody.PitchAccent.mono Prosody.LevelTone.H, terminal := { phraseAccent := Prosody.LevelTone.L, boundaryTone := Prosody.LevelTone.L } }

structure CCG.Intonation.ProsodicPhrase (T : Type u_1) {α : Type u_2} (R : RuleSystem α) : Type (max u_1 u_2)

A prosodic phrase is a tune-marked CCG constituent. Because deriv is a derivation, only constituents can be phrases, the Sense Unit Condition of [Sel84] by construction.

• cat : Cat α

  The category of the constituent.

• deriv : Derivation T R self.cat

  The constituent's derivation.

• tune : Tune

  The tune the phrase carries.

structure CCG.Intonation.InfoStructure (P : Type u_1) : Type u_1

An information-structure analysis is a theme/rheme partition, following [Ste00a]. The theme is what the utterance is about (the λ-abstract presupposing a QUD, marked in English by the L+H* LH% tune per [PH90]) and the rheme is what is asserted about it (marked H* LL%). theme := none encodes an all-rheme structure, thetic in [Kur72]'s sense, with no theme constituent.

• theme : Option P

  The theme (λ-abstract, presupposed QUD); none for all-rheme (thetic) structures.

• rheme : P

  The rheme (comment, answer, assertion).

• foci : List P

  Focused elements (evoking alternatives).

• background : List P

  Background elements (given).

def CCG.Intonation.extractInfoStructure {T : Type u_1} {α : Type u_2} {R : RuleSystem α} (phrases : List (ProsodicPhrase T R)) : Option (InfoStructure (ProsodicPhrase T R))

The information structure of a sequence of prosodic phrases takes the phrase with the theme tune as theme and the phrase with the rheme tune as rheme, and a theme-less utterance is all-rheme. It is none when the phrases yield no coherent partition.

Equations

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