Sumers, Ho, Griffiths, and Hawkins (2024): Reconciling Truthfulness and Relevance as Epistemic and Decision-Theoretic Utility

On the speaker model of Sumers, Ho, Griffiths and Hawkins, Grice's maxims of quality and relation are two independent objectives a speaker trades off. Truthfulness is an epistemic utility, 1 for a true utterance and -1 for a false one (5), truthfulness; relevance is a decision-theoretic utility after van Rooy and Benz, the reward the listener earns by acting on the utterance in a decision problem (6)–(8), RSA.actionUtility of RSA.policy; and the speaker of a Rational Speech Act model, after Frank and Goodman, soft-maximizes their convex combination at a weight λ plus a cost term (9), combinedUtility, speaker. The endpoints are the purely truthful speaker, who is insensitive to the decision problem and uniform over the true utterances, speaker_zero_eq_of_mem, and the purely relevant speaker, who exaggerates whenever exaggeration earns the listener more, speaker_one_real_lt_iff.

Signaling bandits decouple the two objectives. A world assigns a value to each feature, an action carries a set of features, and its reward is the sum of their values (10)–(11), reward; an utterance names a feature and its value, true at a world regardless of the decision context, sem; the listener conditions a uniform prior on the utterance and acts on the expected rewards of the actions in the context. Under the uniform prior the posterior mean of the named feature is the named value and every other feature keeps its prior mean, expectedReward_listener_filter, which is how the paper reads Figure 6C: in the context of a red spotted, a red solid, and a blue striped mushroom, naming the value of green or the zero value of red is true but leaves the listener's policy where the prior had it, green_two_true_irrelevant, red_zero_true_irrelevant; naming a positive value of spots is relevant, and the more so the higher the value, so the exaggeration is false but more relevant than the truth, spots_relevant_iff, exaggeration_relevant; and the combined speaker prefers the true utterance exactly when the relevance gained by exaggerating is worth less than the truthfulness lost, prefers_truth_iff. Relevance is context-dependent where truth is not: in a context of three spotted mushrooms naming the value of spots is irrelevant and naming the value of green is relevant (footnote 12), spots_irrelevant_allSpotted, green_relevant_allSpotted.

Appendix A relates decision problems to Roberts's questions under discussion. For the two-action decision problem in which one action earns r in a cell of the partition containing the true world and s outside it, and the other the reverse, relevance is a logistic function of the listener's posterior mass on the cell, actionUtility_cellReward, so for s < r it ranks utterances exactly as the question's epistemic utility, the log of that mass, does, actionUtility_lt_iff_qudUtility_lt; the identity decision problem of Theorem 1 is the case of the singleton cell, actionUtility_lt_iff_log_lt.

The paper's two experiments put participants in the speaker's role in the mushroom domain. In the free-choice experiment participants instructed to be truthful, given no instruction, or instructed to make the tourist pick well were fit by increasing weights on relevance, the uninstructed participants strictly between the endpoints; in the endorsement experiment the separation widened and the uninstructed participants still balanced the two; and the combined model was favored over either objective alone. The worked examples, on which a pragmatic listener embedding the combined speaker infers that a mentioned garage is open, loosens a stated start time, and rounds the time when asked casually, after Van der Henst and colleagues, are simulations at chosen parameters and are not formalized.

Implementation notes

The listener's decision context is the action type, so a context of the bandit is a type of actions with their feature sets, and an utterance's relevance in two contexts is its utility against two action types. The cost term enters with the sign of (9). Lewis signaling games, where the world state is the correct action and the objectives coincide, are described and not formalized.

TODO

• Theorem 1's exact identity: the reward s at which relevance under the identity decision problem equals the log of the posterior mass, defined through the Lambert W function.

References

• [SHGH24]
• [FG12]
• [Gri75]
• [vR03b]
• [Ben06]
• [Rob12]
• [vdHCS02]
• [QF15]

The speaker objectives

def SumersEtAl2024.truthfulness {W : Type u_1} {U : Type u_2} [DecidableEq W] (sem : U → Finset W) (u : U) (w : W) : ℝ

Truthfulness as epistemic utility (5) is 1 for a true utterance and -1 for a false one.

Equations

• SumersEtAl2024.truthfulness sem u w = if w ∈ sem u then 1 else -1

noncomputable def SumersEtAl2024.combinedUtility {W : Type u_1} {U : Type u_2} {A : Type u_3} [DecidableEq W] [MeasurableSpace U] [Fintype A] [MeasurableSpace A] (lam : ℝ) (cost : U → ℝ) (sem : U → Finset W) (π : ProbabilityTheory.Kernel U A) (R : A → W → ℝ) (u : U) (w : W) : ℝ

The combined utility (9) mixes relevance and truthfulness at weight lam on relevance and adds the cost term.

Equations

• SumersEtAl2024.combinedUtility lam cost sem π R u w = lam * RSA.actionUtility π R u w + (1 - lam) * SumersEtAl2024.truthfulness sem u w + cost u

theorem SumersEtAl2024.combinedUtility_zero {W : Type u_1} {U : Type u_2} {A : Type u_3} [DecidableEq W] [MeasurableSpace U] [Fintype A] [MeasurableSpace A] (cost : U → ℝ) (sem : U → Finset W) (π : ProbabilityTheory.Kernel U A) (R : A → W → ℝ) {u : U} {w : W} : combinedUtility 0 cost sem π R u w = truthfulness sem u w + cost u

theorem SumersEtAl2024.combinedUtility_one {W : Type u_1} {U : Type u_2} {A : Type u_3} [DecidableEq W] [MeasurableSpace U] [Fintype A] [MeasurableSpace A] (cost : U → ℝ) (sem : U → Finset W) (π : ProbabilityTheory.Kernel U A) (R : A → W → ℝ) {u : U} {w : W} : combinedUtility 1 cost sem π R u w = RSA.actionUtility π R u w + cost u

noncomputable def SumersEtAl2024.speaker {W : Type u_1} {U : Type u_2} {A : Type u_3} [Fintype W] [DecidableEq W] [MeasurableSpace W] [DiscreteMeasurableSpace W] [Fintype U] [MeasurableSpace U] [Fintype A] [MeasurableSpace A] (βS lam : ℝ) (cost : U → ℝ) (sem : U → Finset W) (π : ProbabilityTheory.Kernel U A) (R : A → W → ℝ) : ProbabilityTheory.Kernel W U

The speaker (1) is the softmax of combined utility at rationality βS.

Equations

• SumersEtAl2024.speaker βS lam cost sem π R = ProbabilityTheory.Kernel.softmax fun (w : W) (u : U) => ↑(βS * SumersEtAl2024.combinedUtility lam cost sem π R u w)

instance SumersEtAl2024.instIsFiniteKernelSpeaker {W : Type u_1} {U : Type u_2} {A : Type u_3} [Fintype W] [DecidableEq W] [MeasurableSpace W] [DiscreteMeasurableSpace W] [Fintype U] [MeasurableSpace U] [Fintype A] [MeasurableSpace A] (lam : ℝ) (cost : U → ℝ) (sem : U → Finset W) (π : ProbabilityTheory.Kernel U A) (R : A → W → ℝ) {βS : ℝ} : ProbabilityTheory.IsFiniteKernel (speaker βS lam cost sem π R)

instance SumersEtAl2024.instIsMarkovKernelSpeakerOfNonempty {W : Type u_1} {U : Type u_2} {A : Type u_3} [Fintype W] [DecidableEq W] [MeasurableSpace W] [DiscreteMeasurableSpace W] [Fintype U] [MeasurableSpace U] [Fintype A] [MeasurableSpace A] (lam : ℝ) (cost : U → ℝ) (sem : U → Finset W) (π : ProbabilityTheory.Kernel U A) (R : A → W → ℝ) {βS : ℝ} [Nonempty U] : ProbabilityTheory.IsMarkovKernel (speaker βS lam cost sem π R)

theorem SumersEtAl2024.speaker_real_lt_iff {W : Type u_1} {U : Type u_2} {A : Type u_3} [Fintype W] [DecidableEq W] [MeasurableSpace W] [DiscreteMeasurableSpace W] [Fintype U] [MeasurableSpace U] [DiscreteMeasurableSpace U] [Fintype A] [MeasurableSpace A] (lam : ℝ) (cost : U → ℝ) (sem : U → Finset W) (π : ProbabilityTheory.Kernel U A) (R : A → W → ℝ) {βS : ℝ} {u u' : U} {w : W} (hβ : 0 < βS) : ((speaker βS lam cost sem π R) w).real {u} < ((speaker βS lam cost sem π R) w).real {u'} ↔ combinedUtility lam cost sem π R u w < combinedUtility lam cost sem π R u' w

Row preference of the speaker is comparison of combined utility.

theorem SumersEtAl2024.speaker_zero_eq_of_mem {W : Type u_1} {U : Type u_2} {A : Type u_3} [Fintype W] [DecidableEq W] [MeasurableSpace W] [DiscreteMeasurableSpace W] [Fintype U] [MeasurableSpace U] [DiscreteMeasurableSpace U] [Fintype A] [MeasurableSpace A] (sem : U → Finset W) (π : ProbabilityTheory.Kernel U A) (R : A → W → ℝ) {βS : ℝ} {u u' : U} {w : W} (c : ℝ) (hu : w ∈ sem u) (hu' : w ∈ sem u') : ((speaker βS 0 (fun (x : U) => c) sem π R) w) {u} = ((speaker βS 0 (fun (x : U) => c) sem π R) w) {u'}

The purely truthful speaker is insensitive to the decision problem, since at equal costs it puts the same mass on any two true utterances.

theorem SumersEtAl2024.speaker_one_real_lt_iff {W : Type u_1} {U : Type u_2} {A : Type u_3} [Fintype W] [DecidableEq W] [MeasurableSpace W] [DiscreteMeasurableSpace W] [Fintype U] [MeasurableSpace U] [DiscreteMeasurableSpace U] [Fintype A] [MeasurableSpace A] (sem : U → Finset W) (π : ProbabilityTheory.Kernel U A) (R : A → W → ℝ) {βS : ℝ} {u u' : U} {w : W} (hβ : 0 < βS) (c : ℝ) : ((speaker βS 1 (fun (x : U) => c) sem π R) w).real {u} < ((speaker βS 1 (fun (x : U) => c) sem π R) w).real {u'} ↔ RSA.actionUtility π R u w < RSA.actionUtility π R u' w

The purely relevant speaker prefers the utterance that earns the listener more, true or not.

Appendix A: decision problems and questions under discussion

def SumersEtAl2024.cellReward {W : Type u_1} [DecidableEq W] (r s : ℝ) (c : Finset W) : Fin 2 → W → ℝ

In the decision problem of a cell the first action earns r in the cell and s outside it, and the second the reverse.

Equations

• SumersEtAl2024.cellReward r s c a w = if w ∈ c ↔ a = 0 then r else s

noncomputable def SumersEtAl2024.cellMass {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] (L : ProbabilityTheory.Kernel U W) (c : Finset W) (u : U) : ℝ

The listener's posterior mass on the cell (A3).

Equations

• SumersEtAl2024.cellMass L c u = ∑ w ∈ c, (L u).real {w}

noncomputable def SumersEtAl2024.qudUtility {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] (L : ProbabilityTheory.Kernel U W) (c : Finset W) (u : U) : ℝ

The epistemic utility of an utterance relative to a question (A2) is the log of the posterior mass on the cell of the true world.

Equations

• SumersEtAl2024.qudUtility L c u = Real.log (SumersEtAl2024.cellMass L c u)

theorem SumersEtAl2024.expectedReward_cellReward {W : Type u_1} {U : Type u_2} [Fintype W] [DecidableEq W] [MeasurableSpace W] [DiscreteMeasurableSpace W] [MeasurableSpace U] (L : ProbabilityTheory.Kernel U W) [ProbabilityTheory.IsMarkovKernel L] {r s : ℝ} (c : Finset W) (u : U) : RSA.expectedReward L (cellReward r s c) u 0 = s + (r - s) * cellMass L c u ∧ RSA.expectedReward L (cellReward r s c) u 1 = r + (s - r) * cellMass L c u

theorem SumersEtAl2024.actionUtility_cellReward {W : Type u_1} {U : Type u_2} [Fintype W] [DecidableEq W] [MeasurableSpace W] [DiscreteMeasurableSpace W] [MeasurableSpace U] (L : ProbabilityTheory.Kernel U W) [ProbabilityTheory.IsMarkovKernel L] {r s : ℝ} (c : Finset W) {u : U} {w : W} {β : ℝ} [Fintype U] [DiscreteMeasurableSpace U] (hw : w ∈ c) : RSA.actionUtility (RSA.policy β L (cellReward r s c)) (cellReward r s c) u w = s + (r - s) * (β * (r - s) * (2 * cellMass L c u - 1)).sigmoid

Relevance under the cell decision problem is a logistic function of the posterior mass on the cell, the calculation of Appendix A.

theorem SumersEtAl2024.actionUtility_lt_iff_qudUtility_lt {W : Type u_1} {U : Type u_2} [Fintype W] [DecidableEq W] [MeasurableSpace W] [DiscreteMeasurableSpace W] [MeasurableSpace U] (L : ProbabilityTheory.Kernel U W) [ProbabilityTheory.IsMarkovKernel L] {r s : ℝ} (c : Finset W) {u u' : U} {w : W} {β : ℝ} [Fintype U] [DiscreteMeasurableSpace U] (hw : w ∈ c) (hrs : s < r) (hβ : 0 < β) (hu : 0 < cellMass L c u) (hu' : 0 < cellMass L c u') : RSA.actionUtility (RSA.policy β L (cellReward r s c)) (cellReward r s c) u w < RSA.actionUtility (RSA.policy β L (cellReward r s c)) (cellReward r s c) u' w ↔ qudUtility L c u < qudUtility L c u'

The cell decision problem ranks utterances as the question's epistemic utility does, whenever the cell of the true world is favored, s < r (Theorem 2).

theorem SumersEtAl2024.actionUtility_lt_iff_log_lt {W : Type u_1} {U : Type u_2} [Fintype W] [DecidableEq W] [MeasurableSpace W] [DiscreteMeasurableSpace W] [MeasurableSpace U] (L : ProbabilityTheory.Kernel U W) [ProbabilityTheory.IsMarkovKernel L] {r s : ℝ} {u u' : U} {w : W} {β : ℝ} [Fintype U] [DiscreteMeasurableSpace U] (hrs : s < r) (hβ : 0 < β) (hu : 0 < (L u).real {w}) (hu' : 0 < (L u').real {w}) : RSA.actionUtility (RSA.policy β L (cellReward r s {w})) (cellReward r s {w}) u w < RSA.actionUtility (RSA.policy β L (cellReward r s {w})) (cellReward r s {w}) u' w ↔ Real.log ((L u).real {w}) < Real.log ((L u').real {w})

The identity decision problem, the cell of the true world alone, ranks utterances as the log of the listener's posterior probability of the true world does (Theorem 1).

Signaling bandits

def SumersEtAl2024.reward {K : Type u_1} {V : Type u_2} {A : Type u_3} (val : V → ℝ) (feat : A → Finset K) (a : A) (w : K → V) : ℝ

The reward of an action carrying the features feat a at a world is the sum of their values (10)–(11).

Equations

• SumersEtAl2024.reward val feat a w = ∑ k ∈ feat a, val (w k)

theorem SumersEtAl2024.sum_ite_div_sum_ite {K : Type u_1} {V : Type u_2} [Fintype K] [DecidableEq K] [Fintype V] (p : V → Prop) [DecidablePred p] (hp : ∃ (x : V), p x) (f k : K) (g : V → ℝ) : ((∑ w : K → V, if p (w f) then g (w k) else 0) / ∑ w : K → V, if p (w f) then 1 else 0) = if k = f then (∑ x : V with p x, g x) / ↑(Finset.filter p Finset.univ).card else (∑ x : V, g x) / ↑(Fintype.card V)

Among the worlds satisfying a condition on one feature's value, the mean of a function of a feature's value is the conditional mean for the conditioned feature and the prior mean for every other feature.

def SumersEtAl2024.sem {K : Type u_1} {V : Type u_2} [Fintype K] [DecidableEq K] [Fintype V] [DecidableEq V] (u : K × V) : Finset (K → V)

The utterance naming a feature and a value is true at the worlds where the feature has that value.

Equations

• SumersEtAl2024.sem u = {w : K → V | w u.1 = u.2}

theorem SumersEtAl2024.mem_sem_iff {K : Type u_1} {V : Type u_2} [Fintype K] [DecidableEq K] [Fintype V] [DecidableEq V] (u : K × V) (w : K → V) : w ∈ sem u ↔ w u.1 = u.2

Truth does not depend on the decision context, since the meaning mentions no actions.

theorem SumersEtAl2024.expectedReward_listener_filter {K : Type u_1} {V : Type u_2} {A : Type u_3} {U : Type u_4} [Fintype K] [DecidableEq K] [Fintype V] [DecidableEq V] [MeasurableSpace (K → V)] [DiscreteMeasurableSpace (K → V)] [Fintype U] [MeasurableSpace U] [DiscreteMeasurableSpace U] {S : U → Finset (K → V)} {u : U} (p : V → Prop) [DecidablePred p] (hp : ∃ (x : V), p x) (f : K) (hS : S u = {w : K → V | p (w f)}) (val : V → ℝ) (feat : A → Finset K) (a : A) : RSA.expectedReward (RSA.listener (ProbabilityTheory.uniformOn Set.univ) (RSA.truthful fun (u : U) => ↑(S u))) (reward val feat) u a = ∑ k ∈ feat a, if k = f then (∑ x : V with p x, val x) / ↑(Finset.filter p Finset.univ).card else (∑ x : V, val x) / ↑(Fintype.card V)

After an utterance whose meaning is a condition on one feature's value, the listener at the uniform prior expects from an action the conditional mean of the named feature and the prior mean of every other feature it carries.

The mushroom domain of Figure 6

inductive SumersEtAl2024.Feature : Type

The features are three colors and three textures.

• green : Feature
• red : Feature
• blue : Feature
• spots : Feature
• solid : Feature
• stripes : Feature

@[instance_reducible]

instance SumersEtAl2024.instDecidableEqFeature : DecidableEq Feature

Equations

• SumersEtAl2024.instDecidableEqFeature x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance SumersEtAl2024.instFintypeFeature : Fintype Feature

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance SumersEtAl2024.instReprFeature : Repr Feature

Equations

• SumersEtAl2024.instReprFeature = { reprPrec := SumersEtAl2024.instReprFeature.repr }

def SumersEtAl2024.instReprFeature.repr : Feature → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance SumersEtAl2024.instMeasurableSpaceFeature : MeasurableSpace Feature

Equations

• SumersEtAl2024.instMeasurableSpaceFeature = ⊤

@[reducible, inline]

abbrev SumersEtAl2024.Value : Type

Feature values -2 to +2, as 0 to 4.

Equations

• SumersEtAl2024.Value = Fin 5

def SumersEtAl2024.val (v : Value) : ℝ

The reward value of a feature value.

Equations

• SumersEtAl2024.val v = ↑↑v - 2

theorem SumersEtAl2024.sum_val : ∑ x : Value, val x = 0

def SumersEtAl2024.world : Feature → Value

The world of Figure 6A has green +2, red 0, blue -2, spots +1, solid 0 and stripes -1.

Equations

• SumersEtAl2024.world SumersEtAl2024.Feature.green = 4
• SumersEtAl2024.world SumersEtAl2024.Feature.red = 2
• SumersEtAl2024.world SumersEtAl2024.Feature.blue = 0
• SumersEtAl2024.world SumersEtAl2024.Feature.spots = 3
• SumersEtAl2024.world SumersEtAl2024.Feature.solid = 2
• SumersEtAl2024.world SumersEtAl2024.Feature.stripes = 1

def SumersEtAl2024.feat : Fin 3 → Finset Feature

The context of Figure 6B has a red spotted, a red solid, and a blue striped mushroom.

Equations

• SumersEtAl2024.feat 0 = {SumersEtAl2024.Feature.red, SumersEtAl2024.Feature.spots}
• SumersEtAl2024.feat 1 = {SumersEtAl2024.Feature.red, SumersEtAl2024.Feature.solid}
• SumersEtAl2024.feat 2 = {SumersEtAl2024.Feature.blue, SumersEtAl2024.Feature.stripes}

def SumersEtAl2024.featSpotted : Fin 3 → Finset Feature

The context of footnote 12 has a green, a red, and a blue spotted mushroom.

Equations

• SumersEtAl2024.featSpotted 0 = {SumersEtAl2024.Feature.green, SumersEtAl2024.Feature.spots}
• SumersEtAl2024.featSpotted 1 = {SumersEtAl2024.Feature.red, SumersEtAl2024.Feature.spots}
• SumersEtAl2024.featSpotted 2 = {SumersEtAl2024.Feature.blue, SumersEtAl2024.Feature.spots}

@[reducible, inline]

noncomputable abbrev SumersEtAl2024.listener : ProbabilityTheory.Kernel (Feature × Value) (Feature → Value)

The literal listener (3) at the uniform prior over worlds.

Equations

• SumersEtAl2024.listener = RSA.listener (ProbabilityTheory.uniformOn Set.univ) (RSA.truthful fun (u : SumersEtAl2024.Feature × SumersEtAl2024.Value) => ↑(SumersEtAl2024.sem u))

@[reducible, inline]

noncomputable abbrev SumersEtAl2024.prior : ProbabilityTheory.Kernel (Feature × Value) (Feature → Value)

The prior as a listener who has heard nothing.

Equations

• SumersEtAl2024.prior = RSA.listener (ProbabilityTheory.uniformOn Set.univ) (RSA.truthful fun (x : SumersEtAl2024.Feature × SumersEtAl2024.Value) => ↑Finset.univ)

theorem SumersEtAl2024.expectedReward_listener (fs : Fin 3 → Finset Feature) (u : Feature × Value) (a : Fin 3) : RSA.expectedReward listener (reward val fs) u a = ∑ k ∈ fs a, if k = u.1 then val u.2 else 0

theorem SumersEtAl2024.expectedReward_prior (fs : Fin 3 → Finset Feature) (u : Feature × Value) (a : Fin 3) : RSA.expectedReward prior (reward val fs) u a = 0

theorem SumersEtAl2024.actionUtility_eq_prior_of_expectedReward (fs : Fin 3 → Finset Feature) (u : Feature × Value) {β c : ℝ} (h : ∀ (a : Fin 3), RSA.expectedReward listener (reward val fs) u a = c) : RSA.actionUtility (RSA.policy β listener (reward val fs)) (reward val fs) u world = RSA.actionUtility (RSA.policy β prior (reward val fs)) (reward val fs) u world

Two utterances after which every action's expected reward agrees up to a shift are equally useful in the context.

theorem SumersEtAl2024.reward_world : reward val feat 0 world = 1 ∧ reward val feat 1 world = 0 ∧ reward val feat 2 world = -3

The three mushrooms of Figure 6B earn 1, 0 and -3 at the world.

theorem SumersEtAl2024.actionUtility_prior (u : Feature × Value) {β : ℝ} : RSA.actionUtility (RSA.policy β prior (reward val feat)) (reward val feat) u world = -2 / 3

The prior policy is uniform over the context, and the utility of acting on the prior alone is the mean reward.

theorem SumersEtAl2024.green_two_true_irrelevant {β : ℝ} : world ∈ sem (Feature.green, 4) ∧ RSA.actionUtility (RSA.policy β listener (reward val feat)) (reward val feat) (Feature.green, 4) world = RSA.actionUtility (RSA.policy β prior (reward val feat)) (reward val feat) (Feature.green, 4) world

Naming the value of green, absent from the context, is true and irrelevant.

theorem SumersEtAl2024.red_zero_true_irrelevant {β : ℝ} : world ∈ sem (Feature.red, 2) ∧ RSA.actionUtility (RSA.policy β listener (reward val feat)) (reward val feat) (Feature.red, 2) world = RSA.actionUtility (RSA.policy β prior (reward val feat)) (reward val feat) (Feature.red, 2) world

Naming the zero value of red, present in the context, is true and irrelevant, since a zero value is the prior mean.

theorem SumersEtAl2024.expectedReward_spots (a : Fin 3) (v : Value) : RSA.expectedReward listener (reward val feat) (Feature.spots, v) a = if a = 0 then val v else 0

Naming a value of spots makes the listener expect that value from the spotted mushroom and nothing from the others.

theorem SumersEtAl2024.actionUtility_spots {β : ℝ} (v : Value) : RSA.actionUtility (RSA.policy β listener (reward val feat)) (reward val feat) (Feature.spots, v) world = (Real.exp (β * val v) - 3) / (Real.exp (β * val v) + 2)

When a value of spots is named, the listener's softmax share of the spotted mushroom earns 1 and the rest is spent on the blue striped one.

theorem SumersEtAl2024.spots_relevant_iff {β : ℝ} (hβ : 0 < β) (v : Value) : RSA.actionUtility (RSA.policy β prior (reward val feat)) (reward val feat) (Feature.spots, v) world < RSA.actionUtility (RSA.policy β listener (reward val feat)) (reward val feat) (Feature.spots, v) world ↔ 0 < val v

Naming a value of spots is relevant exactly when the value is positive, when it raises the listener's expected earnings above acting on the prior.

theorem SumersEtAl2024.exaggeration_relevant {β : ℝ} (hβ : 0 < β) : world ∈ sem (Feature.spots, 3) ∧ world ∉ sem (Feature.spots, 4) ∧ RSA.actionUtility (RSA.policy β listener (reward val feat)) (reward val feat) (Feature.spots, 3) world < RSA.actionUtility (RSA.policy β listener (reward val feat)) (reward val feat) (Feature.spots, 4) world

The exaggeration ⟨spots, +2⟩ is false where ⟨spots, +1⟩ is true, and is the more relevant of the two.

theorem SumersEtAl2024.prefers_truth_iff {β βS : ℝ} (hβS : 0 < βS) (lam c : ℝ) : ((speaker βS lam (fun (x : Feature × Value) => c) sem (RSA.policy β listener (reward val feat)) (reward val feat)) world).real {(Feature.spots, 4)} < ((speaker βS lam (fun (x : Feature × Value) => c) sem (RSA.policy β listener (reward val feat)) (reward val feat)) world).real {(Feature.spots, 3)} ↔ lam * (RSA.actionUtility (RSA.policy β listener (reward val feat)) (reward val feat) (Feature.spots, 4) world - RSA.actionUtility (RSA.policy β listener (reward val feat)) (reward val feat) (Feature.spots, 3) world) < 2 * (1 - lam)

The combined speaker prefers the truth to the exaggeration exactly when the relevance gained by exaggerating, weighted by lam, is worth less than the truthfulness lost.

theorem SumersEtAl2024.spots_irrelevant_allSpotted {β : ℝ} (v : Value) : RSA.actionUtility (RSA.policy β listener (reward val featSpotted)) (reward val featSpotted) (Feature.spots, v) world = RSA.actionUtility (RSA.policy β prior (reward val featSpotted)) (reward val featSpotted) (Feature.spots, v) world

In the context of three spotted mushrooms naming any value of spots is irrelevant, since it shifts every action's expected reward alike.

theorem SumersEtAl2024.green_relevant_allSpotted {β : ℝ} (hβ : 0 < β) : RSA.actionUtility (RSA.policy β prior (reward val featSpotted)) (reward val featSpotted) (Feature.green, 4) world < RSA.actionUtility (RSA.policy β listener (reward val featSpotted)) (reward val featSpotted) (Feature.green, 4) world

In the same context naming the value of green is relevant, since green is now the deciding feature.