Spinoso-Di Piano, Austin, Piantanida and Cheung (2025): (RSA)²: A Rhetorical-Strategy-Aware Rational Speech Act Framework for Figurative Language Understanding

The framework replaces the Boolean meaning of the literal listener by a rhetorical function, one graded meaning per rhetorical strategy such as literalness, irony or hyperbole. A strategy-indexed literal listener, speaker and pragmatic listener run the standard pipeline (L0, S1, L1), and the listener averages the strategies under a strategy posterior given the utterance (listener).

Main results

• L1_indicator_apply_singleton_of_notMem, listener_apply_singleton_ne_zero_iff: standard RSA gives no mass to a meaning outside the literal extension of the utterance, while the listener gives a meaning of positive prior mass exactly when some strategy of positive posterior weight admits it at the utterance.
• L0_rhetoricalOfQUD, kaoGoodman2015_S1, kaoWuEtAl2014_S1: every literal listener of question-under-discussion RSA is the literal listener of a rhetorical function, at a prior that is positive everywhere, and the speakers of Kao and Goodman's irony model and of Kao and colleagues' hyperbole model are the framework's speakers at that function.
• exists_L0_ne_qudListener: over two or more meanings some literal listener of the framework is no literal listener of question-under-discussion RSA.
• literal_reading_iff: in the running example, the weather is amazing keeps its literal reading exactly when the strategy posterior gives the literal strategy weight.

Implementation notes

• The context of the paper's conditional probabilities indexes the prior, the utterance prior, the rhetorical functions and the strategy posterior. Every statement holds at a fixed context, so the context is not represented.
• Rhetorical functions take values in ℝ≥0∞ where the paper has the unit interval. The bound is a normalization (exists_le_one_and_L0_eq), and the two lemmas about question-under-discussion RSA are stated with it.
• The speaker pays a cost where the paper weighs utterances by a prior; S1_eq_ofWeights_prior gives the cost of a prior.
• The paper's first definition states the literal listener of question-under-discussion RSA as a distribution over meanings (qudListener). Kao and colleagues state it as a distribution over answers, the pushforward of the literal listener along the question. The two give a meaning's cell proportional mass. The constant depends on the utterance in general, and not when the cells of the question have one size, as those of a coordinate projection do (speaker_qudListener_dirac).

TODO

• The price experiment's rhetorical function, set by hand to one where the strategy fits the utterance to the price and to a thousandth elsewhere, the network-fitted function of the weather experiment, the comparison with affect-aware RSA on both, and the language-model listeners of the fifth section are not formalized.

References

• [SPAPC25]
• [KG15]
• [KWBG14]
• [FG12]

The framework

noncomputable def SpinosoDiPianoEtAl2025.L0 {M : Type u_1} {U : Type u_2} {R : Type u_3} [MeasurableSpace M] [MeasurableSpace U] [Fintype U] [DiscreteMeasurableSpace U] (μ : MeasureTheory.Measure M) (f : R → U → M → ENNReal) (r : R) : ProbabilityTheory.Kernel U M

The strategy-indexed literal listener (eq. 4) reweights the prior by the rhetorical function of the strategy.

Equations

• SpinosoDiPianoEtAl2025.L0 μ f r = ProbabilityTheory.Kernel.ofDensity μ (f r)

instance SpinosoDiPianoEtAl2025.instIsFiniteKernelL0 {M : Type u_1} {U : Type u_2} {R : Type u_3} [MeasurableSpace M] [MeasurableSpace U] [Fintype U] [DiscreteMeasurableSpace U] (μ : MeasureTheory.Measure M) (f : R → U → M → ENNReal) (r : R) : ProbabilityTheory.IsFiniteKernel (L0 μ f r)

theorem SpinosoDiPianoEtAl2025.exists_le_one_and_L0_eq {M : Type u_1} {U : Type u_2} {R : Type u_3} [MeasurableSpace M] [MeasurableSpace U] [Fintype M] [Fintype U] [DiscreteMeasurableSpace U] (μ : MeasureTheory.Measure M) {f : R → U → M → ENNReal} (hf : ∀ (r : R) (u : U) (m : M), f r u m ≠ ⊤) : ∃ (f' : R → U → M → ENNReal), (∀ (r : R) (u : U) (m : M), f' r u m ≤ 1) ∧ L0 μ f' = L0 μ f

The unit interval is no restriction on rhetorical functions. Dividing a finite function at each strategy and utterance by its largest value there bounds it by one and leaves the literal listeners unchanged, and with them the speakers and pragmatic listeners.

noncomputable def SpinosoDiPianoEtAl2025.S1 {M : Type u_1} {U : Type u_2} {R : Type u_3} [MeasurableSpace M] [MeasurableSpace U] [Fintype M] [Fintype U] [DiscreteMeasurableSpace U] [DiscreteMeasurableSpace M] (μ : MeasureTheory.Measure M) (f : R → U → M → ENNReal) (α : ℝ) (κ : U → ℝ) (r : R) : ProbabilityTheory.Kernel M U

The strategy-indexed speaker (eq. 5) is the best response to the strategy's literal listener, less the utterance cost.

Equations

• SpinosoDiPianoEtAl2025.S1 μ f α κ r = RSA.speaker α κ (⇑(SpinosoDiPianoEtAl2025.L0 μ f r)) MeasureTheory.Measure.dirac

instance SpinosoDiPianoEtAl2025.instIsFiniteKernelS1 {M : Type u_1} {U : Type u_2} {R : Type u_3} [MeasurableSpace M] [MeasurableSpace U] [Fintype M] [Fintype U] [DiscreteMeasurableSpace U] [DiscreteMeasurableSpace M] (μ : MeasureTheory.Measure M) (f : R → U → M → ENNReal) (α : ℝ) (κ : U → ℝ) (r : R) : ProbabilityTheory.IsFiniteKernel (S1 μ f α κ r)

noncomputable def SpinosoDiPianoEtAl2025.L1 {M : Type u_1} {U : Type u_2} {R : Type u_3} [MeasurableSpace M] [MeasurableSpace U] [Fintype M] [Fintype U] [DiscreteMeasurableSpace U] [DiscreteMeasurableSpace M] (μ : MeasureTheory.Measure M) (f : R → U → M → ENNReal) (α : ℝ) (κ : U → ℝ) (r : R) : ProbabilityTheory.Kernel U M

The strategy-indexed pragmatic listener (eq. 6).

Equations

• SpinosoDiPianoEtAl2025.L1 μ f α κ r = RSA.listener μ ⇑(SpinosoDiPianoEtAl2025.S1 μ f α κ r)

noncomputable def SpinosoDiPianoEtAl2025.listener {M : Type u_1} {U : Type u_2} {R : Type u_3} [MeasurableSpace M] [MeasurableSpace U] [Fintype M] [Fintype U] [DiscreteMeasurableSpace U] [DiscreteMeasurableSpace M] [MeasurableSpace R] (μ : MeasureTheory.Measure M) (f : R → U → M → ENNReal) (α : ℝ) (κ : U → ℝ) (ρ : ProbabilityTheory.Kernel U R) : ProbabilityTheory.Kernel U M

The pragmatic listener (eq. 7) averages the strategy-indexed listeners under the strategy posterior given the utterance.

Equations

• SpinosoDiPianoEtAl2025.listener μ f α κ ρ = ProbabilityTheory.Kernel.ofFunOfCountable fun (u : U) => (ρ u).bind fun (r : R) => (SpinosoDiPianoEtAl2025.L1 μ f α κ r) u

theorem SpinosoDiPianoEtAl2025.S1_eq_ofWeights_prior {M : Type u_1} {U : Type u_2} {R : Type u_3} [MeasurableSpace M] [MeasurableSpace U] [Fintype M] [Fintype U] [DiscreteMeasurableSpace U] [DiscreteMeasurableSpace M] (μ : MeasureTheory.Measure M) (f : R → U → M → ENNReal) (α : ℝ) (hα : α ≠ 0) {π : U → ENNReal} (hπ0 : ∀ (u : U), π u ≠ 0) (hπ : ∀ (u : U), π u ≠ ⊤) (r : R) : S1 μ f α (fun (u : U) => -Real.log (π u).toReal / α) r = ProbabilityTheory.Kernel.ofWeights fun (m : M) (u : U) => ((L0 μ f r) u) {m} ^ α * π u

The speaker with an utterance prior is the speaker with a cost (Appendix A.1). At rationality α ≠ 0 and the cost −log π / α, the speaker's weights are the literal listener's mass to the power α times the utterance prior π. Conversely RSA.speaker_dirac_eq_ofWeights reads the cost weight exp (-(α * κ u)) of any cost as an unnormalized utterance prior.

theorem SpinosoDiPianoEtAl2025.L1_indicator {M : Type u_1} {U : Type u_2} {R : Type u_3} [MeasurableSpace M] [MeasurableSpace U] [Fintype M] [Fintype U] [DiscreteMeasurableSpace U] [DiscreteMeasurableSpace M] (μ : MeasureTheory.Measure M) (f : R → U → M → ENNReal) (α : ℝ) (κ : U → ℝ) (sem : U → Set M) {r : R} (hr : f r = fun (u : U) => (sem u).indicator 1) : L1 μ f α κ r = RSA.listener μ ⇑(RSA.speaker α κ (⇑(RSA.listener μ (RSA.truthful sem))) MeasureTheory.Measure.dirac)

A strategy whose rhetorical function is a Boolean meaning runs standard RSA on it.

theorem SpinosoDiPianoEtAl2025.L1_indicator_apply_singleton_of_notMem {M : Type u_1} {U : Type u_2} {R : Type u_3} [MeasurableSpace M] [MeasurableSpace U] [Fintype M] [Fintype U] [DiscreteMeasurableSpace U] [DiscreteMeasurableSpace M] (μ : MeasureTheory.Measure M) (f : R → U → M → ENNReal) (α : ℝ) (κ : U → ℝ) (hα : 0 < α) (sem : U → Set M) {r : R} (hr : f r = fun (u : U) => (sem u).indicator 1) {u : U} {m : M} (hm : m ∉ sem u) : ((L1 μ f α κ r) u) {m} = 0

Standard RSA gives no mass to non-literal meanings (Appendix A.2). Under a strategy whose rhetorical function is a Boolean meaning, a meaning outside the extension of the utterance has no listener mass.

theorem SpinosoDiPianoEtAl2025.listener_apply_singleton {M : Type u_1} {U : Type u_2} {R : Type u_3} [MeasurableSpace M] [MeasurableSpace U] [Fintype M] [Fintype U] [DiscreteMeasurableSpace U] [DiscreteMeasurableSpace M] (μ : MeasureTheory.Measure M) (f : R → U → M → ENNReal) (α : ℝ) (κ : U → ℝ) [Fintype R] [MeasurableSpace R] [DiscreteMeasurableSpace R] (ρ : ProbabilityTheory.Kernel U R) (u : U) (m : M) : ((listener μ f α κ ρ) u) {m} = ∑ r : R, ((L1 μ f α κ r) u) {m} * (ρ u) {r}

theorem SpinosoDiPianoEtAl2025.L1_apply_singleton_ne_zero_iff {M : Type u_1} {U : Type u_2} {R : Type u_3} [MeasurableSpace M] [MeasurableSpace U] [Fintype M] [Fintype U] [DiscreteMeasurableSpace U] [DiscreteMeasurableSpace M] (μ : MeasureTheory.Measure M) (f : R → U → M → ENNReal) (α : ℝ) (κ : U → ℝ) [MeasureTheory.IsFiniteMeasure μ] (hα : 0 < α) {r : R} {u : U} (hf : ∀ (m : M), f r u m ≠ ⊤) (m : M) : ((L1 μ f α κ r) u) {m} ≠ 0 ↔ f r u m ≠ 0 ∧ μ {m} ≠ 0

A strategy's pragmatic listener puts positive mass on a meaning exactly when the prior does and the strategy's rhetorical function admits the meaning at the utterance, so the framework escapes the literal extension.

theorem SpinosoDiPianoEtAl2025.listener_apply_singleton_ne_zero_iff {M : Type u_1} {U : Type u_2} {R : Type u_3} [MeasurableSpace M] [MeasurableSpace U] [Fintype M] [Fintype U] [DiscreteMeasurableSpace U] [DiscreteMeasurableSpace M] (μ : MeasureTheory.Measure M) (f : R → U → M → ENNReal) (α : ℝ) (κ : U → ℝ) [MeasureTheory.IsFiniteMeasure μ] [Fintype R] [MeasurableSpace R] [DiscreteMeasurableSpace R] (hα : 0 < α) {u : U} (hf : ∀ (r : R) (m : M), f r u m ≠ ⊤) (ρ : ProbabilityTheory.Kernel U R) (m : M) : ((listener μ f α κ ρ) u) {m} ≠ 0 ↔ μ {m} ≠ 0 ∧ ∃ (r : R), (ρ u) {r} ≠ 0 ∧ f r u m ≠ 0

The pragmatic listener interprets an utterance as a meaning exactly when the meaning has positive prior and some strategy of positive posterior weight admits it at the utterance.

Question-under-discussion RSA as a special case

noncomputable def SpinosoDiPianoEtAl2025.rhetoricalOfQUD {M : Type u_1} {U : Type u_2} [MeasurableSpace M] [MeasurableSpace U] {G : Type u_4} {X : Type u_5} (μ : MeasureTheory.Measure M) (L : ProbabilityTheory.Kernel U M) (q : G → M → X) (g : G) (u : U) (m : M) : ENNReal

The rhetorical function of a question (eq. 19) is the literal mass of the meaning's cell over the prior mass of the meaning, divided by its largest value at the utterance.

Equations

• SpinosoDiPianoEtAl2025.rhetoricalOfQUD μ L q g u m = (L u) (q g ⁻¹' {q g m}) / μ {m} / ⨆ (m' : M), (L u) (q g ⁻¹' {q g m'}) / μ {m'}

theorem SpinosoDiPianoEtAl2025.rhetoricalOfQUD_le_one {M : Type u_1} {U : Type u_2} [MeasurableSpace M] [MeasurableSpace U] {G : Type u_4} {X : Type u_5} (μ : MeasureTheory.Measure M) (L : ProbabilityTheory.Kernel U M) (q : G → M → X) (g : G) (u : U) (m : M) : rhetoricalOfQUD μ L q g u m ≤ 1

noncomputable def SpinosoDiPianoEtAl2025.qudListener {M : Type u_1} {U : Type u_2} [MeasurableSpace M] [MeasurableSpace U] {X : Type u_5} [Fintype M] [Fintype U] [DiscreteMeasurableSpace U] (L : ProbabilityTheory.Kernel U M) (q : M → X) : ProbabilityTheory.Kernel U M

The literal listener of question-under-discussion RSA (eq. 13) gives a meaning mass proportional to the literal listener's mass on the meanings with the same answer.

Equations

• SpinosoDiPianoEtAl2025.qudListener L q = ProbabilityTheory.Kernel.ofWeights fun (u : U) (m : M) => (L u) (q ⁻¹' {q m})

theorem SpinosoDiPianoEtAl2025.L0_rhetoricalOfQUD {M : Type u_1} {U : Type u_2} [MeasurableSpace M] [MeasurableSpace U] {G : Type u_4} {X : Type u_5} [Fintype M] [DiscreteMeasurableSpace M] [Fintype U] [DiscreteMeasurableSpace U] (μ : MeasureTheory.Measure M) [MeasureTheory.IsFiniteMeasure μ] (hμ : ∀ (m : M), μ {m} ≠ 0) (L : ProbabilityTheory.Kernel U M) [ProbabilityTheory.IsFiniteKernel L] (q : G → M → X) (g : G) : L0 μ (rhetoricalOfQUD μ L q) g = qudListener L (q g)

The literal listener of question-under-discussion RSA under a question is the literal listener of the question's rhetorical function, at a prior of positive mass everywhere (Lemma 1). The speaker and the pragmatic listener of a question are built from its literal listener as the framework's are, so they agree as well.

Questions with cells of one size

The cells of a coordinate projection all have one size. The literal listener over meanings is then the listener over answers up to a constant, so the speakers who address them agree.

theorem SpinosoDiPianoEtAl2025.qudListener_apply_singleton_of_ncard {M : Type u_1} {U : Type u_2} [MeasurableSpace M] [MeasurableSpace U] {X : Type u_5} [Fintype M] [DiscreteMeasurableSpace M] [Fintype U] [DiscreteMeasurableSpace U] (L : ProbabilityTheory.Kernel U M) [∀ (u : U), MeasureTheory.IsZeroOrProbabilityMeasure (L u)] (q : M → X) {n : ℕ} (hq : ∀ (m : M), (q ⁻¹' {q m}).ncard = n) (u : U) (m : M) : ((qudListener L q) u) {m} = (L u) (q ⁻¹' {q m}) / ↑n

theorem SpinosoDiPianoEtAl2025.speaker_qudListener_dirac {M : Type u_1} {U : Type u_2} [MeasurableSpace M] [MeasurableSpace U] {X : Type u_5} [Fintype M] [DiscreteMeasurableSpace M] [Fintype U] [DiscreteMeasurableSpace U] (L : ProbabilityTheory.Kernel U M) [∀ (u : U), MeasureTheory.IsZeroOrProbabilityMeasure (L u)] (q : M → X) {n : ℕ} (hq : ∀ (m : M), (q ⁻¹' {q m}).ncard = n) [Fintype X] [MeasurableSpace X] [MeasurableSingletonClass X] {α : ℝ} (hα : 0 ≤ α) (κ : U → ℝ) (m : M) : (RSA.speaker α κ (⇑(qudListener L q)) MeasureTheory.Measure.dirac) m = (RSA.speaker α κ (⇑(L.map q)) MeasureTheory.Measure.dirac) (q m)

At a question whose cells have one size, the speaker who addresses the literal listener of question-under-discussion RSA over meanings is the speaker who is informative about the answer, RSA.speaker at the pushforward of the literal listener along the question.

The affect-aware models

The questions of Kao and Goodman's irony model and the goals of Kao and colleagues' hyperbole model have cells of one size, so the speakers of both are speakers of the framework.

theorem SpinosoDiPianoEtAl2025.kaoGoodman2015_S1 (μ : MeasureTheory.Measure KaoGoodman2015.Meaning) [MeasureTheory.IsFiniteMeasure μ] (hμ : ∀ (m : KaoGoodman2015.Meaning), μ {m} ≠ 0) {α : ℝ} (hα : 0 ≤ α) (m : KaoGoodman2015.Meaning) (q : KaoGoodman2015.QUD) : KaoGoodman2015.S1 μ α (m, q) = (S1 μ (rhetoricalOfQUD μ (KaoGoodman2015.L0 μ) KaoGoodman2015.project) α 0 q) m

The question-indexed speaker of Kao and Goodman's irony model is the framework's speaker at the rhetorical function of the question, at a prior of positive mass everywhere.

theorem SpinosoDiPianoEtAl2025.kaoWuEtAl2014_S1 (μ : MeasureTheory.Measure KaoWuEtAl2014.Meaning) [MeasureTheory.IsFiniteMeasure μ] (hμ : ∀ (m : KaoWuEtAl2014.Meaning), μ {m} ≠ 0) (c : ℝ) (m : KaoWuEtAl2014.Meaning) (g : KaoWuEtAl2014.Goal) : KaoWuEtAl2014.S1 μ c (m, g) = (S1 μ (rhetoricalOfQUD μ (KaoWuEtAl2014.L0 μ) KaoWuEtAl2014.project) 1 (KaoWuEtAl2014.cost c) g) m

The goal-indexed speaker of Kao and colleagues' hyperbole model is the framework's speaker at the rhetorical function of the goal, at a prior of positive mass everywhere.

A literal listener beyond question-under-discussion RSA

theorem SpinosoDiPianoEtAl2025.finite_setOf_qudListener {M : Type u_1} {U : Type u_2} [MeasurableSpace M] [MeasurableSpace U] [Fintype M] [DiscreteMeasurableSpace M] [Fintype U] [DiscreteMeasurableSpace U] (μ : MeasureTheory.Measure M) : {ν : MeasureTheory.Measure M | ∃ (sem : U → Set M) (X : Type u_6) (q : M → X) (u : U), ν = (qudListener (RSA.listener μ (RSA.truthful sem)) q) u}.Finite

At a prior there are finitely many literal listeners of question-under-discussion RSA, over every Boolean meaning, question and utterance (eq. 24), since each is fixed by the extension of the utterance and the cells of the question.

theorem SpinosoDiPianoEtAl2025.exists_L0_ne_qudListener {M : Type u_1} {U : Type u_2} {R : Type u_3} [MeasurableSpace M] [MeasurableSpace U] [Fintype M] [DiscreteMeasurableSpace M] [Fintype U] [DiscreteMeasurableSpace U] [Nontrivial M] (μ : MeasureTheory.Measure M) [MeasureTheory.IsFiniteMeasure μ] (hμ : ∀ (m : M), μ {m} ≠ 0) : ∃ (f : R → U → M → ENNReal), (∀ (r : R) (u : U) (m : M), f r u m ≤ 1) ∧ ∀ (sem : U → Set M) {X : Type u_6} (q : M → X) (r : R) (u u' : U), (L0 μ f r) u ≠ (qudListener (RSA.listener μ (RSA.truthful sem)) q) u'

Over two or more meanings, at a prior of positive mass everywhere, some literal listener of the framework is no literal listener of question-under-discussion RSA at any Boolean meaning, question and utterance, since the latter are finitely many and the former realize every distribution (Lemma 2).

The running example

A speaker says the weather is amazing in a blizzard. The paper gives the rhetorical functions of irony and hyperbole at this utterance at two meanings each, and the statements assume no more of them.

inductive SpinosoDiPianoEtAl2025.WeatherStrategy : Type

The rhetorical strategies of the running example.

• literal : WeatherStrategy
• irony : WeatherStrategy
• hyperbole : WeatherStrategy

@[instance_reducible]

instance SpinosoDiPianoEtAl2025.instDecidableEqWeatherStrategy : DecidableEq WeatherStrategy

Equations

• SpinosoDiPianoEtAl2025.instDecidableEqWeatherStrategy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance SpinosoDiPianoEtAl2025.instReprWeatherStrategy : Repr WeatherStrategy

Equations

• SpinosoDiPianoEtAl2025.instReprWeatherStrategy = { reprPrec := SpinosoDiPianoEtAl2025.instReprWeatherStrategy.repr }

def SpinosoDiPianoEtAl2025.instReprWeatherStrategy.repr : WeatherStrategy → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance SpinosoDiPianoEtAl2025.instFintypeWeatherStrategy : Fintype WeatherStrategy

Equations

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

@[instance_reducible]

instance SpinosoDiPianoEtAl2025.instMeasurableSpaceWeatherStrategy : MeasurableSpace WeatherStrategy

Equations

• SpinosoDiPianoEtAl2025.instMeasurableSpaceWeatherStrategy = ⊤

instance SpinosoDiPianoEtAl2025.instDiscreteMeasurableSpaceWeatherStrategy : DiscreteMeasurableSpace WeatherStrategy

theorem SpinosoDiPianoEtAl2025.literal_strategy_apply_eq_zero (μ : MeasureTheory.Measure KaoGoodman2015.Weather) (f : WeatherStrategy → KaoGoodman2015.Weather → KaoGoodman2015.Weather → ENNReal) (α : ℝ) (κ : KaoGoodman2015.Weather → ℝ) (hα : 0 < α) (hliteral : f WeatherStrategy.literal = fun (u : KaoGoodman2015.Weather) => {u}.indicator 1) {m : KaoGoodman2015.Weather} (hm : m ≠ KaoGoodman2015.Weather.amazing) : ((L1 μ f α κ WeatherStrategy.literal) KaoGoodman2015.Weather.amazing) {m} = 0

Under the literal strategy, where an utterance is true of the state it names, the weather is amazing leaves every other state without mass, the standard RSA prediction.

theorem SpinosoDiPianoEtAl2025.literal_reading_iff (μ : MeasureTheory.Measure KaoGoodman2015.Weather) (f : WeatherStrategy → KaoGoodman2015.Weather → KaoGoodman2015.Weather → ENNReal) (α : ℝ) (κ : KaoGoodman2015.Weather → ℝ) [MeasureTheory.IsFiniteMeasure μ] (ρ : ProbabilityTheory.Kernel KaoGoodman2015.Weather WeatherStrategy) (hα : 0 < α) (hf : ∀ (r : WeatherStrategy) (m : KaoGoodman2015.Weather), f r KaoGoodman2015.Weather.amazing m ≠ ⊤) (hliteral : f WeatherStrategy.literal KaoGoodman2015.Weather.amazing KaoGoodman2015.Weather.amazing ≠ 0) (hirony : f WeatherStrategy.irony KaoGoodman2015.Weather.amazing KaoGoodman2015.Weather.amazing = 0) (hhyperbole : f WeatherStrategy.hyperbole KaoGoodman2015.Weather.amazing KaoGoodman2015.Weather.amazing = 0) (hμ : μ {KaoGoodman2015.Weather.amazing} ≠ 0) : ((listener μ f α κ ρ) KaoGoodman2015.Weather.amazing) {KaoGoodman2015.Weather.amazing} ≠ 0 ↔ (ρ KaoGoodman2015.Weather.amazing) {WeatherStrategy.literal} ≠ 0

The listener keeps the literal reading of the weather is amazing exactly when the strategy posterior gives the literal strategy weight, since the ironic and the hyperbolic strategy both exclude amazing weather at this utterance.

theorem SpinosoDiPianoEtAl2025.ironic_reading (μ : MeasureTheory.Measure KaoGoodman2015.Weather) (f : WeatherStrategy → KaoGoodman2015.Weather → KaoGoodman2015.Weather → ENNReal) (α : ℝ) (κ : KaoGoodman2015.Weather → ℝ) [MeasureTheory.IsFiniteMeasure μ] (ρ : ProbabilityTheory.Kernel KaoGoodman2015.Weather WeatherStrategy) (hα : 0 < α) (hf : ∀ (r : WeatherStrategy) (m : KaoGoodman2015.Weather), f r KaoGoodman2015.Weather.amazing m ≠ ⊤) (hirony : f WeatherStrategy.irony KaoGoodman2015.Weather.amazing KaoGoodman2015.Weather.terrible ≠ 0) (hμ : μ {KaoGoodman2015.Weather.terrible} ≠ 0) (hρ : (ρ KaoGoodman2015.Weather.amazing) {WeatherStrategy.irony} ≠ 0) : ((listener μ f α κ ρ) KaoGoodman2015.Weather.amazing) {KaoGoodman2015.Weather.terrible} ≠ 0

The listener reads the weather is amazing as terrible weather once the strategy posterior gives weight to irony, which admits terrible weather at this utterance.

theorem SpinosoDiPianoEtAl2025.hyperbolic_reading (μ : MeasureTheory.Measure KaoGoodman2015.Weather) (f : WeatherStrategy → KaoGoodman2015.Weather → KaoGoodman2015.Weather → ENNReal) (α : ℝ) (κ : KaoGoodman2015.Weather → ℝ) [MeasureTheory.IsFiniteMeasure μ] (ρ : ProbabilityTheory.Kernel KaoGoodman2015.Weather WeatherStrategy) (hα : 0 < α) (hf : ∀ (r : WeatherStrategy) (m : KaoGoodman2015.Weather), f r KaoGoodman2015.Weather.amazing m ≠ ⊤) (hhyperbole : f WeatherStrategy.hyperbole KaoGoodman2015.Weather.amazing KaoGoodman2015.Weather.good ≠ 0) (hμ : μ {KaoGoodman2015.Weather.good} ≠ 0) (hρ : (ρ KaoGoodman2015.Weather.amazing) {WeatherStrategy.hyperbole} ≠ 0) : ((listener μ f α κ ρ) KaoGoodman2015.Weather.amazing) {KaoGoodman2015.Weather.good} ≠ 0

The listener reads the weather is amazing as good weather once the strategy posterior gives weight to hyperbole, which admits good weather at this utterance.