QUD-projected aggregation for RSA pragmatic models

A Question Under Discussion (QUD) partitions worlds via a projection project : G → W → β — two worlds are QUD-equivalent under goal g iff they project to the same value. The QUD-projected aggregation of a non-negative weight function sums the weight over the equivalence class.

This is the architectural primitive shared by all Kao-family RSA models (metaphor, hyperbole, irony): the speaker's "informativeness" along a QUD dimension is the projected weight at the literally-true world. A literally-false utterance can have positive QUD-projected mass at a world w iff some QUD-equivalent world w' is literally true — this is the architectural mechanism for nonliteral interpretation.

Main definition

• RSA.QUD.proj project weight g w — sum of weight w' over all w' with project g w' = project g w.

Main theorems

• RSA.QUD.self_le_proj — the world is in its own equivalence class, so weight w ≤ proj project weight g w.
• RSA.QUD.proj_pos_iff_exists_class_member — positive iff some equivalence-class member has positive weight (the headline lemma for nonliteral interpretation).
• RSA.QUD.proj_le_total — bounded by the total weight.
• RSA.QUD.proj_le_one_of_pmf — when the weight is a PMF, bounded by 1.

Anchoring

QUD-projection in RSA was introduced by @cite{goodman-stuhlmueller-2013} and is used by @cite{kao-bergen-goodman-2014} (metaphor), @cite{kao-wu-bergen-goodman-2014} (hyperbole), @cite{kao-goodman-2015} (irony), and the broader Kao family.

noncomputable def RSA.QUD.proj {W : Type u_1} {G : Type u_2} {β : Type u_3} [Fintype W] [DecidableEq β] (project : G → W → β) (weight : W → ENNReal) (g : G) (w : W) : ENNReal

QUD-projected aggregation: sum of weight w' over the QUD-equivalence class of w under projection project g.

Equations

• RSA.QUD.proj project weight g w = ∑ w' : W with project g w' = project g w, weight w'

theorem RSA.QUD.self_le_proj {W : Type u_1} {G : Type u_2} {β : Type u_3} [Fintype W] [DecidableEq β] (project : G → W → β) (weight : W → ENNReal) (g : G) (w : W) : weight w ≤ proj project weight g w

The world w is in its own QUD-equivalence class, so its weight provides a lower bound on the QUD-projected aggregation.

theorem RSA.QUD.proj_pos_iff_exists_class_member {W : Type u_1} {G : Type u_2} {β : Type u_3} [Fintype W] [DecidableEq β] (project : G → W → β) (weight : W → ENNReal) (g : G) (w : W) : 0 < proj project weight g w ↔ ∃ w' ∈ {w' : W | project g w' = project g w}, 0 < weight w'

Headline lemma: the QUD-projected aggregation is positive iff some world in the same QUD-equivalence class has positive weight.

This is the architectural mechanism for nonliteral interpretation across the Kao family (metaphor, hyperbole, irony): a literally-false utterance has positive projected mass at world w iff there exists a QUD-equivalent world w' (potentially differing on non-QUD dimensions) that IS literally true.

theorem RSA.QUD.proj_le_total {W : Type u_1} {G : Type u_2} {β : Type u_3} [Fintype W] [DecidableEq β] (project : G → W → β) (weight : W → ENNReal) (g : G) (w : W) : proj project weight g w ≤ ∑ w' : W, weight w'

The QUD-projected aggregation is bounded by the total weight.

theorem RSA.QUD.proj_le_one_of_pmf {W : Type u_1} {G : Type u_2} {β : Type u_3} [Fintype W] [DecidableEq β] (project : G → W → β) (p : PMF W) (g : G) (w : W) : proj project (⇑p) g w ≤ 1

When the weight is a PMF, the QUD-projected aggregation is bounded by 1 (the equivalence class is a subset of the support).

theorem RSA.QUD.proj_ne_top_of_pmf {W : Type u_1} {G : Type u_2} {β : Type u_3} [Fintype W] [DecidableEq β] (project : G → W → β) (p : PMF W) (g : G) (w : W) : proj project (⇑p) g w ≠ ⊤

When the weight is a PMF, the QUD-projected aggregation is finite.