inductive CCG.Intonation.InfoFeature : Type

The INFORMATION feature on CCG categories.

Categories are marked as:

• θ (theta): Part of the theme
• ρ (rho): Part of the rheme
• unmarked: Unspecified (can unify with either)
• φ (phi): Phrasal (after boundary tone applies)

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

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 CCG.Intonation.instDecidableEqInfoFeature : DecidableEq InfoFeature

Equations

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

def CCG.Intonation.instInhabitedInfoFeature.default : InfoFeature

Equations

• CCG.Intonation.instInhabitedInfoFeature.default = CCG.Intonation.InfoFeature.θ

instance CCG.Intonation.instInhabitedInfoFeature : Inhabited InfoFeature

Equations

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

def CCG.Intonation.InfoFeature.unifies : InfoFeature → InfoFeature → Bool

Can two info features unify?

Equations

• CCG.Intonation.InfoFeature.unmarked.unifies x✝ = true
• x✝.unifies CCG.Intonation.InfoFeature.unmarked = true
• CCG.Intonation.InfoFeature.θ.unifies CCG.Intonation.InfoFeature.θ = true
• CCG.Intonation.InfoFeature.ρ.unifies CCG.Intonation.InfoFeature.ρ = true
• CCG.Intonation.InfoFeature.φ.unifies CCG.Intonation.InfoFeature.φ = true
• x✝¹.unifies x✝ = false

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

Unify two info features

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

structure CCG.Intonation.ProsodicCat : Type

A CCG category with prosodic annotation.

The INFORMATION feature projects through the category:

• (Sθ\NPθ)/NPθ: All arguments and result share the same info value

• cat : Cat
• info : InfoFeature

instance CCG.Intonation.instReprProsodicCat : Repr ProsodicCat

Equations

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

def CCG.Intonation.instReprProsodicCat.repr : ProsodicCat → ℕ → Std.Format

Equations

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

instance CCG.Intonation.instDecidableEqProsodicCat : DecidableEq ProsodicCat

Equations

• CCG.Intonation.instDecidableEqProsodicCat = CCG.Intonation.instDecidableEqProsodicCat.decEq

def CCG.Intonation.instDecidableEqProsodicCat.decEq (x✝ x✝¹ : ProsodicCat) : Decidable (x✝ = x✝¹)

Equations

• CCG.Intonation.instDecidableEqProsodicCat.decEq { cat := a, info := a_1 } { cat := b, info := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def CCG.Intonation.ProsodicCat.theme (c : Cat) : ProsodicCat

Notation helpers

Equations

• CCG.Intonation.ProsodicCat.theme c = { cat := c, info := CCG.Intonation.InfoFeature.θ }

def CCG.Intonation.ProsodicCat.rheme (c : Cat) : ProsodicCat

Equations

• CCG.Intonation.ProsodicCat.rheme c = { cat := c, info := CCG.Intonation.InfoFeature.ρ }

def CCG.Intonation.ProsodicCat.plain (c : Cat) : ProsodicCat

Equations

• CCG.Intonation.ProsodicCat.plain c = { cat := c, info := CCG.Intonation.InfoFeature.unmarked }

def CCG.Intonation.ProsodicCat.phrasal (c : Cat) : ProsodicCat

Equations

• CCG.Intonation.ProsodicCat.phrasal c = { cat := c, info := CCG.Intonation.InfoFeature.φ }

structure CCG.Intonation.ProsodicLexEntry : Type

A prosodic lexical entry: word + pitch accent → prosodic category.

The pitch accent determines the INFORMATION feature:

• H* → ρ (rheme)
• L+H* → θ (theme)
• null → unmarked

• form : String
• cat : Cat
• accent : Core.Prosody.PitchAccent

instance CCG.Intonation.instReprProsodicLexEntry : Repr ProsodicLexEntry

Equations

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

def CCG.Intonation.instReprProsodicLexEntry.repr : ProsodicLexEntry → ℕ → Std.Format

Equations

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

def CCG.Intonation.ProsodicLexEntry.prosodicCat (e : ProsodicLexEntry) : ProsodicCat

Get the prosodic category from a lexical entry

Equations

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

structure CCG.Intonation.Tune : Type

An intonational tune: pitch accent + boundary.

The two main tunes in English:

• L+H* LH%: Theme tune (fall-rise)
• H* LL%: Rheme tune (fall)

• accent : Core.Prosody.PitchAccent
• boundary : Core.Prosody.BoundaryTone

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

Equations

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

instance CCG.Intonation.instReprTune : Repr Tune

Equations

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

instance CCG.Intonation.instDecidableEqTune : DecidableEq Tune

Equations

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

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

Equations

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

def CCG.Intonation.themeTune : Tune

The canonical theme tune

Equations

• CCG.Intonation.themeTune = { accent := Core.Prosody.PitchAccent.L_plus_H_star, boundary := Core.Prosody.BoundaryTone.LH_pct }

def CCG.Intonation.rhemeTune : Tune

The canonical rheme tune

Equations

• CCG.Intonation.rhemeTune = { accent := Core.Prosody.PitchAccent.H_star, boundary := Core.Prosody.BoundaryTone.LL_pct }

def CCG.Intonation.Tune.isTheme (t : Tune) : Bool

Is this a theme tune?

Equations

• t.isTheme = (t.accent == Core.Prosody.PitchAccent.L_plus_H_star && t.boundary == Core.Prosody.BoundaryTone.LH_pct)

def CCG.Intonation.Tune.isRheme (t : Tune) : Bool

Is this a rheme tune?

Equations

• t.isRheme = (t.accent == Core.Prosody.PitchAccent.H_star && t.boundary == Core.Prosody.BoundaryTone.LL_pct)

def CCG.Intonation.prosodicForwardApp : ProsodicCat → ProsodicCat → Option ProsodicCat

Prosodic forward application: X/Y + Y → X Only succeeds if INFORMATION features unify.

Equations

• One or more equations did not get rendered due to their size.
• CCG.Intonation.prosodicForwardApp x✝¹ x✝ = none

def CCG.Intonation.prosodicBackwardApp : ProsodicCat → ProsodicCat → Option ProsodicCat

Prosodic backward application: Y + X\Y → X Only succeeds if INFORMATION features unify.

Equations

• One or more equations did not get rendered due to their size.
• CCG.Intonation.prosodicBackwardApp x✝¹ x✝ = none

def CCG.Intonation.prosodicForwardComp : ProsodicCat → ProsodicCat → Option ProsodicCat

Prosodic forward composition: X/Y + Y/Z → X/Z INFORMATION features must unify and project to result.

Equations

• One or more equations did not get rendered due to their size.
• CCG.Intonation.prosodicForwardComp x✝¹ x✝ = none

def CCG.Intonation.applyBoundary : ProsodicCat → Core.Prosody.BoundaryTone → ProsodicCat

Apply a boundary tone to a prosodic category. Converts θ/ρ marking to φ (phrasal).

Equations

• CCG.Intonation.applyBoundary { cat := cat, info := CCG.Intonation.InfoFeature.θ } x✝ = { cat := cat, info := CCG.Intonation.InfoFeature.φ }
• CCG.Intonation.applyBoundary { cat := cat, info := CCG.Intonation.InfoFeature.ρ } x✝ = { cat := cat, info := CCG.Intonation.InfoFeature.φ }
• CCG.Intonation.applyBoundary { cat := cat, info := CCG.Intonation.InfoFeature.unmarked } x✝ = { cat := cat, info := CCG.Intonation.InfoFeature.φ }
• CCG.Intonation.applyBoundary { cat := cat, info := CCG.Intonation.InfoFeature.φ } x✝ = { cat := cat, info := CCG.Intonation.InfoFeature.φ }

inductive CCG.Intonation.ProsodicDeriv : Type

A prosodic derivation step. Extends CCG derivations with prosodic information.

• lex : ProsodicLexEntry → ProsodicDeriv
• fapp : ProsodicDeriv → ProsodicDeriv → ProsodicDeriv
• bapp : ProsodicDeriv → ProsodicDeriv → ProsodicDeriv
• fcomp : ProsodicDeriv → ProsodicDeriv → ProsodicDeriv
• bcomp : ProsodicDeriv → ProsodicDeriv → ProsodicDeriv
• ftr : ProsodicDeriv → Cat → ProsodicDeriv
• boundary : ProsodicDeriv → Core.Prosody.BoundaryTone → ProsodicDeriv

instance CCG.Intonation.instReprProsodicDeriv : Repr ProsodicDeriv

Equations

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

def CCG.Intonation.instReprProsodicDeriv.repr : ProsodicDeriv → ℕ → Std.Format

Equations

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

def CCG.Intonation.ProsodicDeriv.prosodicCat : ProsodicDeriv → Option ProsodicCat

Get the prosodic category of a derivation

Equations

• (CCG.Intonation.ProsodicDeriv.lex a).prosodicCat = some a.prosodicCat
• (a.fapp a_1).prosodicCat = do let c1 ← a.prosodicCat let c2 ← a_1.prosodicCat CCG.Intonation.prosodicForwardApp c1 c2
• (a.bapp a_1).prosodicCat = do let c1 ← a.prosodicCat let c2 ← a_1.prosodicCat CCG.Intonation.prosodicBackwardApp c1 c2
• (a.fcomp a_1).prosodicCat = do let c1 ← a.prosodicCat let c2 ← a_1.prosodicCat CCG.Intonation.prosodicForwardComp c1 c2
• (a.bcomp a_1).prosodicCat = none
• (a.ftr a_1).prosodicCat = do let __discr ← a.prosodicCat match __discr with | { cat := x, info := i } => some { cat := CCG.forwardTypeRaise x a_1, info := i }
• (a.boundary a_1).prosodicCat = do let c ← a.prosodicCat some (CCG.Intonation.applyBoundary c a_1)

structure CCG.Intonation.ProsodicPhrase : Type

A prosodic phrase: a derivation with a boundary tone applied.

• deriv : ProsodicDeriv
• tune : Tune

instance CCG.Intonation.instReprProsodicPhrase : Repr ProsodicPhrase

Equations

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

def CCG.Intonation.instReprProsodicPhrase.repr : ProsodicPhrase → ℕ → Std.Format

Equations

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

def CCG.Intonation.extractInfoStructure (phrases : List ProsodicPhrase) : Option (Core.InformationStructure.InfoStructure ProsodicDeriv)

Extract Information Structure from a sequence of prosodic phrases.

The phrase with theme tune (L+H* LH%) becomes the theme. The phrase with rheme tune (H* LL%) becomes the rheme.

Equations

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

instance CCG.Intonation.instHasInfoStructureListProsodicPhraseProsodicDeriv : Core.InformationStructure.HasInfoStructure (List ProsodicPhrase) ProsodicDeriv

Prosodic CCG derivations have Information Structure.

Equations

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

def CCG.Intonation.fred_L : ProsodicLexEntry

Equations

• CCG.Intonation.fred_L = { form := "Fred", cat := CCG.NP, accent := Core.Prosody.PitchAccent.L_plus_H_star }

def CCG.Intonation.ate_null : ProsodicLexEntry

Equations

• CCG.Intonation.ate_null = { form := "ate", cat := CCG.TV, accent := Core.Prosody.PitchAccent.null }

def CCG.Intonation.the_null : ProsodicLexEntry

Equations

• CCG.Intonation.the_null = { form := "the", cat := CCG.Det, accent := Core.Prosody.PitchAccent.null }

def CCG.Intonation.beans_H : ProsodicLexEntry

Equations

• CCG.Intonation.beans_H = { form := "beans", cat := CCG.N, accent := Core.Prosody.PitchAccent.H_star }

def CCG.Intonation.fred_tr : ProsodicDeriv

Equations

• CCG.Intonation.fred_tr = (CCG.Intonation.ProsodicDeriv.lex CCG.Intonation.fred_L).ftr CCG.S

def CCG.Intonation.fred_ate : ProsodicDeriv

Equations

• CCG.Intonation.fred_ate = CCG.Intonation.fred_tr.fcomp (CCG.Intonation.ProsodicDeriv.lex CCG.Intonation.ate_null)

def CCG.Intonation.fred_ate_phrase : ProsodicDeriv

Equations

• CCG.Intonation.fred_ate_phrase = CCG.Intonation.fred_ate.boundary Core.Prosody.BoundaryTone.LH_pct

def CCG.Intonation.the_beans : ProsodicDeriv

Equations

• CCG.Intonation.the_beans = (CCG.Intonation.ProsodicDeriv.lex CCG.Intonation.the_null).fapp (CCG.Intonation.ProsodicDeriv.lex CCG.Intonation.beans_H)

def CCG.Intonation.the_beans_phrase : ProsodicDeriv

Equations

• CCG.Intonation.the_beans_phrase = CCG.Intonation.the_beans.boundary Core.Prosody.BoundaryTone.LL_pct

def CCG.Intonation.anna_L : ProsodicLexEntry

Equations

• CCG.Intonation.anna_L = { form := "Anna", cat := CCG.NP, accent := Core.Prosody.PitchAccent.L_plus_H_star }

def CCG.Intonation.married_null : ProsodicLexEntry

Equations

• CCG.Intonation.married_null = { form := "married", cat := CCG.TV, accent := Core.Prosody.PitchAccent.null }

def CCG.Intonation.manny_H : ProsodicLexEntry

Equations

• CCG.Intonation.manny_H = { form := "Manny", cat := CCG.NP, accent := Core.Prosody.PitchAccent.H_star }

def CCG.Intonation.anna_tr : ProsodicDeriv

Equations

• CCG.Intonation.anna_tr = (CCG.Intonation.ProsodicDeriv.lex CCG.Intonation.anna_L).ftr CCG.S

def CCG.Intonation.anna_married : ProsodicDeriv

Equations

• CCG.Intonation.anna_married = CCG.Intonation.anna_tr.fcomp (CCG.Intonation.ProsodicDeriv.lex CCG.Intonation.married_null)

def CCG.Intonation.anna_married_theme : ProsodicPhrase

Equations

• CCG.Intonation.anna_married_theme = { deriv := CCG.Intonation.anna_married.boundary Core.Prosody.BoundaryTone.LH_pct, tune := CCG.Intonation.themeTune }

def CCG.Intonation.manny_rheme : ProsodicPhrase

Equations

• CCG.Intonation.manny_rheme = { deriv := (CCG.Intonation.ProsodicDeriv.lex CCG.Intonation.manny_H).boundary Core.Prosody.BoundaryTone.LL_pct, tune := CCG.Intonation.rhemeTune }

def CCG.Intonation.anna_married_manny : List ProsodicPhrase

Equations

• CCG.Intonation.anna_married_manny = [CCG.Intonation.anna_married_theme, CCG.Intonation.manny_rheme]

def CCG.Intonation.ProsodicDeriv.wellFormed : ProsodicDeriv → Bool

Check if a prosodic derivation is well-formed (simplified)

Equations

• (CCG.Intonation.ProsodicDeriv.lex a).wellFormed = true
• (a.fapp a_1).wellFormed = (a.wellFormed && a_1.wellFormed && a.prosodicCat.isSome)
• (a.bapp a_1).wellFormed = (a.wellFormed && a_1.wellFormed)
• (a.fcomp a_1).wellFormed = (a.wellFormed && a_1.wellFormed && a.prosodicCat.isSome)
• (a.bcomp a_1).wellFormed = (a.wellFormed && a_1.wellFormed)
• (a.ftr a_1).wellFormed = a.wellFormed
• (a.boundary a_1).wellFormed = (a.wellFormed && a.prosodicCat.isSome)