The decision-theoretic listener

This file defines the listener of Rational Speech Act models who acts. After an utterance the listener's belief is a kernel from utterances to states, and a decision problem is a reward for each action at each state. The listener's expected reward of an action is the reward averaged over the belief, and the listener chooses an action by the softmax of expected reward at a rationality. The decision-theoretic utility of an utterance for the speaker is the true reward of the action the listener's policy chooses. In a signaling game an action is a guess of the state, rewarded when right, so the expected reward of a guess is the belief's mass on it.

Main definitions

• RSA.expectedReward: the listener's expected reward of an action after an utterance.
• RSA.policy: the listener's policy, the softmax of expected reward at a rationality.
• RSA.actionUtility: the expected true reward of the listener's choice, the speaker's decision-theoretic utility of an utterance at a state.

Main results

• RSA.policy_real_lt_iff, RSA.policy_single_real_lt_iff: the listener prefers the action with the higher expected reward, and in a signaling game the state the belief finds more probable.
• RSA.policy_real_singleton: the policy's share of an action is the real softmax.
• RSA.policy_real_of_pair, RSA.actionUtility_of_pair: with two actions the share is the logistic function of the scaled difference in expected reward, and the utility is the rewards weighted by the shares.

References

• [SHGH24]
• [HGI25]
• [vR03b]
• [QF15]

noncomputable def RSA.actionUtility {W : Type u_1} {U : Type u_2} {A : Type u_3} [MeasurableSpace U] [Fintype A] [MeasurableSpace A] (π : ProbabilityTheory.Kernel U A) (R : A → W → ℝ) (u : U) (w : W) : ℝ

The decision-theoretic utility of an utterance at a state is the true reward of the action the listener's policy chooses, in expectation.

Equations

• RSA.actionUtility π R u w = ∑ a : A, (π u).real {a} * R a w

theorem RSA.actionUtility_of_pair {W : Type u_1} {U : Type u_2} {A : Type u_3} [MeasurableSpace U] [Fintype A] [MeasurableSpace A] [DiscreteMeasurableSpace A] (R : A → W → ℝ) (π : ProbabilityTheory.Kernel U A) {u : U} {a a' : A} {w : W} [ProbabilityTheory.IsMarkovKernel π] (haa' : a ≠ a') (hall : ∀ (c : A), c = a ∨ c = a') : actionUtility π R u w = (π u).real {a} * R a w + (1 - (π u).real {a}) * R a' w

With two actions, utility is the reward of the first weighted by its share and of the second by the rest.

noncomputable def RSA.expectedReward {W : Type u_1} {U : Type u_2} {A : Type u_3} [Fintype W] [MeasurableSpace W] [MeasurableSpace U] (L : ProbabilityTheory.Kernel U W) (R : A → W → ℝ) (u : U) (a : A) : ℝ

The listener's expected reward of an action after an utterance is the reward averaged over the belief.

Equations

• RSA.expectedReward L R u a = ∑ w : W, (L u).real {w} * R a w

theorem RSA.expectedReward_single {W : Type u_1} {U : Type u_2} [Fintype W] [MeasurableSpace W] [MeasurableSpace U] [DecidableEq W] (L : ProbabilityTheory.Kernel U W) (u : U) (w : W) : expectedReward L (fun (a : W) => Pi.single a 1) u w = (L u).real {w}

In a signaling game an action is a guess of the state, rewarded when right, so the expected reward of a guess is the belief's mass on it.

noncomputable def RSA.policyScore {W : Type u_1} {U : Type u_2} {A : Type u_3} [Fintype W] [MeasurableSpace W] [MeasurableSpace U] (β : ℝ) (L : ProbabilityTheory.Kernel U W) (R : A → W → ℝ) (u : U) (a : A) : EReal

The score of an action for the listener is rationality times expected reward.

Equations

• RSA.policyScore β L R u a = ↑(β * RSA.expectedReward L R u a)

noncomputable def RSA.policy {W : Type u_1} {U : Type u_2} {A : Type u_3} [Fintype W] [MeasurableSpace W] [MeasurableSpace U] [Fintype U] [DiscreteMeasurableSpace U] [Fintype A] [MeasurableSpace A] (β : ℝ) (L : ProbabilityTheory.Kernel U W) (R : A → W → ℝ) : ProbabilityTheory.Kernel U A

The listener's policy is the softmax of expected reward at rationality β.

Equations

• RSA.policy β L R = ProbabilityTheory.Kernel.softmax (RSA.policyScore β L R)

instance RSA.instIsFiniteKernelPolicy {W : Type u_1} {U : Type u_2} {A : Type u_3} [Fintype W] [MeasurableSpace W] [MeasurableSpace U] [Fintype U] [DiscreteMeasurableSpace U] [Fintype A] [MeasurableSpace A] (β : ℝ) (L : ProbabilityTheory.Kernel U W) (R : A → W → ℝ) : ProbabilityTheory.IsFiniteKernel (policy β L R)

instance RSA.instIsMarkovKernelPolicyOfNonempty {W : Type u_1} {U : Type u_2} {A : Type u_3} [Fintype W] [MeasurableSpace W] [MeasurableSpace U] [Fintype U] [DiscreteMeasurableSpace U] [Fintype A] [MeasurableSpace A] (β : ℝ) (L : ProbabilityTheory.Kernel U W) (R : A → W → ℝ) [Nonempty A] : ProbabilityTheory.IsMarkovKernel (policy β L R)

theorem RSA.policy_real_lt_iff {W : Type u_1} {U : Type u_2} {A : Type u_3} [Fintype W] [MeasurableSpace W] [MeasurableSpace U] [Fintype U] [DiscreteMeasurableSpace U] [Fintype A] [MeasurableSpace A] [DiscreteMeasurableSpace A] {β : ℝ} (L : ProbabilityTheory.Kernel U W) (R : A → W → ℝ) {u : U} {a a' : A} (hβ : 0 < β) : ((policy β L R) u).real {a} < ((policy β L R) u).real {a'} ↔ expectedReward L R u a < expectedReward L R u a'

Row preference of the policy is comparison of expected reward.

theorem RSA.policy_single_real_lt_iff {W : Type u_1} {U : Type u_2} [Fintype W] [MeasurableSpace W] [MeasurableSpace U] [Fintype U] [DiscreteMeasurableSpace U] {β : ℝ} (L : ProbabilityTheory.Kernel U W) {u : U} {w : W} [DecidableEq W] [DiscreteMeasurableSpace W] (hβ : 0 < β) {w' : W} : ((policy β L fun (a : W) => Pi.single a 1) u).real {w} < ((policy β L fun (a : W) => Pi.single a 1) u).real {w'} ↔ (L u).real {w} < (L u).real {w'}

A listener rewarded for guessing the state prefers the states the belief finds more probable.

theorem RSA.policy_real_singleton {W : Type u_1} {U : Type u_2} {A : Type u_3} [Fintype W] [MeasurableSpace W] [MeasurableSpace U] [Fintype U] [DiscreteMeasurableSpace U] [Fintype A] [MeasurableSpace A] [DiscreteMeasurableSpace A] {β : ℝ} (L : ProbabilityTheory.Kernel U W) (R : A → W → ℝ) {u : U} {a : A} : ((policy β L R) u).real {a} = Real.softmax (fun (a : A) => β * expectedReward L R u a) a

The policy's share of an action is the real softmax of the scaled expected rewards.

theorem RSA.policy_real_of_pair {W : Type u_1} {U : Type u_2} {A : Type u_3} [Fintype W] [MeasurableSpace W] [MeasurableSpace U] [Fintype U] [DiscreteMeasurableSpace U] [Fintype A] [MeasurableSpace A] [DiscreteMeasurableSpace A] {β : ℝ} (L : ProbabilityTheory.Kernel U W) (R : A → W → ℝ) {u : U} {a a' : A} (haa' : a ≠ a') (hall : ∀ (c : A), c = a ∨ c = a') : ((policy β L R) u).real {a} = (β * (expectedReward L R u a - expectedReward L R u a')).sigmoid

With two actions, the policy's share of one is the logistic function of the scaled difference in expected reward.

theorem RSA.actionUtility_policy_eq_of_expectedReward_eq_add {W : Type u_1} {U : Type u_2} {A : Type u_3} [Fintype W] [MeasurableSpace W] [MeasurableSpace U] [Fintype U] [DiscreteMeasurableSpace U] [Fintype A] [MeasurableSpace A] [DiscreteMeasurableSpace A] {β : ℝ} (L : ProbabilityTheory.Kernel U W) (R : A → W → ℝ) {u : U} {w : W} {L' : ProbabilityTheory.Kernel U W} {u' : U} {c : ℝ} (h : ∀ (a : A), expectedReward L R u a = expectedReward L' R u' a + c) : actionUtility (policy β L R) R u w = actionUtility (policy β L' R) R u' w

Two utterances after which the listener's expected rewards agree up to a constant shift leave the policy, and so the utility at every state, the same; the listeners may differ.