The RSA recursion as alternating maximization #
A speaker observes the state through a kernel and addresses a listener, who hears her utterance
and infers the state. The free energy of a speaker and a listener is the conditional entropy of
the utterance given the observation plus the rationality times the expected utility, the
listener's log-probability of the state less the cost of the utterance. The two agents of the
Rational Speech Act recursion are its two partial maximizers. Against a fixed listener the
speaker of RSA.speaker at the Bayesian belief maximizes it, and against a fixed speaker the
Bayesian listener does, so a round of the recursion never lowers it.
Main definitions #
RSA.expectedUtility,RSA.freeEnergy: the expected utility and the free energy of a speaker and a listener, for a prior over states and an observation kernel.
Main statements #
RSA.freeEnergy_add_sum_klDiv,RSA.freeEnergy_le_freeEnergy_speaker: against a fixed listener the free energy of a speaker falls short of the RSA speaker's by her expected divergence from it.RSA.freeEnergy_le_freeEnergy_listener: against a fixed speaker her Bayesian listener maximizes the free energy.RSA.freeEnergy_speaker_le_freeEnergy_listener,RSA.freeEnergy_listener_le_freeEnergy_speaker: in a round of the recursion the listener's update and the speaker's update each raise the free energy, with no condition on the supports.
Implementation notes #
- The free energy is the functional the source calls the RSA tradeoff. Row by row it is the free energy of the Gibbs variational principle, entropy plus expected log-weight, for the weights the speaker normalizes.
- The speaker's belief is any family
bthat satisfies Bayes' rule with the denominator cleared,(κ ∘ₘ μ) {o} * b o {w} = μ {w} * κ w {o}on reals. The listenerlistener μ κof the observation kernel is one (RSA.comp_real_mul_listener_real), and so is the point mass for a speaker who observes the state itself (RSA.id_comp_real_mul_dirac_real). - The utility is real-valued, with
Real.log 0 = 0, where an extended-real utility would be−∞at a state the listener rules out. The two agree for a speaker who uses no utterance whose listener rules out a state she entertains, and the two maximality statements quantify over such competitors. Along the recursion the condition holds of itself. - The source proves the two maximality statements for a speaker who knows the state. The statements here, for a speaker who observes it through a kernel, run the same argument with her belief in place of the point mass.
References #
The rows of the speaker #
theorem
RSA.isProbabilityMeasure_speaker_of_absolutelyContinuous
{W : Type u_1}
{O : Type u_2}
{U : Type u_3}
[MeasurableSpace W]
[MeasurableSpace O]
[MeasurableSpace U]
[Fintype W]
[Fintype U]
[MeasurableSingletonClass U]
[Countable O]
[MeasurableSingletonClass O]
{α : ℝ}
{C : U → ℝ}
{L : U → MeasureTheory.Measure W}
[∀ (u : U), MeasureTheory.IsFiniteMeasure (L u)]
{b : O → MeasureTheory.Measure W}
{o : O}
{q : MeasureTheory.Measure U}
[MeasureTheory.IsProbabilityMeasure q]
(hα : 0 ≤ α)
(hq : q.AbsolutelyContinuous ((speaker α C L b) o))
:
MeasureTheory.IsProbabilityMeasure ((speaker α C L b) o)
A speaker row that dominates a probability measure is a probability measure.
theorem
RSA.toReal_klDiv_speaker_add_measureEntropy
{W : Type u_1}
{O : Type u_2}
{U : Type u_3}
[MeasurableSpace W]
[MeasurableSpace O]
[MeasurableSpace U]
[Fintype W]
[Fintype U]
[MeasurableSingletonClass U]
[Countable O]
[MeasurableSingletonClass O]
{α : ℝ}
{C : U → ℝ}
{L : U → MeasureTheory.Measure W}
[∀ (u : U), MeasureTheory.IsFiniteMeasure (L u)]
{b : O → MeasureTheory.Measure W}
{o : O}
{q : MeasureTheory.Measure U}
[MeasureTheory.IsProbabilityMeasure q]
[MeasurableSingletonClass W]
[MeasureTheory.IsFiniteMeasure (b o)]
(hα : 0 ≤ α)
(hq : q.AbsolutelyContinuous ((speaker α C L b) o))
:
(InformationTheory.klDiv q ((speaker α C L b) o)).toReal + InformationTheory.measureEntropy q = Real.log (∑ u : U, (((b o).geomMean fun (w : W) => (L u) {w}) ^ α).toReal * Real.exp (-(α * C u))) - α * ∫ (u : U), ∫ (w : W), Real.log ((L u).real {w}) ∂b o - C u ∂q
Gibbs' variational identity for a speaker row. The divergence of a distribution over
utterances from the row and its entropy add up to the log partition function less α times its
expected utility under the speaker's belief.
theorem
RSA.measureEntropy_add_utility_le_speaker
{W : Type u_1}
{O : Type u_2}
{U : Type u_3}
[MeasurableSpace W]
[MeasurableSpace O]
[MeasurableSpace U]
[Fintype W]
[Fintype U]
[MeasurableSingletonClass U]
[Countable O]
[MeasurableSingletonClass O]
{α : ℝ}
{C : U → ℝ}
{L : U → MeasureTheory.Measure W}
[∀ (u : U), MeasureTheory.IsFiniteMeasure (L u)]
{b : O → MeasureTheory.Measure W}
{o : O}
{q : MeasureTheory.Measure U}
[MeasureTheory.IsProbabilityMeasure q]
[MeasurableSingletonClass W]
[MeasureTheory.IsFiniteMeasure (b o)]
(hα : 0 ≤ α)
(hq : q.AbsolutelyContinuous ((speaker α C L b) o))
:
InformationTheory.measureEntropy q + α * ∫ (u : U), ∫ (w : W), Real.log ((L u).real {w}) ∂b o - C u ∂q ≤ InformationTheory.measureEntropy ((speaker α C L b) o) + α * ∫ (u : U), ∫ (w : W), Real.log ((L u).real {w}) ∂b o - C u ∂(speaker α C L b) o
Among the distributions it dominates, a speaker row has the greatest entropy plus α times
expected utility under her belief.
The free energy #
noncomputable def
RSA.expectedUtility
{W : Type u_1}
{O : Type u_2}
{U : Type u_3}
[MeasurableSpace W]
[MeasurableSpace O]
[MeasurableSpace U]
(μ : MeasureTheory.Measure W)
(κ : ProbabilityTheory.Kernel W O)
(C : U → ℝ)
[Fintype W]
(S : ProbabilityTheory.Kernel O U)
(L : ProbabilityTheory.Kernel U W)
:
ℝ
The expected utility of a speaker and a listener averages the listener's log-probability of the state, less the cost of the utterance, over the states, the speaker's observations and her utterances.
Equations
- RSA.expectedUtility μ κ C S L = ∑ w : W, μ.real {w} * ∫ (u : U), Real.log ((L u).real {w}) - C u ∂(S.comp κ) w
Instances For
noncomputable def
RSA.freeEnergy
{W : Type u_1}
{O : Type u_2}
{U : Type u_3}
[MeasurableSpace W]
[MeasurableSpace O]
[MeasurableSpace U]
(μ : MeasureTheory.Measure W)
(κ : ProbabilityTheory.Kernel W O)
(C : U → ℝ)
(α : ℝ)
[Fintype W]
[Fintype O]
(S : ProbabilityTheory.Kernel O U)
(L : ProbabilityTheory.Kernel U W)
:
ℝ
The free energy of a speaker and a listener is the conditional entropy of the utterance given
the speaker's observation plus α times the expected utility.
Equations
- RSA.freeEnergy μ κ C α S L = ∑ o : O, (μ.bind ⇑κ).real {o} * InformationTheory.measureEntropy (S o) + α * RSA.expectedUtility μ κ C S L
Instances For
theorem
RSA.freeEnergy_id
{W : Type u_1}
{U : Type u_3}
[MeasurableSpace W]
[MeasurableSpace U]
(μ : MeasureTheory.Measure W)
(C : U → ℝ)
(α : ℝ)
[Fintype W]
(S : ProbabilityTheory.Kernel W U)
(L : ProbabilityTheory.Kernel U W)
:
freeEnergy μ ProbabilityTheory.Kernel.id C α S L = ∑ w : W, μ.real {w} * InformationTheory.measureEntropy (S w) + α * ∑ w : W, μ.real {w} * ∫ (u : U), Real.log ((L u).real {w}) - C u ∂S w
For a speaker who observes the state itself the free energy averages over the states alone.
theorem
RSA.freeEnergy_le
{W : Type u_1}
{O : Type u_2}
{U : Type u_3}
[MeasurableSpace W]
[MeasurableSpace O]
[MeasurableSpace U]
(μ : MeasureTheory.Measure W)
(κ : ProbabilityTheory.Kernel W O)
(C : U → ℝ)
[Fintype W]
[Fintype O]
[Fintype U]
[MeasurableSingletonClass W]
[MeasurableSingletonClass O]
[MeasurableSingletonClass U]
[MeasureTheory.IsProbabilityMeasure μ]
[ProbabilityTheory.IsMarkovKernel κ]
{α : ℝ}
(hα : 0 ≤ α)
(S : ProbabilityTheory.Kernel O U)
[ProbabilityTheory.IsMarkovKernel S]
(L : ProbabilityTheory.Kernel U W)
[∀ (u : U), MeasureTheory.IsZeroOrProbabilityMeasure (L u)]
:
freeEnergy μ κ C α S L ≤ Real.log ↑(Fintype.card U) + α * ∑ u : U, |C u|
The free energy is bounded above, by the log of the number of utterances when there is no cost.
The speaker's step #
theorem
RSA.expectedUtility_eq_sum_comp
{W : Type u_1}
{O : Type u_2}
{U : Type u_3}
[MeasurableSpace W]
[MeasurableSpace O]
[MeasurableSpace U]
{μ : MeasureTheory.Measure W}
{κ : ProbabilityTheory.Kernel W O}
{C : U → ℝ}
[Fintype W]
[Fintype O]
[Fintype U]
[MeasurableSingletonClass W]
[MeasurableSingletonClass O]
[MeasurableSingletonClass U]
[MeasureTheory.IsFiniteMeasure μ]
[ProbabilityTheory.IsFiniteKernel κ]
{b : O → MeasureTheory.Measure W}
[∀ (o : O), MeasureTheory.IsFiniteMeasure (b o)]
(hb : ∀ (o : O) (w : W), (μ.bind ⇑κ).real {o} * (b o).real {w} = μ.real {w} * (κ w).real {o})
(S : ProbabilityTheory.Kernel O U)
[ProbabilityTheory.IsFiniteKernel S]
(L : ProbabilityTheory.Kernel U W)
:
expectedUtility μ κ C S L = ∑ o : O, (μ.bind ⇑κ).real {o} * ∫ (u : U), ∫ (w : W), Real.log ((L u).real {w}) ∂b o - C u ∂S o
The expected utility as the speaker sees it averages, over her observations and utterances, the listener's log-probability of the state expected under her belief, less the cost.
theorem
RSA.freeEnergy_add_sum_klDiv
{W : Type u_1}
{O : Type u_2}
{U : Type u_3}
[MeasurableSpace W]
[MeasurableSpace O]
[MeasurableSpace U]
{μ : MeasureTheory.Measure W}
{κ : ProbabilityTheory.Kernel W O}
{C : U → ℝ}
{α : ℝ}
[Fintype W]
[Fintype O]
[Fintype U]
[MeasurableSingletonClass W]
[MeasurableSingletonClass O]
[MeasurableSingletonClass U]
[MeasureTheory.IsFiniteMeasure μ]
[ProbabilityTheory.IsFiniteKernel κ]
{b : O → MeasureTheory.Measure W}
[∀ (o : O), MeasureTheory.IsFiniteMeasure (b o)]
(hb : ∀ (o : O) (w : W), (μ.bind ⇑κ).real {o} * (b o).real {w} = μ.real {w} * (κ w).real {o})
(hα : 0 ≤ α)
(L : ProbabilityTheory.Kernel U W)
[ProbabilityTheory.IsFiniteKernel L]
(S : ProbabilityTheory.Kernel O U)
[ProbabilityTheory.IsMarkovKernel S]
(hS : ∀ (o : O), (μ.bind ⇑κ) {o} ≠ 0 → (S o).AbsolutelyContinuous ((speaker α C (⇑L) b) o))
:
freeEnergy μ κ C α S L + ∑ o : O, (μ.bind ⇑κ).real {o} * (InformationTheory.klDiv (S o) ((speaker α C (⇑L) b) o)).toReal = ∑ o : O,
(μ.bind ⇑κ).real {o} * Real.log (∑ u : U, (((b o).geomMean fun (w : W) => (L u) {w}) ^ α).toReal * Real.exp (-(α * C u)))
Against a fixed listener, the free energy of a speaker and her expected divergence from the RSA speaker add up to the expected log partition function.
theorem
RSA.freeEnergy_le_freeEnergy_speaker
{W : Type u_1}
{O : Type u_2}
{U : Type u_3}
[MeasurableSpace W]
[MeasurableSpace O]
[MeasurableSpace U]
{μ : MeasureTheory.Measure W}
{κ : ProbabilityTheory.Kernel W O}
{C : U → ℝ}
{α : ℝ}
[Fintype W]
[Fintype O]
[Fintype U]
[MeasurableSingletonClass W]
[MeasurableSingletonClass O]
[MeasurableSingletonClass U]
[MeasureTheory.IsFiniteMeasure μ]
[ProbabilityTheory.IsFiniteKernel κ]
{b : O → MeasureTheory.Measure W}
[∀ (o : O), MeasureTheory.IsFiniteMeasure (b o)]
(hb : ∀ (o : O) (w : W), (μ.bind ⇑κ).real {o} * (b o).real {w} = μ.real {w} * (κ w).real {o})
(hα : 0 ≤ α)
(L : ProbabilityTheory.Kernel U W)
[ProbabilityTheory.IsFiniteKernel L]
(S : ProbabilityTheory.Kernel O U)
[ProbabilityTheory.IsMarkovKernel S]
(hS : ∀ (o : O), (μ.bind ⇑κ) {o} ≠ 0 → (S o).AbsolutelyContinuous ((speaker α C (⇑L) b) o))
:
freeEnergy μ κ C α S L ≤ freeEnergy μ κ C α (speaker α C (⇑L) b) L
Against a fixed listener the speaker at the Bayesian belief maximizes the free energy.
The listener's step #
theorem
RSA.expectedUtility_listener_eq_posterior
{W : Type u_1}
{O : Type u_2}
{U : Type u_3}
[MeasurableSpace W]
[MeasurableSpace O]
[MeasurableSpace U]
(μ : MeasureTheory.Measure W)
(κ : ProbabilityTheory.Kernel W O)
(C : U → ℝ)
[Fintype W]
[Fintype U]
[MeasurableSingletonClass W]
[MeasurableSingletonClass U]
[Nonempty W]
[MeasureTheory.IsProbabilityMeasure μ]
[ProbabilityTheory.IsMarkovKernel κ]
(S : ProbabilityTheory.Kernel O U)
[ProbabilityTheory.IsMarkovKernel S]
:
expectedUtility μ κ C S (listener μ ⇑(S.comp κ)) = expectedUtility μ κ C S (ProbabilityTheory.posterior (S.comp κ) μ)
The expected utility of a speaker against her listener is her expected utility against the posterior, since the two agree wherever she is heard.
theorem
RSA.expectedUtility_le_listener
{W : Type u_1}
{O : Type u_2}
{U : Type u_3}
[MeasurableSpace W]
[MeasurableSpace O]
[MeasurableSpace U]
(μ : MeasureTheory.Measure W)
(κ : ProbabilityTheory.Kernel W O)
(C : U → ℝ)
[Fintype W]
[Fintype U]
[MeasurableSingletonClass W]
[MeasurableSingletonClass U]
[Nonempty W]
[MeasureTheory.IsProbabilityMeasure μ]
[ProbabilityTheory.IsMarkovKernel κ]
(S : ProbabilityTheory.Kernel O U)
[ProbabilityTheory.IsMarkovKernel S]
(L : ProbabilityTheory.Kernel U W)
[∀ (u : U), MeasureTheory.IsZeroOrProbabilityMeasure (L u)]
(hL : ∀ (u : U), (μ.bind ⇑(S.comp κ)) {u} ≠ 0 → ((listener μ ⇑(S.comp κ)) u).AbsolutelyContinuous (L u))
:
expectedUtility μ κ C S L ≤ expectedUtility μ κ C S (listener μ ⇑(S.comp κ))
Against a fixed speaker her Bayesian listener maximizes the expected utility.
theorem
RSA.freeEnergy_le_freeEnergy_listener
{W : Type u_1}
{O : Type u_2}
{U : Type u_3}
[MeasurableSpace W]
[MeasurableSpace O]
[MeasurableSpace U]
(μ : MeasureTheory.Measure W)
(κ : ProbabilityTheory.Kernel W O)
(C : U → ℝ)
(α : ℝ)
[Fintype W]
[Fintype U]
[MeasurableSingletonClass W]
[MeasurableSingletonClass U]
[Nonempty W]
[MeasureTheory.IsProbabilityMeasure μ]
[ProbabilityTheory.IsMarkovKernel κ]
(S : ProbabilityTheory.Kernel O U)
[ProbabilityTheory.IsMarkovKernel S]
(L : ProbabilityTheory.Kernel U W)
[∀ (u : U), MeasureTheory.IsZeroOrProbabilityMeasure (L u)]
(hL : ∀ (u : U), (μ.bind ⇑(S.comp κ)) {u} ≠ 0 → ((listener μ ⇑(S.comp κ)) u).AbsolutelyContinuous (L u))
[Fintype O]
(hα : 0 ≤ α)
:
freeEnergy μ κ C α S L ≤ freeEnergy μ κ C α S (listener μ ⇑(S.comp κ))
Against a fixed speaker her Bayesian listener maximizes the free energy.
A round of the recursion #
The side conditions of the two steps hold of themselves along the recursion: the speaker who answers a listener uses no utterance whose listener rules out a state she entertains, and the Bayesian listener of a speaker rules out no state at which she might have said the utterance.
theorem
RSA.speaker_listener_apply_singleton_ne_zero
{W : Type u_1}
{O : Type u_2}
{U : Type u_3}
[MeasurableSpace W]
[MeasurableSpace O]
[MeasurableSpace U]
{μ : MeasureTheory.Measure W}
{κ : ProbabilityTheory.Kernel W O}
{C : U → ℝ}
{α : ℝ}
[Fintype W]
[Fintype O]
[Fintype U]
[MeasurableSingletonClass W]
[MeasurableSingletonClass O]
[MeasurableSingletonClass U]
[MeasureTheory.IsProbabilityMeasure μ]
[ProbabilityTheory.IsMarkovKernel κ]
{b : O → MeasureTheory.Measure W}
[∀ (o : O), MeasureTheory.IsFiniteMeasure (b o)]
(hb : ∀ (o : O) (w : W), (μ.bind ⇑κ).real {o} * (b o).real {w} = μ.real {w} * (κ w).real {o})
(hα : 0 ≤ α)
{S : ProbabilityTheory.Kernel O U}
[ProbabilityTheory.IsFiniteKernel S]
{o : O}
{u : U}
(ho : (μ.bind ⇑κ) {o} ≠ 0)
(hS : (S o) {u} ≠ 0)
:
An utterance a speaker might say at an observation that can occur is one the best response to her listener might say there too.
theorem
RSA.isMarkovKernel_speaker_listener
{W : Type u_1}
{O : Type u_2}
{U : Type u_3}
[MeasurableSpace W]
[MeasurableSpace O]
[MeasurableSpace U]
{μ : MeasureTheory.Measure W}
{κ : ProbabilityTheory.Kernel W O}
{C : U → ℝ}
{α : ℝ}
[Fintype W]
[Fintype O]
[Fintype U]
[MeasurableSingletonClass W]
[MeasurableSingletonClass O]
[MeasurableSingletonClass U]
[MeasureTheory.IsProbabilityMeasure μ]
[ProbabilityTheory.IsMarkovKernel κ]
{b : O → MeasureTheory.Measure W}
[∀ (o : O), MeasureTheory.IsFiniteMeasure (b o)]
(hb : ∀ (o : O) (w : W), (μ.bind ⇑κ).real {o} * (b o).real {w} = μ.real {w} * (κ w).real {o})
(hα : 0 ≤ α)
(hκ : ∀ (o : O), (μ.bind ⇑κ) {o} ≠ 0)
(S : ProbabilityTheory.Kernel O U)
[ProbabilityTheory.IsMarkovKernel S]
:
When every observation can occur, the best response to the listener of a speaker is again a probability kernel.
theorem
RSA.freeEnergy_listener_le_freeEnergy_speaker
{W : Type u_1}
{O : Type u_2}
{U : Type u_3}
[MeasurableSpace W]
[MeasurableSpace O]
[MeasurableSpace U]
{μ : MeasureTheory.Measure W}
{κ : ProbabilityTheory.Kernel W O}
{C : U → ℝ}
{α : ℝ}
[Fintype W]
[Fintype O]
[Fintype U]
[MeasurableSingletonClass W]
[MeasurableSingletonClass O]
[MeasurableSingletonClass U]
[MeasureTheory.IsProbabilityMeasure μ]
[ProbabilityTheory.IsMarkovKernel κ]
{b : O → MeasureTheory.Measure W}
[∀ (o : O), MeasureTheory.IsFiniteMeasure (b o)]
(hb : ∀ (o : O) (w : W), (μ.bind ⇑κ).real {o} * (b o).real {w} = μ.real {w} * (κ w).real {o})
(hα : 0 ≤ α)
(S : ProbabilityTheory.Kernel O U)
[ProbabilityTheory.IsMarkovKernel S]
:
freeEnergy μ κ C α S (listener μ ⇑(S.comp κ)) ≤ freeEnergy μ κ C α (speaker α C (⇑(listener μ ⇑(S.comp κ))) b) (listener μ ⇑(S.comp κ))
The speaker's best response to the listener of any speaker raises the free energy.
theorem
RSA.freeEnergy_speaker_le_freeEnergy_listener
{W : Type u_1}
{O : Type u_2}
{U : Type u_3}
[MeasurableSpace W]
[MeasurableSpace O]
[MeasurableSpace U]
{μ : MeasureTheory.Measure W}
{κ : ProbabilityTheory.Kernel W O}
{C : U → ℝ}
{α : ℝ}
[Fintype W]
[Fintype O]
[Fintype U]
[MeasurableSingletonClass W]
[MeasurableSingletonClass O]
[MeasurableSingletonClass U]
[MeasureTheory.IsProbabilityMeasure μ]
[ProbabilityTheory.IsMarkovKernel κ]
{b : O → MeasureTheory.Measure W}
[∀ (o : O), MeasureTheory.IsFiniteMeasure (b o)]
(hb : ∀ (o : O) (w : W), (μ.bind ⇑κ).real {o} * (b o).real {w} = μ.real {w} * (κ w).real {o})
(hα : 0 ≤ α)
[Nonempty W]
(L : ProbabilityTheory.Kernel U W)
[∀ (u : U), MeasureTheory.IsZeroOrProbabilityMeasure (L u)]
[ProbabilityTheory.IsMarkovKernel (speaker α C (⇑L) b)]
:
freeEnergy μ κ C α (speaker α C (⇑L) b) L ≤ freeEnergy μ κ C α (speaker α C (⇑L) b) (listener μ ⇑((speaker α C (⇑L) b).comp κ))
The listener's update to the speaker who answers her raises the free energy.
The speaker who knows the state #
theorem
RSA.id_comp_real_mul_dirac_real
{W : Type u_1}
[MeasurableSpace W]
(μ : MeasureTheory.Measure W)
[MeasurableSingletonClass W]
(o w : W)
:
(μ.bind ⇑ProbabilityTheory.Kernel.id).real {o} * (MeasureTheory.Measure.dirac o).real {w} = μ.real {w} * (ProbabilityTheory.Kernel.id w).real {o}
A speaker who observes the state itself believes the point mass there.