Zaslavsky, Hu and Levy (2021): A Rate–Distortion View of Human Pragmatic Reasoning?

Zaslavsky, Hu and Levy show that the Rational Speech Act recursion is an alternating maximization. A reference game has finitely many meanings and utterances, a prior over the meanings, a lexicon and a cost on the utterances. A speaker is a kernel from meanings to utterances and a listener a kernel back. The tradeoff of a speaker and a listener is the speaker's conditional entropy plus α times the expected utility, the listener's log-probability of the speaker's meaning less the cost of her utterance. Against a fixed listener the RSA speaker maximizes the tradeoff, and against a fixed speaker the Bayesian listener does, so the tradeoff never decreases along the recursion.

Main statements

• freeEnergy_le_freeEnergy_speaker, freeEnergy_le_freeEnergy_listener: against a fixed listener the RSA speaker maximizes the tradeoff, and against a fixed speaker the Bayesian listener does.
• freeEnergy_le_freeEnergy_listener_succ, freeEnergy_le_freeEnergy_speaker_succ, exists_tendsto_freeEnergy: along the recursion each listener update and each speaker update raises the tradeoff, which therefore converges.
• listener_apply_singleton_eq_zero, speaker_listener_apply_singleton_eq_zero: no agent of the recursion pairs an utterance with a meaning the lexicon rules out for it.

Implementation notes

• The paper's speaker knows the meaning, so its tradeoff is RSA.freeEnergy at the identity observation kernel, which RSA.freeEnergy_id writes as the paper does, and its speaker believes the point mass. The two maximality statements are cases of the ones in the alternating-maximization file, whose notes say how the real-valued utility there relates to the paper's.
• listener t is the paper's listener of depth t, and the speaker who answers it is the paper's speaker of depth t + 1. The recursion assumes a prior that charges every meaning and a finite lexicon in which every meaning has an applicable utterance, so that every speaker is a probability kernel. A listener's row is zero at an utterance that applies to no meaning. The lexicon is any such weight and the cost any real function, where the paper's lexicon has values in the unit interval and its cost is nonnegative.
• The lexicon statements need 0 < α, where the paper has 0 ≤ α. At α = 0 the speaker here is uniform over all the utterances, since 0 ^ 0 = 1.

TODO

• The fixed points of the recursion are stationary points of the tradeoff, and the limit of the tradeoff along the recursion is its value at one.
• The rate–distortion variant, whose tradeoff has mutual information in place of the conditional entropy, with its update equations.
• The asymptotic behaviour of the recursion and the criticality of α = 1.

References

• [ZHL21]
• [FG12]

The two steps

theorem ZaslavskyHuLevy2021.freeEnergy_le_freeEnergy_speaker {M : Type u_1} {U : Type u_2} [MeasurableSpace M] [MeasurableSpace U] [Fintype M] [Fintype U] [MeasurableSingletonClass M] [MeasurableSingletonClass U] (P : MeasureTheory.Measure M) (C : U → ℝ) [MeasureTheory.IsFiniteMeasure P] {α : ℝ} (hα : 0 ≤ α) (L : ProbabilityTheory.Kernel U M) [ProbabilityTheory.IsFiniteKernel L] (S : ProbabilityTheory.Kernel M U) [ProbabilityTheory.IsMarkovKernel S] (hS : ∀ (m : M), P {m} ≠ 0 → (S m).AbsolutelyContinuous ((RSA.speaker α C (⇑L) MeasureTheory.Measure.dirac) m)) : RSA.freeEnergy P ProbabilityTheory.Kernel.id C α S L ≤ RSA.freeEnergy P ProbabilityTheory.Kernel.id C α (RSA.speaker α C (⇑L) MeasureTheory.Measure.dirac) L

Against a fixed listener the RSA speaker maximizes the tradeoff (7).

theorem ZaslavskyHuLevy2021.expectedUtility_le_listener {M : Type u_1} {U : Type u_2} [MeasurableSpace M] [MeasurableSpace U] [Fintype M] [Fintype U] [MeasurableSingletonClass M] [MeasurableSingletonClass U] (P : MeasureTheory.Measure M) (C : U → ℝ) [Nonempty M] [MeasureTheory.IsProbabilityMeasure P] (S : ProbabilityTheory.Kernel M U) [ProbabilityTheory.IsMarkovKernel S] (L : ProbabilityTheory.Kernel U M) [∀ (u : U), MeasureTheory.IsZeroOrProbabilityMeasure (L u)] (hL : ∀ (u : U), (P.bind ⇑S) {u} ≠ 0 → ((RSA.listener P ⇑S) u).AbsolutelyContinuous (L u)) : RSA.expectedUtility P ProbabilityTheory.Kernel.id C S L ≤ RSA.expectedUtility P ProbabilityTheory.Kernel.id C S (RSA.listener P ⇑S)

Against a fixed speaker her Bayesian listener maximizes the expected utility (12).

theorem ZaslavskyHuLevy2021.freeEnergy_le_freeEnergy_listener {M : Type u_1} {U : Type u_2} [MeasurableSpace M] [MeasurableSpace U] [Fintype M] [Fintype U] [MeasurableSingletonClass M] [MeasurableSingletonClass U] (P : MeasureTheory.Measure M) (C : U → ℝ) (α : ℝ) [Nonempty M] [MeasureTheory.IsProbabilityMeasure P] (S : ProbabilityTheory.Kernel M U) [ProbabilityTheory.IsMarkovKernel S] (L : ProbabilityTheory.Kernel U M) [∀ (u : U), MeasureTheory.IsZeroOrProbabilityMeasure (L u)] (hL : ∀ (u : U), (P.bind ⇑S) {u} ≠ 0 → ((RSA.listener P ⇑S) u).AbsolutelyContinuous (L u)) (hα : 0 ≤ α) : RSA.freeEnergy P ProbabilityTheory.Kernel.id C α S L ≤ RSA.freeEnergy P ProbabilityTheory.Kernel.id C α S (RSA.listener P ⇑S)

Against a fixed speaker her Bayesian listener maximizes the tradeoff (8).

The recursion

noncomputable def ZaslavskyHuLevy2021.listener {M : Type u_1} {U : Type u_2} [MeasurableSpace M] [MeasurableSpace U] [Fintype M] [Fintype U] [MeasurableSingletonClass M] [MeasurableSingletonClass U] (P : MeasureTheory.Measure M) (C : U → ℝ) (α : ℝ) (l : U → M → ENNReal) : ℕ → ProbabilityTheory.Kernel U M

The listeners of the recursion (3) start from the literal listener L₀(m | u) ∝ l(m, u) P(m), and each later one is the listener of the speaker (2) who answers the one before.

Equations

• ZaslavskyHuLevy2021.listener P C α l 0 = ProbabilityTheory.Kernel.ofDensity P l
• ZaslavskyHuLevy2021.listener P C α l t.succ = RSA.listener P ⇑(RSA.speaker α C (⇑(ZaslavskyHuLevy2021.listener P C α l t)) MeasureTheory.Measure.dirac)

instance ZaslavskyHuLevy2021.instIsFiniteKernelListener {M : Type u_1} {U : Type u_2} [MeasurableSpace M] [MeasurableSpace U] [Fintype M] [Fintype U] [MeasurableSingletonClass M] [MeasurableSingletonClass U] (P : MeasureTheory.Measure M) (C : U → ℝ) (α : ℝ) (l : U → M → ENNReal) (t : ℕ) : ProbabilityTheory.IsFiniteKernel (listener P C α l t)

instance ZaslavskyHuLevy2021.instIsZeroOrProbabilityMeasureCoeKernelMeasureListener {M : Type u_1} {U : Type u_2} [MeasurableSpace M] [MeasurableSpace U] [Fintype M] [Fintype U] [MeasurableSingletonClass M] [MeasurableSingletonClass U] (P : MeasureTheory.Measure M) (C : U → ℝ) (α : ℝ) (l : U → M → ENNReal) (t : ℕ) (u : U) : MeasureTheory.IsZeroOrProbabilityMeasure ((listener P C α l t) u)

theorem ZaslavskyHuLevy2021.listener_apply_singleton_eq_zero {M : Type u_1} {U : Type u_2} [MeasurableSpace M] [MeasurableSpace U] [Fintype M] [Fintype U] [MeasurableSingletonClass M] [MeasurableSingletonClass U] {P : MeasureTheory.Measure M} {C : U → ℝ} {α : ℝ} {l : U → M → ENNReal} {u : U} {m : M} (hα : 0 < α) (h : l u m = 0) (t : ℕ) : ((listener P C α l t) u) {m} = 0

The listeners of the recursion respect the lexicon. An utterance never leads the listener to a meaning it does not apply to.

theorem ZaslavskyHuLevy2021.speaker_listener_apply_singleton_eq_zero {M : Type u_1} {U : Type u_2} [MeasurableSpace M] [MeasurableSpace U] [Fintype M] [Fintype U] [MeasurableSingletonClass M] [MeasurableSingletonClass U] {P : MeasureTheory.Measure M} {C : U → ℝ} {α : ℝ} {l : U → M → ENNReal} {u : U} {m : M} (hα : 0 < α) (h : l u m = 0) (t : ℕ) : ((RSA.speaker α C (⇑(listener P C α l t)) MeasureTheory.Measure.dirac) m) {u} = 0

The speakers of the recursion respect the lexicon. No meaning is expressed by an utterance that does not apply to it.

theorem ZaslavskyHuLevy2021.listener_apply_singleton_ne_zero {M : Type u_1} {U : Type u_2} [MeasurableSpace M] [MeasurableSpace U] [Fintype M] [Fintype U] [MeasurableSingletonClass M] [MeasurableSingletonClass U] {P : MeasureTheory.Measure M} {C : U → ℝ} {α : ℝ} {l : U → M → ENNReal} {u : U} {m : M} [MeasureTheory.IsFiniteMeasure P] (hP : ∀ (m : M), P {m} ≠ 0) (hl : ∀ (u : U) (m : M), l u m ≠ ⊤) (hα : 0 ≤ α) (h : l u m ≠ 0) (t : ℕ) : ((listener P C α l t) u) {m} ≠ 0

No listener of the recursion rules out a meaning the utterance applies to.

theorem ZaslavskyHuLevy2021.isMarkovKernel_speaker_listener {M : Type u_1} {U : Type u_2} [MeasurableSpace M] [MeasurableSpace U] [Fintype M] [Fintype U] [MeasurableSingletonClass M] [MeasurableSingletonClass U] {P : MeasureTheory.Measure M} {C : U → ℝ} {α : ℝ} {l : U → M → ENNReal} [MeasureTheory.IsFiniteMeasure P] (hP : ∀ (m : M), P {m} ≠ 0) (hl : ∀ (u : U) (m : M), l u m ≠ ⊤) (hα : 0 ≤ α) (hm : ∀ (m : M), ∃ (u : U), l u m ≠ 0) (t : ℕ) : ProbabilityTheory.IsMarkovKernel (RSA.speaker α C (⇑(listener P C α l t)) MeasureTheory.Measure.dirac)

Every speaker of the recursion is a probability kernel when every meaning has an utterance that applies to it.

theorem ZaslavskyHuLevy2021.freeEnergy_le_freeEnergy_speaker_succ {M : Type u_1} {U : Type u_2} [MeasurableSpace M] [MeasurableSpace U] [Fintype M] [Fintype U] [MeasurableSingletonClass M] [MeasurableSingletonClass U] {P : MeasureTheory.Measure M} {C : U → ℝ} {α : ℝ} {l : U → M → ENNReal} [MeasureTheory.IsProbabilityMeasure P] (hP : ∀ (m : M), P {m} ≠ 0) (hl : ∀ (u : U) (m : M), l u m ≠ ⊤) (hα : 0 ≤ α) (hm : ∀ (m : M), ∃ (u : U), l u m ≠ 0) (t : ℕ) : RSA.freeEnergy P ProbabilityTheory.Kernel.id C α (RSA.speaker α C (⇑(listener P C α l t)) MeasureTheory.Measure.dirac) (listener P C α l (t + 1)) ≤ RSA.freeEnergy P ProbabilityTheory.Kernel.id C α (RSA.speaker α C (⇑(listener P C α l (t + 1))) MeasureTheory.Measure.dirac) (listener P C α l (t + 1))

Each speaker update raises the tradeoff, the second inequality of (9).

theorem ZaslavskyHuLevy2021.freeEnergy_le_freeEnergy_listener_succ {M : Type u_1} {U : Type u_2} [MeasurableSpace M] [MeasurableSpace U] [Fintype M] [Fintype U] [MeasurableSingletonClass M] [MeasurableSingletonClass U] {P : MeasureTheory.Measure M} {C : U → ℝ} {α : ℝ} {l : U → M → ENNReal} [MeasureTheory.IsProbabilityMeasure P] (hP : ∀ (m : M), P {m} ≠ 0) (hl : ∀ (u : U) (m : M), l u m ≠ ⊤) (hα : 0 ≤ α) (hm : ∀ (m : M), ∃ (u : U), l u m ≠ 0) [Nonempty M] (t : ℕ) : RSA.freeEnergy P ProbabilityTheory.Kernel.id C α (RSA.speaker α C (⇑(listener P C α l t)) MeasureTheory.Measure.dirac) (listener P C α l t) ≤ RSA.freeEnergy P ProbabilityTheory.Kernel.id C α (RSA.speaker α C (⇑(listener P C α l t)) MeasureTheory.Measure.dirac) (listener P C α l (t + 1))

Each listener update raises the tradeoff, the first inequality of (9).

theorem ZaslavskyHuLevy2021.exists_tendsto_freeEnergy {M : Type u_1} {U : Type u_2} [MeasurableSpace M] [MeasurableSpace U] [Fintype M] [Fintype U] [MeasurableSingletonClass M] [MeasurableSingletonClass U] {P : MeasureTheory.Measure M} {C : U → ℝ} {α : ℝ} {l : U → M → ENNReal} [MeasureTheory.IsProbabilityMeasure P] (hP : ∀ (m : M), P {m} ≠ 0) (hl : ∀ (u : U) (m : M), l u m ≠ ⊤) (hα : 0 ≤ α) (hm : ∀ (m : M), ∃ (u : U), l u m ≠ 0) [Nonempty M] : ∃ (g : ℝ), Filter.Tendsto (fun (t : ℕ) => RSA.freeEnergy P ProbabilityTheory.Kernel.id C α (RSA.speaker α C (⇑(listener P C α l t)) MeasureTheory.Measure.dirac) (listener P C α l t)) Filter.atTop (nhds g)

The tradeoff converges along the recursion, being monotone and bounded above.