Docs / Pragmatics / RSA / KullbackLeibler

The speaker and the Kullback–Leibler divergence

import Linglib.Pragmatics.RSA.KullbackLeibler · namespace RSA

Source

Goodman and Stuhlmüller's speaker scores an utterance by the expected log-probability its listener gives the state under her belief. That utility and the negative Kullback–Leibler divergence of the listener from her belief differ by the entropy of the belief, which no utterance changes, so she is equally the softmax of the negative divergence, and at no cost prefers the utterance whose listener is closer to her belief.

References

Declarations

The utility of an utterance is minus the divergence of its listener from the belief, less its cost and the entropy of the belief, which no utterance changes.

theorem utility_eq_neg_klDiv_subL35–44
{W : Type u_1} {U : Type u_2} [MeasurableSpace W] [Fintype W] [MeasurableSingletonClass W] {C : U → ℝ} {L : U → MeasureTheory.Measure W} {u : U} {β : MeasureTheory.Measure W} [MeasureTheory.IsProbabilityMeasure β] [MeasureTheory.IsZeroOrProbabilityMeasure (L u)] :
utility C L β u = -↑(InformationTheory.klDiv β (L u)) - ↑(C u) - ↑(InformationTheory.measureEntropy β)
theorem speaker_eq_softmax_klDivL46–51
{W : Type u_1} {U : Type u_2} {O : Type u_3} [MeasurableSpace W] [Fintype W] [MeasurableSingletonClass W] [MeasurableSpace U] [Fintype U] [MeasurableSingletonClass U] [MeasurableSpace O] [Countable O] [MeasurableSingletonClass O] {α : ℝ} {C : U → ℝ} {L : U → MeasureTheory.Measure W} {b : O → MeasureTheory.Measure W} [∀ (o : O), MeasureTheory.IsProbabilityMeasure (b o)] [∀ (u : U), MeasureTheory.IsZeroOrProbabilityMeasure (L u)] :
speaker α C L b = ProbabilityTheory.Kernel.softmax fun (o : O) (u : U) => ↑α * (-↑(InformationTheory.klDiv (b o) (L u)) - ↑(C u))
theorem speaker_zero_real_singleton_lt_iff_klDivL53–69
{W : Type u_1} {U : Type u_2} {O : Type u_3} [MeasurableSpace W] [Fintype W] [MeasurableSingletonClass W] [MeasurableSpace U] [Fintype U] [MeasurableSingletonClass U] [MeasurableSpace O] [Countable O] [MeasurableSingletonClass O] {α : ℝ} {L : U → MeasureTheory.Measure W} {b : O → MeasureTheory.Measure W} {o : O} {u u' : U} [MeasureTheory.IsProbabilityMeasure (b o)] [∀ (u : U), MeasureTheory.IsZeroOrProbabilityMeasure (L u)] (hα : 0 < α) :
((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)