Kao and Goodman (2015): Let's Talk (Ironically) About the Weather

Kao and Goodman model irony on the RSA kernel pipeline. The model is that of Kao and colleagues for hyperbole, over meanings that pair a weather state with the speaker's affect toward it, the question being the state or a dimension of affect (eq. 1). The paper's contribution is the affect space, valence together with the arousal dimension it finds in its elicited emotion ratings.

Main results

• KaoGoodman2015.irony: under the arousal question, the weather is terrible can mean amazing weather with positive valence and high arousal, whenever the prior admits high arousal at terrible weather.
• KaoGoodman2015.valence_flip_needs_arousal: under the questions of state and valence alone, a positive-valence reading of terrible needs positive valence to be possible at terrible weather itself.
• KaoGoodman2015.hyperbole: the reading as merely bad weather is available under the valence question.

Implementation notes

• Priors are arguments. The state prior of a weather context and the affect prior of Experiment 1, the probabilities of positive valence and high arousal at each state, enter as one probability measure on meanings, and the question prior as a probability measure on questions.
• The model's fits to Experiment 2 are not stated.

References

• [KG15]
• [KWBG14]

inductive KaoGoodman2015.Weather : Type

The weather states, which are also the utterances.

• terrible : Weather
• bad : Weather
• neutral : Weather
• good : Weather
• amazing : Weather

@[instance_reducible]

instance KaoGoodman2015.instDecidableEqWeather : DecidableEq Weather

Equations

• KaoGoodman2015.instDecidableEqWeather x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance KaoGoodman2015.instReprWeather : Repr Weather

Equations

• KaoGoodman2015.instReprWeather = { reprPrec := KaoGoodman2015.instReprWeather.repr }

def KaoGoodman2015.instReprWeather.repr : Weather → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance KaoGoodman2015.instFintypeWeather : Fintype Weather

Equations

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

@[instance_reducible]

instance KaoGoodman2015.instMeasurableSpaceWeather : MeasurableSpace Weather

Equations

• KaoGoodman2015.instMeasurableSpaceWeather = ⊤

instance KaoGoodman2015.instDiscreteMeasurableSpaceWeather : DiscreteMeasurableSpace Weather

instance KaoGoodman2015.instNonemptyWeather : Nonempty Weather

@[reducible, inline]

abbrev KaoGoodman2015.Affect : Type

The speaker's affect records positive valence and high arousal.

Equations

• KaoGoodman2015.Affect = (Bool × Bool)

@[reducible, inline]

abbrev KaoGoodman2015.Meaning : Type

A meaning pairs the weather state with the speaker's affect toward it.

Equations

• KaoGoodman2015.Meaning = (KaoGoodman2015.Weather × KaoGoodman2015.Affect)

inductive KaoGoodman2015.QUD : Type

The question under discussion asks for the state or for a dimension of affect.

• state : QUD
• valence : QUD
• arousal : QUD

@[instance_reducible]

instance KaoGoodman2015.instDecidableEqQUD : DecidableEq QUD

Equations

• KaoGoodman2015.instDecidableEqQUD x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def KaoGoodman2015.instReprQUD.repr : QUD → ℕ → Std.Format

Equations

• KaoGoodman2015.instReprQUD.repr KaoGoodman2015.QUD.state prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "KaoGoodman2015.QUD.state")).group prec✝
• KaoGoodman2015.instReprQUD.repr KaoGoodman2015.QUD.valence prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "KaoGoodman2015.QUD.valence")).group prec✝
• KaoGoodman2015.instReprQUD.repr KaoGoodman2015.QUD.arousal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "KaoGoodman2015.QUD.arousal")).group prec✝

@[instance_reducible]

instance KaoGoodman2015.instReprQUD : Repr QUD

Equations

• KaoGoodman2015.instReprQUD = { reprPrec := KaoGoodman2015.instReprQUD.repr }

@[instance_reducible]

instance KaoGoodman2015.instFintypeQUD : Fintype QUD

Equations

• KaoGoodman2015.instFintypeQUD = { elems := { val := ↑KaoGoodman2015.QUD.enumList, nodup := KaoGoodman2015.QUD.enumList_nodup }, complete := KaoGoodman2015.instFintypeQUD._proof_1 }

@[instance_reducible]

instance KaoGoodman2015.instMeasurableSpaceQUD : MeasurableSpace QUD

Equations

• KaoGoodman2015.instMeasurableSpaceQUD = ⊤

instance KaoGoodman2015.instDiscreteMeasurableSpaceQUD : DiscreteMeasurableSpace QUD

instance KaoGoodman2015.instNonemptyQUD : Nonempty QUD

def KaoGoodman2015.project : QUD → Meaning → Weather ⊕ Bool

The projection of a question (eq. 1) reads off the state, the valence, or the arousal.

Equations

• KaoGoodman2015.project KaoGoodman2015.QUD.state x✝ = Sum.inl x✝.1
• KaoGoodman2015.project KaoGoodman2015.QUD.valence x✝ = Sum.inr x✝.2.1
• KaoGoodman2015.project KaoGoodman2015.QUD.arousal x✝ = Sum.inr x✝.2.2

def KaoGoodman2015.sem (u : Weather) : Set Meaning

An utterance is true of the meanings whose state it names.

Equations

• KaoGoodman2015.sem u = {m : KaoGoodman2015.Meaning | m.1 = u}

noncomputable def KaoGoodman2015.L0 (μ : MeasureTheory.Measure Meaning) : ProbabilityTheory.Kernel Weather Meaning

The literal listener conditions the prior on the state named.

Equations

• KaoGoodman2015.L0 μ = RSA.listener μ (RSA.truthful KaoGoodman2015.sem)

instance KaoGoodman2015.instIsFiniteKernelWeatherMeaningL0 (μ : MeasureTheory.Measure Meaning) : ProbabilityTheory.IsFiniteKernel (L0 μ)

noncomputable def KaoGoodman2015.S1 (μ : MeasureTheory.Measure Meaning) (α : ℝ) (p : Meaning × QUD) : MeasureTheory.Measure Weather

The question-indexed speaker knows the answer to her question and is informative about the literal listener's belief about it (eq. 1), at rationality α and no utterance cost.

Equations

• KaoGoodman2015.S1 μ α p = (RSA.speaker α 0 (⇑((KaoGoodman2015.L0 μ).map (KaoGoodman2015.project p.2))) MeasureTheory.Measure.dirac) (KaoGoodman2015.project p.2 p.1)

instance KaoGoodman2015.instIsFiniteMeasureWeatherS1 (μ : MeasureTheory.Measure Meaning) (α : ℝ) (p : Meaning × QUD) : MeasureTheory.IsFiniteMeasure (S1 μ α p)

noncomputable def KaoGoodman2015.L1 (μ : MeasureTheory.Measure Meaning) [MeasureTheory.IsProbabilityMeasure μ] (ν : MeasureTheory.Measure QUD) [MeasureTheory.IsProbabilityMeasure ν] (α : ℝ) : ProbabilityTheory.Kernel Weather (Meaning × QUD)

The pragmatic listener over meaning and question inverts the speaker against the product of the meaning prior and the question prior; its first marginal is the meaning listener.

Equations

• KaoGoodman2015.L1 μ ν α = RSA.listener (μ.prod ν) (KaoGoodman2015.S1 μ α)

theorem KaoGoodman2015.listener_ne_zero_iff (μ : MeasureTheory.Measure Meaning) [MeasureTheory.IsProbabilityMeasure μ] (ν : MeasureTheory.Measure QUD) [MeasureTheory.IsProbabilityMeasure ν] (α : ℝ) (hα : 0 < α) (u : Weather) (m : Meaning) : ((L1 μ ν α) u).fst {m} ≠ 0 ↔ μ {m} ≠ 0 ∧ ∃ (q : QUD), ν {q} ≠ 0 ∧ ∃ (m' : Meaning), project q m' = project q m ∧ m'.1 = u ∧ μ {m'} ≠ 0

A meaning is a possible interpretation of an utterance exactly when it has positive prior and, under some question of positive prior, shares its answer with a meaning of positive prior at which the utterance is literally true.

theorem KaoGoodman2015.hyperbole (μ : MeasureTheory.Measure Meaning) [MeasureTheory.IsProbabilityMeasure μ] (ν : MeasureTheory.Measure QUD) [MeasureTheory.IsProbabilityMeasure ν] (α : ℝ) (hα : 0 < α) (hν : ν {QUD.valence} ≠ 0) {a a' : Bool} (hbad : μ {(Weather.bad, false, a)} ≠ 0) (hterrible : μ {(Weather.terrible, false, a')} ≠ 0) : ((L1 μ ν α) Weather.terrible).fst {(Weather.bad, false, a)} ≠ 0

Under the valence question, "terrible" can hyperbolically mean bad weather with negative valence, through the negative valence of terrible weather.

theorem KaoGoodman2015.irony (μ : MeasureTheory.Measure Meaning) [MeasureTheory.IsProbabilityMeasure μ] (ν : MeasureTheory.Measure QUD) [MeasureTheory.IsProbabilityMeasure ν] (α : ℝ) (hα : 0 < α) (hν : ν {QUD.arousal} ≠ 0) {v : Bool} (hamazing : μ {(Weather.amazing, true, true)} ≠ 0) (hterrible : μ {(Weather.terrible, v, true)} ≠ 0) : ((L1 μ ν α) Weather.terrible).fst {(Weather.amazing, true, true)} ≠ 0

Under the arousal question, "terrible" can ironically mean amazing weather with positive valence and high arousal, through the high arousal of terrible weather.

theorem KaoGoodman2015.valence_flip_needs_arousal (μ : MeasureTheory.Measure Meaning) [MeasureTheory.IsProbabilityMeasure μ] (ν : MeasureTheory.Measure QUD) [MeasureTheory.IsProbabilityMeasure ν] (α : ℝ) (hα : 0 < α) (hν : ∀ (q : QUD), ν {q} ≠ 0 → q ≠ QUD.arousal) {s : Weather} {a : Bool} (h : ((L1 μ ν α) Weather.terrible).fst {(s, true, a)} ≠ 0) : ∃ (a' : Bool), μ {(Weather.terrible, true, a')} ≠ 0

Without the arousal question, a positive-valence reading of "terrible" needs positive valence to be possible at terrible weather itself, since a negative utterance carries no true information about positive affect.