Speakers who address a question

A question under discussion is a function q : W → X from states to answers. Kao and colleagues let the speaker be informative about the answer alone: the listener's belief about the answer is the pushforward L.map q of his belief about the state, and the speaker, who knows the answer q w at her state, is RSA.speaker α C (L.map q) Measure.dirac (q w). With the question as a coordinate of the state, the listener who does not know which question she addresses is RSA.listener over pairs of a state and a question.

An utterance that is false at a state can then be produced there, when it is true at a state with the same answer, which is how the model derives hyperbole, metaphor and irony.

Main results

• RSA.listener_truthful_map_apply_singleton: a literal listener's probability of an answer is the prior mass of the states with that answer where the utterance is true, over the prior mass of the states where it is true.
• RSA.speaker_map_dirac_apply_singleton_ne_zero_iff: the speaker produces an utterance exactly when its listener gives mass to a state with the same answer as hers.
• RSA.listener_prod_speaker_map_dirac_fst_apply_singleton_ne_zero_iff: the listener takes a state to be possible exactly when it has positive prior and, under some question of positive prior, shares its answer with a state the literal listener gives mass.

References

• [KWBG14]
• [KBG14]
• [KG15]

theorem RSA.listener_truthful_map_apply_singleton {W : Type u_1} {U : Type u_2} {X : Type u_3} [MeasurableSpace W] [MeasurableSpace U] [MeasurableSingletonClass U] [MeasurableSpace X] [MeasurableSingletonClass X] [Countable W] [DiscreteMeasurableSpace W] [Countable U] (μ : MeasureTheory.Measure W) (sem : U → Set W) (q : W → X) (u : U) (x : X) : (((listener μ (truthful sem)).map q) u) {x} = μ (sem u ∩ q ⁻¹' {x}) / μ (sem u)

A literal listener's probability of an answer is the prior mass of the states with that answer where the utterance is true, over the prior mass of the states where it is true.

theorem RSA.speaker_map_dirac_apply_singleton_ne_zero_iff {W : Type u_1} {U : Type u_2} {X : Type u_3} [MeasurableSpace W] [MeasurableSpace U] [MeasurableSingletonClass U] [MeasurableSpace X] [MeasurableSingletonClass X] [Fintype W] [MeasurableSingletonClass W] [Fintype U] [Fintype X] {α : ℝ} (hα : 0 < α) (C : U → ℝ) (L : ProbabilityTheory.Kernel U W) [ProbabilityTheory.IsFiniteKernel L] (q : W → X) (w : W) (u : U) : ((speaker α C (⇑(L.map q)) MeasureTheory.Measure.dirac) (q w)) {u} ≠ 0 ↔ ∃ (w' : W), q w' = q w ∧ (L u) {w'} ≠ 0

The speaker who addresses a question produces an utterance exactly when its listener gives mass to a state with the same answer as hers.

theorem RSA.listener_prod_speaker_map_dirac_fst_apply_singleton_ne_zero_iff {W : Type u_1} {U : Type u_2} {X : Type u_3} {G : Type u_4} [MeasurableSpace W] [MeasurableSpace U] [MeasurableSingletonClass U] [MeasurableSpace X] [MeasurableSingletonClass X] [Fintype W] [MeasurableSingletonClass W] [Fintype U] [Fintype X] {α : ℝ} [Fintype G] [MeasurableSpace G] [MeasurableSingletonClass G] (hα : 0 < α) (C : U → ℝ) (L : ProbabilityTheory.Kernel U W) [ProbabilityTheory.IsFiniteKernel L] (q : G → W → X) (μ : MeasureTheory.Measure W) [MeasureTheory.IsFiniteMeasure μ] (ν : MeasureTheory.Measure G) [MeasureTheory.IsFiniteMeasure ν] (u : U) (w : W) : ((listener (μ.prod ν) fun (p : W × G) => (speaker α C (⇑(L.map (q p.2))) MeasureTheory.Measure.dirac) (q p.2 p.1)) u).fst {w} ≠ 0 ↔ μ {w} ≠ 0 ∧ ∃ (g : G), ν {g} ≠ 0 ∧ ∃ (w' : W), q g w' = q g w ∧ (L u) {w'} ≠ 0

The listener who does not know which question the speaker addresses takes a state to be possible exactly when it has positive prior and, under some question of positive prior, shares its answer with a state the literal listener gives mass.