Speakers with beliefs

A speaker who does not know the state believes a measure on states. RSA.speaker scores an utterance by the expected log-probability its listener gives the state under that belief, as Goodman and Stuhlmüller do. This file relates that score to the Kullback–Leibler divergence of the listener's posterior from the belief: the two differ by the entropy of the belief, which no utterance changes, so they define the same speaker. It then treats the speaker whose belief is a prior conditioned on what she knows.

Main results

• RSA.speaker_eq_softmax_sum_log, RSA.speaker_eq_softmax_klDiv: the speaker is the softmax of the expected log-probability the listener gives the state under her belief, and of the negative divergence of the listener from her belief.
• RSA.speaker_cond_ofDensity_apply_eq: a speaker who knows an event on which every graded meaning is constant sees the listener only through those constants.
• RSA.speaker_cond_listener_truthful_apply_eq, RSA.speaker_zero_cond_listener_truthful_real_singleton_lt_iff: a speaker whose belief is the prior conditioned on what she knows depends on it, against a literal listener, only through the utterances it entails, and among those prefers the one of smaller prior mass.

References

• [GS13]

theorem RSA.speaker_eq_softmax_sum_log {W : Type u_1} {U : Type u_2} {O : Type u_3} [MeasurableSpace W] [Fintype W] {α : ℝ} {C : U → ℝ} {L : U → MeasureTheory.Measure W} {b : O → MeasureTheory.Measure W} [MeasurableSpace U] [Fintype U] [MeasurableSpace O] [Countable O] [MeasurableSingletonClass O] [∀ (u : U), MeasureTheory.IsFiniteMeasure (L u)] (h : ∀ (o : O) (u : U), (b o).AbsolutelyContinuous (L u)) : speaker α C L b = ProbabilityTheory.Kernel.softmax fun (o : O) (u : U) => ↑(α * (∑ w : W, (b o).real {w} * Real.log ((L u).real {w}) - C u))

When every listener dominates every belief, the speaker is the softmax of the expected log-probability the listener gives the state under the belief, less the cost.

theorem RSA.speaker_apply_singleton_eq_zero_iff_not_ac {W : Type u_1} {U : Type u_2} {O : Type u_3} [MeasurableSpace W] [Fintype W] {α : ℝ} {C : U → ℝ} {L : U → MeasureTheory.Measure W} {b : O → MeasureTheory.Measure W} {o : O} {u : U} [MeasurableSpace U] [Fintype U] [MeasurableSpace O] [Countable O] [MeasurableSingletonClass O] [MeasurableSingletonClass U] [MeasureTheory.IsFiniteMeasure (b o)] [∀ (u : U), MeasureTheory.IsFiniteMeasure (L u)] (hα : 0 < α) : ((speaker α C L b) o) {u} = 0 ↔ ¬(b o).AbsolutelyContinuous (L u)

theorem RSA.speaker_eq_softmax_klDiv {W : Type u_1} {U : Type u_2} {O : Type u_3} [MeasurableSpace W] [Fintype W] {α : ℝ} {C : U → ℝ} {L : U → MeasureTheory.Measure W} {b : O → MeasureTheory.Measure W} [MeasurableSpace U] [Fintype U] [MeasurableSpace O] [Countable O] [MeasurableSingletonClass O] [MeasurableSingletonClass U] [MeasurableSingletonClass W] [∀ (o : O), MeasureTheory.IsProbabilityMeasure (b o)] [∀ (u : U), MeasureTheory.IsZeroOrProbabilityMeasure (L u)] (hα : 0 < α) : speaker α C L b = ProbabilityTheory.Kernel.softmax fun (o : O) (u : U) => -↑(ENNReal.ofReal α * InformationTheory.klDiv (b o) (L u)) - ↑(α * C u)

For probability beliefs the speaker is the softmax of the negative Kullback–Leibler divergence of the listener from the belief, less the cost, since the divergence and the expected log-probability differ by the entropy of the belief, which no utterance changes.

theorem RSA.speaker_zero_real_singleton_lt_iff_klDiv {W : Type u_1} {U : Type u_2} {O : Type u_3} [MeasurableSpace W] [Fintype W] {α : ℝ} {L : U → MeasureTheory.Measure W} {b : O → MeasureTheory.Measure W} {o : O} {u u' : U} [MeasurableSpace U] [Fintype U] [MeasurableSpace O] [Countable O] [MeasurableSingletonClass O] [MeasurableSingletonClass U] [MeasurableSingletonClass W] [MeasureTheory.IsProbabilityMeasure (b o)] [∀ (u : U), MeasureTheory.IsZeroOrProbabilityMeasure (L u)] (hα : 0 < α) (h : ∃ (u : U), InformationTheory.klDiv (b o) (L u) ≠ ⊤) : ((speaker α 0 L b) o).real {u} < ((speaker α 0 L b) o).real {u'} ↔ InformationTheory.klDiv (b o) (L u') < InformationTheory.klDiv (b o) (L u)

At no cost the speaker prefers the utterance whose listener is closer to her belief.

Knowledge against a literal listener

A speaker who knows only that the state lies in an event believes the prior conditioned on it. Against a literal listener she produces exactly the utterances her knowledge entails, and among them prefers the one whose extension has the smaller prior mass.

theorem RSA.speaker_cond_listener_truthful_apply_singleton_eq_zero_iff {W : Type u_1} {U : Type u_2} {O : Type u_3} [MeasurableSpace W] [Fintype W] {α : ℝ} {C : U → ℝ} {o : O} {u : U} [MeasurableSpace U] [Fintype U] [MeasurableSpace O] [Countable O] [MeasurableSingletonClass O] [MeasurableSingletonClass U] [MeasurableSingletonClass W] {μ : MeasureTheory.Measure W} [MeasureTheory.IsFiniteMeasure μ] {A : O → Set W} {sem : U → Set W} (hα : 0 < α) : ((speaker α C ⇑(listener μ (truthful sem)) fun (o : O) => μ[|A o]) o) {u} = 0 ↔ ¬A o ≤ᵐ[μ] sem u

The speaker produces exactly the utterances her knowledge entails.

theorem RSA.speaker_zero_cond_listener_truthful_real_singleton_lt_iff {W : Type u_1} {U : Type u_2} {O : Type u_3} [MeasurableSpace W] [Fintype W] {α : ℝ} {o : O} {u u' : U} [MeasurableSpace U] [Fintype U] [MeasurableSpace O] [Countable O] [MeasurableSingletonClass O] [MeasurableSingletonClass U] [MeasurableSingletonClass W] {μ : MeasureTheory.Measure W} [MeasureTheory.IsFiniteMeasure μ] {A : O → Set W} {sem : U → Set W} (hα : 0 < α) (hA : μ (A o) ≠ 0) (hu : A o ≤ᵐ[μ] sem u) (hu' : A o ≤ᵐ[μ] sem u') : ((speaker α 0 ⇑(listener μ (truthful sem)) fun (o : O) => μ[|A o]) o).real {u} < ((speaker α 0 ⇑(listener μ (truthful sem)) fun (o : O) => μ[|A o]) o).real {u'} ↔ μ (sem u') < μ (sem u)

Among the utterances her knowledge entails, the speaker prefers the one of smaller prior mass.

theorem RSA.speaker_cond_ofDensity_apply_eq {W : Type u_1} {U : Type u_2} {O : Type u_3} [MeasurableSpace W] [Fintype W] {α : ℝ} {C : U → ℝ} [MeasurableSpace U] [Fintype U] [MeasurableSpace O] [Countable O] [MeasurableSingletonClass O] [MeasurableSingletonClass U] [MeasurableSingletonClass W] {μ : MeasureTheory.Measure W} [MeasureTheory.IsFiniteMeasure μ] {A : O → Set W} {m : U → W → ENNReal} (hα : 0 ≤ α) {o₁ o₂ : O} (h₁ : μ (A o₁) ≠ 0) (h₂ : μ (A o₂) ≠ 0) {g : U → ENNReal} (hg₁ : ∀ (u : U), ∀ w ∈ A o₁, μ {w} ≠ 0 → m u w = g u) (hg₂ : ∀ (u : U), ∀ w ∈ A o₂, μ {w} ≠ 0 → m u w = g u) : (speaker α C ⇑(ProbabilityTheory.Kernel.ofDensity μ m) fun (o : O) => μ[|A o]) o₂ = (speaker α C ⇑(ProbabilityTheory.Kernel.ofDensity μ m) fun (o : O) => μ[|A o]) o₁

A speaker who knows an event on which every graded meaning is constant sees the listener only through those constants, so two such events with the same constants yield the same speaker.

theorem RSA.speaker_cond_listener_truthful_apply_eq {W : Type u_1} {U : Type u_2} {O : Type u_3} [MeasurableSpace W] [Fintype W] {α : ℝ} {C : U → ℝ} [MeasurableSpace U] [Fintype U] [MeasurableSpace O] [Countable O] [MeasurableSingletonClass O] [MeasurableSingletonClass U] [MeasurableSingletonClass W] {μ : MeasureTheory.Measure W} [MeasureTheory.IsFiniteMeasure μ] {A : O → Set W} {sem : U → Set W} (hα : 0 ≤ α) {o₁ o₂ : O} (h₁ : μ (A o₁) ≠ 0) (h₂ : μ (A o₂) ≠ 0) (h : ∀ (u : U), A o₂ ≤ᵐ[μ] sem u ↔ A o₁ ≤ᵐ[μ] sem u) : (speaker α C ⇑(listener μ (truthful sem)) fun (o : O) => μ[|A o]) o₂ = (speaker α C ⇑(listener μ (truthful sem)) fun (o : O) => μ[|A o]) o₁

Against a literal listener the speaker depends on what she knows only through the utterances it entails.