Hawkins, Gweon and Goodman (2021): The division of labor in communication

This file formalizes the resource-rational model of perspective-taking of [HGG21] for the director–matcher task. A Game fixes the target, the shared context, the graded meaning of Eq. 1 (a false description keeps a small mass ε) and the prior over the object hidden behind an occluder. The egocentric speaker utility Game.egoUtility (Eq. 3) rewards informativity for the literal listener over the shared context; the asymmetry-aware utility Game.asymUtility (Eq. 2) averages it over the hidden object; Game.mixUtility (Eq. 5) interpolates with the weight wS, and Game.mixSpeaker is the corresponding score speaker of the kernel pipeline. On the listener's side Game.mixListener (Eq. 6) mixes the literal listener over the speaker's view with the one over the listener's own view, and Game.rrSpeakerUtility is the resource-rational trade-off of Eq. 10 between the accuracy the best utterance earns and the linear cost of perspective-taking.

Game.gain_eq decomposes the extra preference of the asymmetric over the egocentric utility for a more specific description into a sum over hidden objects, from which Appendix A's Theorem 1 follows when the two descriptions are equally informative over the shared context (Game.gain_pos_of_tie), together with the preference of every mixture speaker with wS > 0 (Game.mixSpeaker_prefers). Game.gain_neg_of_shared_hidden records that the theorem's premise cannot be dropped: a hidden object satisfying both descriptions weakens the asymmetric speaker's relative preference.

Implementation notes

• The literal listener Game.L0 is the uniform prior on a finite context reweighted by the meaning of Eq. 1, and the speakers are Kernel.softmax over the single state of the fixed target.
• Appendix A's proof treats a hidden object that satisfies both descriptions as leaving the listener unchanged, which holds only when the two descriptions have the same mass over the shared context; Game.gain_eq makes the residual term explicit and Game.gain_neg_of_shared_hidden exhibits the failure. The paper's simulations, with a target that shape alone identifies in the shared context, satisfy the tie (stimulus_tie).
• The nested weights of Eqs. 7–9 and the listener's resource-rational utility over the pragmatic listener are not formalized; the speaker's Eq. 10 uses the literal listener of Eq. 6 with a discrete uniform prior over the listener weight, whose expectation is the midpoint (Game.rrSpeakerUtility_eq).

TODO

• Eqs. 7–9: agents reasoning about the partner's weight, and the interior optimum of §2.4.
• Appendix B: the listener's posterior over the speaker's weight from observed utterances.

References

• [HGG21]
• [KLB03]

The model (§2)

structure HawkinsGweonGoodman2021.Game (O : Type u_1) (U : Type u_2) : Type (max u_1 u_2)

A director–matcher game: utterances U describe objects O; the speaker refers to target in the shared context, with the listener possibly seeing one more object drawn from hidden.

• applies : U → O → Prop

  Whether an utterance is true of an object.

• target : O

  The target of reference.

• context : Finset O

  The shared context: the objects both agents see.

• hidden : O → ℝ

  The prior over the object hidden behind an occluder.

• cost : U → ℝ

  The production cost of an utterance.

• ε : ℝ

  The mass a false description keeps in Eq. 1.

noncomputable def HawkinsGweonGoodman2021.Game.meaning {O : Type u_1} {U : Type u_2} (g : Game O U) [(u : U) → DecidablePred (g.applies u)] (u : U) (o : O) : ℝ

The graded meaning of Eq. 1: 1 where the utterance is true, ε where it is false.

Equations

• g.meaning u o = if g.applies u o then 1 else g.ε

noncomputable def HawkinsGweonGoodman2021.Game.mass {O : Type u_1} {U : Type u_2} (g : Game O U) [(u : U) → DecidablePred (g.applies u)] (S : Finset O) (u : U) : ℝ

The total meaning mass of an utterance over a context.

Equations

• g.mass S u = ∑ o ∈ S, g.meaning u o

noncomputable def HawkinsGweonGoodman2021.Game.L0 {O : Type u_1} {U : Type u_2} (g : Game O U) [(u : U) → DecidablePred (g.applies u)] (S : Finset O) (u : U) (o : O) : ℝ

The literal listener over a context (Eq. 1): the uniform prior on the context reweighted by the meaning.

Equations

• g.L0 S u o = g.meaning u o / g.mass S u

noncomputable def HawkinsGweonGoodman2021.Game.egoUtility {O : Type u_1} {U : Type u_2} (g : Game O U) [(u : U) → DecidablePred (g.applies u)] (u : U) : ℝ

(3): the egocentric speaker utility, informativity for the literal listener over the shared context less cost.

Equations

• g.egoUtility u = Real.log (g.L0 g.context u g.target) - g.cost u

theorem HawkinsGweonGoodman2021.Game.meaning_pos {O : Type u_1} {U : Type u_2} (g : Game O U) [(u : U) → DecidablePred (g.applies u)] (hε : 0 < g.ε) (u : U) (o : O) : 0 < g.meaning u o

theorem HawkinsGweonGoodman2021.Game.meaning_le_one {O : Type u_1} {U : Type u_2} (g : Game O U) [(u : U) → DecidablePred (g.applies u)] (hε1 : g.ε ≤ 1) (u : U) (o : O) : g.meaning u o ≤ 1

theorem HawkinsGweonGoodman2021.Game.mass_pos {O : Type u_1} {U : Type u_2} (g : Game O U) [(u : U) → DecidablePred (g.applies u)] (hε : 0 < g.ε) {S : Finset O} (hS : S.Nonempty) (u : U) : 0 < g.mass S u

theorem HawkinsGweonGoodman2021.Game.meaning_le_of_specific {O : Type u_1} {U : Type u_2} (g : Game O U) [(u : U) → DecidablePred (g.applies u)] (hε1 : g.ε ≤ 1) {u₀ u₁ : U} (hspec : ∀ (o : O), g.applies u₀ o → g.applies u₁ o) (o : O) : g.meaning u₀ o ≤ g.meaning u₁ o

A more specific utterance has pointwise smaller meaning.

theorem HawkinsGweonGoodman2021.Game.mass_congr {O : Type u_1} {U : Type u_2} (g : Game O U) [(u : U) → DecidablePred (g.applies u)] {S : Finset O} {u₀ u₁ : U} (h : ∀ o ∈ S, g.applies u₀ o ↔ g.applies u₁ o) : g.mass S u₀ = g.mass S u₁

Two utterances true of the same objects of a context have the same mass there.

noncomputable def HawkinsGweonGoodman2021.Game.mixListener {O : Type u_1} {U : Type u_2} (g : Game O U) [(u : U) → DecidablePred (g.applies u)] [DecidableEq O] (h : O) (wL : ℝ) (u : U) (o : O) : ℝ

(6): the listener mixing the literal listener over the speaker's view (the asymmetry-aware listener, which discounts its private object h) with the one over its own view, with weight wL.

Equations

• g.mixListener h wL u o = wL * g.L0 g.context u o + (1 - wL) * g.L0 (insert h g.context) u o

theorem HawkinsGweonGoodman2021.Game.mass_insert_of_notMem {O : Type u_1} {U : Type u_2} (g : Game O U) [(u : U) → DecidablePred (g.applies u)] [DecidableEq O] {S : Finset O} {h : O} (hh : h ∉ S) (u : U) : g.mass (insert h S) u = g.meaning u h + g.mass S u

theorem HawkinsGweonGoodman2021.Game.L0_insert_le {O : Type u_1} {U : Type u_2} (g : Game O U) [(u : U) → DecidablePred (g.applies u)] [DecidableEq O] (hε : 0 < g.ε) (u : U) (o h : O) (hh : h ∉ g.context) (hc : g.context.Nonempty) : g.L0 (insert h g.context) u o ≤ g.L0 g.context u o

The literal listener's share of the target drops when an object enters the context.

theorem HawkinsGweonGoodman2021.Game.mixListener_target_mono {O : Type u_1} {U : Type u_2} (g : Game O U) [(u : U) → DecidablePred (g.applies u)] [DecidableEq O] (hε : 0 < g.ε) (u : U) (h : O) (hh : h ∉ g.context) (hc : g.context.Nonempty) : Monotone fun (wL : ℝ) => g.mixListener h wL u g.target

Listener accuracy is monotone in the listener's perspective-taking weight.

noncomputable def HawkinsGweonGoodman2021.Game.asymUtility {O : Type u_1} {U : Type u_2} (g : Game O U) [(u : U) → DecidablePred (g.applies u)] [Fintype O] (u : U) : ℝ

(2): the asymmetry-aware speaker utility, informativity averaged over the object the listener may see behind the occluder.

Equations

• g.asymUtility u = ∑ h : O, g.hidden h * Real.log (g.meaning u g.target / (g.meaning u h + g.mass g.context u)) - g.cost u

noncomputable def HawkinsGweonGoodman2021.Game.mixUtility {O : Type u_1} {U : Type u_2} (g : Game O U) [(u : U) → DecidablePred (g.applies u)] [Fintype O] (wS : ℝ) (u : U) : ℝ

(5): the mixture utility with perspective-taking weight wS.

Equations

• g.mixUtility wS u = wS * g.asymUtility u + (1 - wS) * g.egoUtility u

theorem HawkinsGweonGoodman2021.Game.mixUtility_zero {O : Type u_1} {U : Type u_2} (g : Game O U) [(u : U) → DecidablePred (g.applies u)] [Fintype O] (u : U) : g.mixUtility 0 u = g.egoUtility u

theorem HawkinsGweonGoodman2021.Game.mixUtility_one {O : Type u_1} {U : Type u_2} (g : Game O U) [(u : U) → DecidablePred (g.applies u)] [Fintype O] (u : U) : g.mixUtility 1 u = g.asymUtility u

Appendix A

theorem HawkinsGweonGoodman2021.Game.gain_eq {O : Type u_1} {U : Type u_2} (g : Game O U) [(u : U) → DecidablePred (g.applies u)] [Fintype O] (hε : 0 < g.ε) (hc : g.context.Nonempty) (hsum : ∑ h : O, g.hidden h = 1) (u₀ u₁ : U) : g.asymUtility u₀ - g.asymUtility u₁ - (g.egoUtility u₀ - g.egoUtility u₁) = ∑ h : O, g.hidden h * (Real.log (1 + g.meaning u₁ h / g.mass g.context u₁) - Real.log (1 + g.meaning u₀ h / g.mass g.context u₀))

The extra preference of the asymmetric over the egocentric utility for u₀ against u₁, decomposed over the hidden object: each hidden object contributes the log-ratio of how much it dilutes the two descriptions.

theorem HawkinsGweonGoodman2021.Game.gain_pos_of_tie {O : Type u_1} {U : Type u_2} (g : Game O U) [(u : U) → DecidablePred (g.applies u)] [Fintype O] (hε : 0 < g.ε) (hε1 : g.ε < 1) (hc : g.context.Nonempty) (hp : ∀ (h : O), 0 ≤ g.hidden h) (hsum : ∑ h : O, g.hidden h = 1) {u₀ u₁ : U} (hspec : ∀ (o : O), g.applies u₀ o → g.applies u₁ o) (htie : g.mass g.context u₀ = g.mass g.context u₁) (hstar : ∃ (h : O), g.applies u₁ h ∧ ¬g.applies u₀ h ∧ 0 < g.hidden h) : g.egoUtility u₀ - g.egoUtility u₁ < g.asymUtility u₀ - g.asymUtility u₁

Appendix A, Theorem 1, under the tie that makes its proof go through: if u₀ is more specific than u₁, the two are equally informative over the shared context, and some hidden object of positive prior satisfies u₁ but not u₀, then the asymmetric utility favours u₀ over u₁ strictly more than the egocentric utility does.

theorem HawkinsGweonGoodman2021.Game.gain_neg_of_shared_hidden {O : Type u_1} {U : Type u_2} (g : Game O U) [(u : U) → DecidablePred (g.applies u)] [Fintype O] (hε : 0 < g.ε) (hc : g.context.Nonempty) (hp : ∀ (h : O), 0 ≤ g.hidden h) (hsum : ∑ h : O, g.hidden h = 1) {u₀ u₁ : U} (hshared : ∀ (h : O), 0 < g.hidden h → g.applies u₀ h ∧ g.applies u₁ h) (hlt : g.mass g.context u₀ < g.mass g.context u₁) : g.asymUtility u₀ - g.asymUtility u₁ < g.egoUtility u₀ - g.egoUtility u₁

The premise of Appendix A cannot be dropped: when every hidden object of positive prior satisfies both descriptions and u₀ is strictly more specific over the shared context, the asymmetric utility favours u₀ over u₁ strictly less than the egocentric utility does, since the shared hidden object dilutes the narrower description more.

The resource-rational speaker (§2.4)

noncomputable def HawkinsGweonGoodman2021.Game.accuracy {O : Type u_1} {U : Type u_2} (g : Game O U) [(u : U) → DecidablePred (g.applies u)] [Fintype O] [DecidableEq O] (u : U) (wL : ℝ) : ℝ

The expected accuracy of an utterance for a listener of weight wL, averaged over the hidden object.

Equations

• g.accuracy u wL = ∑ h : O, g.hidden h * g.mixListener h wL u g.target

theorem HawkinsGweonGoodman2021.Game.accuracy_eq {O : Type u_1} {U : Type u_2} (g : Game O U) [(u : U) → DecidablePred (g.applies u)] [Fintype O] [DecidableEq O] (u : U) (wL : ℝ) : g.accuracy u wL = wL * ∑ h : O, g.hidden h * g.L0 g.context u g.target + (1 - wL) * ∑ h : O, g.hidden h * g.L0 (insert h g.context) u g.target

Accuracy is affine in the listener weight.

noncomputable def HawkinsGweonGoodman2021.Game.best {O : Type u_1} {U : Type u_2} (g : Game O U) [(u : U) → DecidablePred (g.applies u)] [Fintype O] [Fintype U] [Nonempty U] (wS : ℝ) : U

The utterance the mixture speaker of weight wS prefers, u* of Eq. 10.

Equations

• g.best wS = Classical.choose ⋯

theorem HawkinsGweonGoodman2021.Game.best_isMax {O : Type u_1} {U : Type u_2} (g : Game O U) [(u : U) → DecidablePred (g.applies u)] [Fintype O] [Fintype U] [Nonempty U] (wS : ℝ) (u : U) : g.mixUtility wS u ≤ g.mixUtility wS (g.best wS)

noncomputable def HawkinsGweonGoodman2021.Game.rrSpeakerUtility {O : Type u_1} {U : Type u_2} (g : Game O U) [(u : U) → DecidablePred (g.applies u)] [Fintype O] [DecidableEq O] [Fintype U] [Nonempty U] (β wS : ℝ) : ℝ

(10): the speaker's resource-rational utility, the accuracy of its preferred utterance under a listener weight drawn uniformly from the five-point grid, less the linear cost β · wS of perspective-taking.

Equations

• g.rrSpeakerUtility β wS = 1 / 5 * ∑ k ∈ Finset.range 5, g.accuracy (g.best wS) (↑k / 4) - β * wS

theorem HawkinsGweonGoodman2021.Game.rrSpeakerUtility_eq {O : Type u_1} {U : Type u_2} (g : Game O U) [(u : U) → DecidablePred (g.applies u)] [Fintype O] [DecidableEq O] [Fintype U] [Nonempty U] (β wS : ℝ) : g.rrSpeakerUtility β wS = g.accuracy (g.best wS) (1 / 2) - β * wS

Accuracy is affine in the listener weight, so its average over the grid is its value at the midpoint.

Speakers of the kernel pipeline

noncomputable def HawkinsGweonGoodman2021.Game.mixSpeaker {O : Type u_1} {U : Type u_2} (g : Game O U) [(u : U) → DecidablePred (g.applies u)] [Fintype O] [Fintype U] [MeasurableSpace U] (α wS : ℝ) : ProbabilityTheory.Kernel Unit U

(1), (5): the mixture speaker with rationality α and perspective-taking weight wS, a score speaker over the single state of the fixed target.

Equations

• g.mixSpeaker α wS = ProbabilityTheory.Kernel.softmax fun (x : Unit) (u : U) => ↑(α * g.mixUtility wS u)

theorem HawkinsGweonGoodman2021.Game.mixSpeaker_lt_iff {O : Type u_1} {U : Type u_2} (g : Game O U) [(u : U) → DecidablePred (g.applies u)] [Fintype O] [Fintype U] [MeasurableSpace U] [MeasurableSingletonClass U] {α : ℝ} (hα : 0 < α) (wS : ℝ) {u u' : U} : ((g.mixSpeaker α wS) ()).real {u} < ((g.mixSpeaker α wS) ()).real {u'} ↔ g.mixUtility wS u < g.mixUtility wS u'

theorem HawkinsGweonGoodman2021.Game.mixSpeaker_prefers {O : Type u_1} {U : Type u_2} (g : Game O U) [(u : U) → DecidablePred (g.applies u)] [Fintype O] [Fintype U] [MeasurableSpace U] [MeasurableSingletonClass U] (hε : 0 < g.ε) (hε1 : g.ε < 1) (hc : g.context.Nonempty) (hp : ∀ (h : O), 0 ≤ g.hidden h) (hsum : ∑ h : O, g.hidden h = 1) {u₀ u₁ : U} (hspec : ∀ (o : O), g.applies u₀ o → g.applies u₁ o) (htie : g.mass g.context u₀ = g.mass g.context u₁) (hstar : ∃ (h : O), g.applies u₁ h ∧ ¬g.applies u₀ h ∧ 0 < g.hidden h) (hego : g.egoUtility u₁ ≤ g.egoUtility u₀) {α wS : ℝ} (hα : 0 < α) (hw : 0 < wS) : ((g.mixSpeaker α wS) ()).real {u₁} < ((g.mixSpeaker α wS) ()).real {u₀}

Appendix A's corollary: whenever the egocentric speaker does not disprefer the more specific description, every mixture speaker with wS > 0 prefers it, under the tie of gain_pos_of_tie.

The stimulus of §2.4

inductive HawkinsGweonGoodman2021.Feature : Type

The three features of the objects.

• shape : Feature
• color : Feature
• texture : Feature

@[instance_reducible]

instance HawkinsGweonGoodman2021.instDecidableEqFeature : DecidableEq Feature

Equations

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

@[instance_reducible]

instance HawkinsGweonGoodman2021.instFintypeFeature : Fintype Feature

Equations

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

@[instance_reducible]

instance HawkinsGweonGoodman2021.instReprFeature : Repr Feature

Equations

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

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

Equations

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

@[reducible, inline]

abbrev HawkinsGweonGoodman2021.Obj : Type

An object as its profile of matches with the target on each feature.

Equations

• HawkinsGweonGoodman2021.Obj = (HawkinsGweonGoodman2021.Feature → Bool)

@[reducible, inline]

abbrev HawkinsGweonGoodman2021.Utt : Type

An utterance mentions a set of features.

Equations

• HawkinsGweonGoodman2021.Utt = Finset HawkinsGweonGoodman2021.Feature

@[instance_reducible]

instance HawkinsGweonGoodman2021.instMeasurableSpaceUtt : MeasurableSpace Utt

Equations

• HawkinsGweonGoodman2021.instMeasurableSpaceUtt = ⊤

instance HawkinsGweonGoodman2021.instMeasurableSingletonClassUtt : MeasurableSingletonClass Utt

def HawkinsGweonGoodman2021.target : Obj

The target matches itself on every feature.

Equations

• HawkinsGweonGoodman2021.target x✝ = true

def HawkinsGweonGoodman2021.d1 : Obj

The distractor sharing the target's color and texture.

Equations

• HawkinsGweonGoodman2021.d1 f = decide (f ≠ HawkinsGweonGoodman2021.Feature.shape)

def HawkinsGweonGoodman2021.d2 : Obj

The distractor matching the target on nothing.

Equations

• HawkinsGweonGoodman2021.d2 x✝ = false

noncomputable def HawkinsGweonGoodman2021.hiddenPrior (o : Obj) : ℝ

The prior over the hidden object's profile when each of the four values of a feature is equally likely: a match on each feature with probability 1/4, independently.

Equations

• HawkinsGweonGoodman2021.hiddenPrior o = ∏ f : HawkinsGweonGoodman2021.Feature, if o f = true then 1 / 4 else 3 / 4

noncomputable def HawkinsGweonGoodman2021.stimulus (c : ℝ) : Game Obj Utt

The game of §2.4: the target with the two distractors of Fig. 1 in view, a hidden object drawn from hiddenPrior, cost c per mentioned feature, and ε = 1/100.

Equations

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

@[instance_reducible]

instance HawkinsGweonGoodman2021.instDecidablePredObjAppliesUttStimulus (c : ℝ) (u : Utt) : DecidablePred ((stimulus c).applies u)

Equations

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

theorem HawkinsGweonGoodman2021.stimulus_hidden (c : ℝ) : (stimulus c).hidden = hiddenPrior

theorem HawkinsGweonGoodman2021.hiddenPrior_pos (o : Obj) : 0 < hiddenPrior o

theorem HawkinsGweonGoodman2021.hiddenPrior_nonneg (o : Obj) : 0 ≤ hiddenPrior o

theorem HawkinsGweonGoodman2021.sum_hiddenPrior : ∑ o : Obj, hiddenPrior o = 1

theorem HawkinsGweonGoodman2021.stimulus_tie (c : ℝ) : (stimulus c).mass (stimulus c).context {Feature.shape, Feature.color, Feature.texture} = (stimulus c).mass (stimulus c).context {Feature.shape}

In the shared context shape alone identifies the target, so the full description and the bare shape have the same mass there.

theorem HawkinsGweonGoodman2021.stimulus_prefers_full {c α wS : ℝ} (hα : 0 < α) (hw : 0 < wS) (hego : (stimulus c).egoUtility {Feature.shape} ≤ (stimulus c).egoUtility {Feature.shape, Feature.color, Feature.texture}) : (((stimulus c).mixSpeaker α wS) ()).real {{Feature.shape}} < (((stimulus c).mixSpeaker α wS) ()).real {{Feature.shape, Feature.color, Feature.texture}}

§2.4.1, first prediction: on the stimulus, a mixture speaker with any wS > 0 prefers the full description to the bare shape whenever the cost does not already make the egocentric speaker prefer the shape, since a hidden object matching the shape alone has positive prior.