CCG Intonation and Information Structure

This file defines [Ste00a]'s alignment of prosodic structure with CCG derivations: the INFORMATION feature (theme/rheme) as a unification lattice, the projection of that feature through a derivation from its leaves' pitch accents, and prosodic phrases as tune-marked constituents.

CCG's "spurious ambiguity" is the engine: alternative derivations of one string are alternative information structures, disambiguated by intonation — "Anna married Manny" derives both [Anna][married Manny] and, via composition, [Anna married] [Manny], and the theme tune on "ANNA married" selects the latter. Because a ProsodicPhrase carries an intrinsically typed Derivation, only CCG constituents can be prosodic phrases — [Sel84]'s Sense Unit Condition holds by construction ([Ste00a] ch. 2).

Main definitions

• InfoFeature: the INFORMATION feature — theme θ, rheme ρ, unmarked (the ⊥ of a flat subsumption order), and phrasal φ; InfoFeature.unify is its partial join, a PartialUnify instance.
• accentInfo: the marking a pitch accent contributes (L+H* ⇒ θ, null ⇒ unmarked, other accents ⇒ ρ).
• Derivation.infoFeature: the feature a derivation projects under an accent assignment for its leaf forms — combination unifies, type-raising preserves; none on a theme/rheme clash.
• Tune, themeTune, rhemeTune: pitch accent plus terminal contour.
• ProsodicPhrase, extractInfoStructure: tune-marked constituents and the theme/rheme partition of an utterance ([PH90]).

Implementation notes

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

The INFORMATION feature

inductive CCG.Intonation.InfoFeature : Type

• θ : InfoFeature
• ρ : InfoFeature
• unmarked : InfoFeature
• φ : InfoFeature

@[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 → Option InfoFeature

Unify two info features: the partial join in the subsumption order below (PartialUnify).

Equations

• CCG.Intonation.InfoFeature.unmarked.unify x✝ = some x✝
• x✝.unify CCG.Intonation.InfoFeature.unmarked = some x✝
• CCG.Intonation.InfoFeature.θ.unify CCG.Intonation.InfoFeature.θ = some CCG.Intonation.InfoFeature.θ
• CCG.Intonation.InfoFeature.ρ.unify CCG.Intonation.InfoFeature.ρ = some CCG.Intonation.InfoFeature.ρ
• CCG.Intonation.InfoFeature.φ.unify CCG.Intonation.InfoFeature.φ = some CCG.Intonation.InfoFeature.φ
• x✝¹.unify x✝ = none

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

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

Projecting information structure through a derivation

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

The information marking a pitch accent contributes ([Ste00a]: L+H* marks the theme, unaccented material is unmarked, and H* with the remaining accents mark the rheme).

Equations

• CCG.Intonation.accentInfo Features.Prosody.PitchAccent.L_plus_H_star = CCG.Intonation.InfoFeature.θ
• CCG.Intonation.accentInfo Features.Prosody.PitchAccent.null = CCG.Intonation.InfoFeature.unmarked
• CCG.Intonation.accentInfo x✝ = CCG.Intonation.InfoFeature.ρ

def CCG.Intonation.AccentAssignment : Type

An assignment of pitch accents to the leaf forms of a derivation.

Equations

• CCG.Intonation.AccentAssignment = (String → Features.Prosody.PitchAccent)

def CCG.Derivation.infoFeature (acc : Intonation.AccentAssignment) {c : Cat Atom} : Derivation Atom c → Option Intonation.InfoFeature

The INFORMATION feature a derivation projects under an accent assignment: leaves contribute accentInfo of their accent, combination unifies the daughters' features, and type-raising preserves. 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: pitch accent plus terminal contour. The two main tunes of English ([Ste00a]): L+H* LH% marks the theme, H* LL% the rheme.

• accent : Features.Prosody.PitchAccent
• terminal : Features.Prosody.TerminalContour

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 continuation rise (LH%).

Equations

• CCG.Intonation.themeTune = { accent := Features.Prosody.PitchAccent.L_plus_H_star, terminal := Features.Prosody.TerminalContour.continuation }

def CCG.Intonation.rhemeTune : Tune

The rheme tune: H* with declarative fall (LL%).

Equations

• CCG.Intonation.rhemeTune = { accent := Features.Prosody.PitchAccent.H_star, terminal := Features.Prosody.TerminalContour.declarative }

structure CCG.Intonation.ProsodicPhrase : Type

A prosodic phrase: a tune-marked CCG constituent. Because deriv is an intrinsically typed derivation, only constituents can be phrases — the Sense Unit Condition ([Sel84]) by construction.

• cat : Cat Atom
• deriv : Derivation Atom self.cat
• tune : Tune

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

An information-structure analysis as a theme/rheme partition, following [Ste00a]: the theme is what the utterance is about (the λ-abstract presupposing a QUD, marked by the L+H* LH% theme tune in English per [PH90]); the rheme is what is asserted about it (marked H* LL%). theme := none encodes an all-rheme (thetic, in [Kur72]'s sense) structure 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 (phrases : List ProsodicPhrase) : Option (InfoStructure ProsodicPhrase)

Extract the information structure of a sequence of prosodic phrases: the phrase with the theme tune becomes the theme, the phrase with the rheme tune the rheme, and a theme-less utterance is all-rheme. none when the phrase list yields no coherent partition.

Equations

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