[HGG21]: the division of labor in communication

A resource-rational extension of RSA for perspective-taking in the [KLB03] director–matcher reference game. Perspective-taking is costly, so each agent allocates effort via a mixture weight w ∈ [0,1], and the optimal effort depends on the partner's expected effort.

Two PMF reference games formalize the task, built on the canonical operators (RSA.L0OfBoolMeaning, RSA.S1Belief, PMF.posterior):

• egocentric (egoL0/egoS1/egoL1) — three visible objects, shape alone identifies the target.
• asymmetric (asymL0/asymS1/asymL1) — a hidden object behind an occlusion, whose feature-match profile is the latent variable (latentPrior), marginalized via RSA.marginalizeKernel; the speaker hedges with more specific utterances.

The mixture model and resource-rational optimization sit outside the RSA loop, in ℝ, grounded in the PMF literal listener.

Main declarations

• egoL1, asymL1 — the two pragmatic-listener posteriors.
• MontaguGrounding.grounding_ego_meaning — the literal semantics is intersective predicate modification (Modifier.intersective).
• asym_S1_prefers_specificity_when_shape_matches — under asymmetry, the speaker prefers a more specific utterance when the hidden object shares a feature.
• mixUtility, rrUtilityFull — log-space mixture utility and resource-rational utility over the perspective-taking weight.
• no_cost_prefers_full_pt, high_cost_penalizes_full_pt — full perspective-taking is worth its cost only when the cost is low.

Empirical anchors

Experiment 1 (83 dyads, 2×2 occlusion × distractor): speakers used more words under occlusion (+1.3 words) and under a same-shape distractor (+0.6 words). Experiment 2 (116 dyads, a [KLB03] replication): scripted directors elicited ~51% critical errors vs. ~20% for naive directors, listeners adapted from 43% to 30% errors over four critical trials, and informativity predicted accuracy (ρ = −0.81). The eight critical items are the [KLB03] materials (the paper's Table 1). Effect sizes and model fits: [HGG21].

The RSA model

The egocentric game (egoL0/egoS1/egoL1) is over three visible objects with a belief-based α = 2 speaker. The asymmetric game adds a hidden object whose feature-match profile is the latent variable, each feature matching the target independently with probability 1/4. Utterance semantics are intersective predicate modification (see MontaguGrounding).

Finite types

inductive HawkinsGweonGoodman2021.VisObj : Type

The 3 visible objects in the example display.

target: shape=0, color=0, texture=0 d1: shape=1, color=0, texture=0 (shares color+texture with target) d2: shape=2, color=1, texture=1 (differs on all features)

• target : VisObj
• d1 : VisObj
• d2 : VisObj

@[implicit_reducible]

instance HawkinsGweonGoodman2021.instDecidableEqVisObj : DecidableEq VisObj

Equations

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

def HawkinsGweonGoodman2021.instReprVisObj.repr : VisObj → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance HawkinsGweonGoodman2021.instReprVisObj : Repr VisObj

Equations

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

@[implicit_reducible]

instance HawkinsGweonGoodman2021.instInhabitedVisObj : Inhabited VisObj

Equations

• HawkinsGweonGoodman2021.instInhabitedVisObj = { default := HawkinsGweonGoodman2021.instInhabitedVisObj.default }

@[implicit_reducible]

instance HawkinsGweonGoodman2021.instFintypeVisObj : Fintype VisObj

Equations

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

inductive HawkinsGweonGoodman2021.AsymObj : Type

The 4 objects in the asymmetric display (3 visible + 1 behind occlusion)

• target : AsymObj
• d1 : AsymObj
• d2 : AsymObj
• hidden : AsymObj

@[implicit_reducible]

instance HawkinsGweonGoodman2021.instDecidableEqAsymObj : DecidableEq AsymObj

Equations

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

def HawkinsGweonGoodman2021.instReprAsymObj.repr : AsymObj → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance HawkinsGweonGoodman2021.instReprAsymObj : Repr AsymObj

Equations

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

@[implicit_reducible]

instance HawkinsGweonGoodman2021.instInhabitedAsymObj : Inhabited AsymObj

Equations

• HawkinsGweonGoodman2021.instInhabitedAsymObj = { default := HawkinsGweonGoodman2021.instInhabitedAsymObj.default }

@[implicit_reducible]

instance HawkinsGweonGoodman2021.instFintypeAsymObj : Fintype AsymObj

Equations

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

inductive HawkinsGweonGoodman2021.Utt : Type

Utterance: which features to mention (2³ = 8 possible utterances)

• null : Utt
• s : Utt
• c : Utt
• t : Utt
• sc : Utt
• st : Utt
• ct : Utt
• sct : Utt

@[implicit_reducible]

instance HawkinsGweonGoodman2021.instDecidableEqUtt : DecidableEq Utt

Equations

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

def HawkinsGweonGoodman2021.instReprUtt.repr : Utt → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance HawkinsGweonGoodman2021.instReprUtt : Repr Utt

Equations

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

@[implicit_reducible]

instance HawkinsGweonGoodman2021.instInhabitedUtt : Inhabited Utt

Equations

• HawkinsGweonGoodman2021.instInhabitedUtt = { default := HawkinsGweonGoodman2021.instInhabitedUtt.default }

@[implicit_reducible]

instance HawkinsGweonGoodman2021.instFintypeUtt : Fintype Utt

Equations

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

instance HawkinsGweonGoodman2021.instNonemptyVisObj : Nonempty VisObj

instance HawkinsGweonGoodman2021.instNonemptyAsymObj : Nonempty AsymObj

instance HawkinsGweonGoodman2021.instNonemptyUtt : Nonempty Utt

def HawkinsGweonGoodman2021.Utt.cost : Utt → ℕ

Utterance cost: number of features mentioned

Equations

• HawkinsGweonGoodman2021.Utt.null.cost = 0
• HawkinsGweonGoodman2021.Utt.s.cost = 1
• HawkinsGweonGoodman2021.Utt.c.cost = 1
• HawkinsGweonGoodman2021.Utt.t.cost = 1
• HawkinsGweonGoodman2021.Utt.sc.cost = 2
• HawkinsGweonGoodman2021.Utt.st.cost = 2
• HawkinsGweonGoodman2021.Utt.ct.cost = 2
• HawkinsGweonGoodman2021.Utt.sct.cost = 3

Literal semantics

def HawkinsGweonGoodman2021.Utt.applies (u : Utt) (shapeOk colorOk textureOk : Bool) : Bool

Does utterance apply to an entity with given feature-match profile? For each feature the utterance mentions, the entity must match the target.

def HawkinsGweonGoodman2021.egoMeaning (u : Utt) (w : VisObj) : Bool

Egocentric literal meaning: does utterance apply to visible object? Target matches on all features. d1 differs only on shape. d2 differs on all.

Equations

• HawkinsGweonGoodman2021.egoMeaning u HawkinsGweonGoodman2021.VisObj.target = true
• HawkinsGweonGoodman2021.egoMeaning u HawkinsGweonGoodman2021.VisObj.d1 = u.applies false true true
• HawkinsGweonGoodman2021.egoMeaning u HawkinsGweonGoodman2021.VisObj.d2 = u.applies false false false

def HawkinsGweonGoodman2021.asymMeaning (l : Bool × Bool × Bool) (u : Utt) (w : AsymObj) : Bool

Asymmetric literal meaning: includes hidden object behind occlusion. The hidden object's match profile is the latent variable l = (matchShape, matchColor, matchTexture). Each feature independently matches target with P = 1/4.

Equations

• HawkinsGweonGoodman2021.asymMeaning l u HawkinsGweonGoodman2021.AsymObj.target = true
• HawkinsGweonGoodman2021.asymMeaning l u HawkinsGweonGoodman2021.AsymObj.d1 = u.applies false true true
• HawkinsGweonGoodman2021.asymMeaning l u HawkinsGweonGoodman2021.AsymObj.d2 = u.applies false false false
• HawkinsGweonGoodman2021.asymMeaning l u HawkinsGweonGoodman2021.AsymObj.hidden = u.applies l.1 l.2.1 l.2.2

Model

Both configurations use the canonical PMF reference-game operators (RSA.L0OfBoolMeaning, RSA.S1Belief, PMF.posterior), as in Studies/TesslerFranke2020PMF: L0 is uniform on an utterance's extension, S1 is the belief-based speaker with α = 2 and no cost, and L1 is the Bayesian posterior under a uniform world prior. The asymmetric model marginalizes the hidden-object profile via RSA.marginalizeKernel.

Egocentric model

theorem HawkinsGweonGoodman2021.egoExtension_nonempty (u : Utt) : (RSA.extensionOf egoMeaning u).Nonempty

Every utterance applies to the target (it matches on all features), so each extension is non-empty.

noncomputable def HawkinsGweonGoodman2021.egoL0 (u : Utt) : PMF VisObj

Literal listener: uniform on the extension of egoMeaning u.

Equations

• HawkinsGweonGoodman2021.egoL0 u = RSA.L0OfBoolMeaning HawkinsGweonGoodman2021.egoMeaning u ⋯

theorem HawkinsGweonGoodman2021.egoL0_apply_of_false {u : Utt} {w : VisObj} (h : egoMeaning u w ≠ true) : (egoL0 u) w = 0

theorem HawkinsGweonGoodman2021.egoL0_apply_of_true {u : Utt} {w : VisObj} (h : egoMeaning u w = true) : (egoL0 u) w = (↑(RSA.extensionOf egoMeaning u).card)⁻¹

theorem HawkinsGweonGoodman2021.egoL0_ne_zero_of_applies {u : Utt} {w : VisObj} (h : egoMeaning u w = true) : (egoL0 u) w ≠ 0

theorem HawkinsGweonGoodman2021.egoL0_null_ne_zero (w : VisObj) : (egoL0 Utt.null) w ≠ 0

noncomputable def HawkinsGweonGoodman2021.egoS1 (w : VisObj) : PMF Utt

Belief-based speaker: S1(u | w) ∝ L0(w | u)^2, no cost (α = 2).

Equations

• HawkinsGweonGoodman2021.egoS1 w = RSA.S1Belief HawkinsGweonGoodman2021.egoL0 (fun (x : HawkinsGweonGoodman2021.Utt) => 1) 2 w ⋯ ⋯

theorem HawkinsGweonGoodman2021.egoS1_eq_zero_of_not_applies {u : Utt} {w : VisObj} (h : egoMeaning u w ≠ true) : (egoS1 w) u = 0

theorem HawkinsGweonGoodman2021.egoS1_ne_zero_of_applies {u : Utt} {w : VisObj} (h : egoMeaning u w = true) : (egoS1 w) u ≠ 0

noncomputable def HawkinsGweonGoodman2021.egoWorldPrior : PMF VisObj

Uniform world prior over the three visible objects.

Equations

• HawkinsGweonGoodman2021.egoWorldPrior = PMF.uniformOfFintype HawkinsGweonGoodman2021.VisObj

theorem HawkinsGweonGoodman2021.egoMarginal_ne_zero (u : Utt) : PMF.marginal egoS1 egoWorldPrior u ≠ 0

noncomputable def HawkinsGweonGoodman2021.egoL1 (u : Utt) : PMF VisObj

Pragmatic listener: Bayesian posterior of egoS1 under the uniform prior.

Equations

• HawkinsGweonGoodman2021.egoL1 u = PMF.posterior HawkinsGweonGoodman2021.egoS1 HawkinsGweonGoodman2021.egoWorldPrior u ⋯

theorem HawkinsGweonGoodman2021.egoL1_eq_one_of_unique {u : Utt} (h : ∀ (w : VisObj), w ≠ VisObj.target → egoMeaning u w ≠ true) : (egoL1 u) VisObj.target = 1

An utterance applying only to the target makes the listener certain: the posterior puts full mass on the target.

Asymmetric model

The hidden object's feature-match profile is the latent variable Profile, with prior weight 1 for a match and 3 for a non-match on each feature (each feature matches the target with probability 1/4). The speaker is conditioned on the latent; the listener marginalizes it via RSA.marginalizeKernel.

@[reducible, inline]

abbrev HawkinsGweonGoodman2021.Profile : Type

Whether the hidden object matches the target on (shape, color, texture).

Equations

• HawkinsGweonGoodman2021.Profile = (Bool × Bool × Bool)

theorem HawkinsGweonGoodman2021.asymExtension_nonempty (l : Profile) (u : Utt) : (RSA.extensionOf (asymMeaning l) u).Nonempty

noncomputable def HawkinsGweonGoodman2021.asymL0 (l : Profile) (u : Utt) : PMF AsymObj

Literal listener under hidden profile l.

Equations

• HawkinsGweonGoodman2021.asymL0 l u = RSA.L0OfBoolMeaning (HawkinsGweonGoodman2021.asymMeaning l) u ⋯

theorem HawkinsGweonGoodman2021.asymL0_apply_of_false {l : Profile} {u : Utt} {w : AsymObj} (h : asymMeaning l u w ≠ true) : (asymL0 l u) w = 0

theorem HawkinsGweonGoodman2021.asymL0_apply_of_true {l : Profile} {u : Utt} {w : AsymObj} (h : asymMeaning l u w = true) : (asymL0 l u) w = (↑(RSA.extensionOf (asymMeaning l) u).card)⁻¹

theorem HawkinsGweonGoodman2021.asymL0_ne_zero_of_applies {l : Profile} {u : Utt} {w : AsymObj} (h : asymMeaning l u w = true) : (asymL0 l u) w ≠ 0

theorem HawkinsGweonGoodman2021.asymL0_null_ne_zero (l : Profile) (w : AsymObj) : (asymL0 l Utt.null) w ≠ 0

noncomputable def HawkinsGweonGoodman2021.asymS1 (l : Profile) (w : AsymObj) : PMF Utt

Speaker conditioned on the hidden-object profile.

Equations

• HawkinsGweonGoodman2021.asymS1 l w = RSA.S1Belief (HawkinsGweonGoodman2021.asymL0 l) (fun (x : HawkinsGweonGoodman2021.Utt) => 1) 2 w ⋯ ⋯

theorem HawkinsGweonGoodman2021.asymS1_eq_zero_of_not_applies {l : Profile} {u : Utt} {w : AsymObj} (h : asymMeaning l u w ≠ true) : (asymS1 l w) u = 0

theorem HawkinsGweonGoodman2021.asymS1_ne_zero_of_applies {l : Profile} {u : Utt} {w : AsymObj} (h : asymMeaning l u w = true) : (asymS1 l w) u ≠ 0

noncomputable def HawkinsGweonGoodman2021.profileWeight (l : Profile) : ENNReal

Latent prior weight: 1 per matching feature, 3 per non-match.

Equations

• HawkinsGweonGoodman2021.profileWeight l = ((if l.1 = true then 1 else 3) * if l.2.1 = true then 1 else 3) * if l.2.2 = true then 1 else 3

theorem HawkinsGweonGoodman2021.profileWeight_ne_zero (l : Profile) : profileWeight l ≠ 0

theorem HawkinsGweonGoodman2021.profileWeight_ne_top (l : Profile) : profileWeight l ≠ ⊤

noncomputable def HawkinsGweonGoodman2021.latentPrior : PMF Profile

Prior over hidden-object profiles.

Equations

• HawkinsGweonGoodman2021.latentPrior = PMF.normalize HawkinsGweonGoodman2021.profileWeight HawkinsGweonGoodman2021.profileWeight_tsum_ne_zero✝ HawkinsGweonGoodman2021.profileWeight_tsum_ne_top✝

theorem HawkinsGweonGoodman2021.latentPrior_ne_zero (l : Profile) : latentPrior l ≠ 0

noncomputable def HawkinsGweonGoodman2021.asymMarginalSpeaker (w : AsymObj) : PMF Utt

Listener's marginal speaker: hidden profile integrated out.

Equations

• HawkinsGweonGoodman2021.asymMarginalSpeaker w = RSA.marginalizeKernel HawkinsGweonGoodman2021.latentPrior HawkinsGweonGoodman2021.asymS1 w

theorem HawkinsGweonGoodman2021.asymMarginalSpeaker_eq_zero_of_not_applies {u : Utt} {w : AsymObj} (h : ∀ (l : Bool × Bool × Bool), asymMeaning l u w ≠ true) : (asymMarginalSpeaker w) u = 0

theorem HawkinsGweonGoodman2021.asymMarginalSpeaker_ne_zero_of_applies {l : Profile} {u : Utt} {w : AsymObj} (h : asymMeaning l u w = true) : (asymMarginalSpeaker w) u ≠ 0

noncomputable def HawkinsGweonGoodman2021.asymWorldPrior : PMF AsymObj

Uniform world prior over the four objects (three visible + hidden).

Equations

• HawkinsGweonGoodman2021.asymWorldPrior = PMF.uniformOfFintype HawkinsGweonGoodman2021.AsymObj

theorem HawkinsGweonGoodman2021.asymMarginal_ne_zero (u : Utt) : PMF.marginal asymMarginalSpeaker asymWorldPrior u ≠ 0

noncomputable def HawkinsGweonGoodman2021.asymL1 (u : Utt) : PMF AsymObj

Pragmatic listener: posterior of the latent-marginalized speaker.

Equations

• HawkinsGweonGoodman2021.asymL1 u = PMF.posterior HawkinsGweonGoodman2021.asymMarginalSpeaker HawkinsGweonGoodman2021.asymWorldPrior u ⋯

Compositional grounding

The literal semantics is intersective predicate modification [HK98]: each mentioned feature is an intersective adjective — Modifier.intersective applied to a feature property — and grounding_ego_meaning shows egoMeaning is exactly their iterated conjunction. This grounds the Bool RSA meaning in the project-canonical Prop-valued modifier rather than a local copy.

def HawkinsGweonGoodman2021.MontaguGrounding.shapeP (w : VisObj) : Prop

Shape adjective: holds of the target (the only shape-0 object).

Equations

• HawkinsGweonGoodman2021.MontaguGrounding.shapeP w = (w = HawkinsGweonGoodman2021.VisObj.target)

def HawkinsGweonGoodman2021.MontaguGrounding.colorP (w : VisObj) : Prop

Color adjective: holds of the objects sharing the target's color (target, d1).

Equations

• HawkinsGweonGoodman2021.MontaguGrounding.colorP w = (w = HawkinsGweonGoodman2021.VisObj.target ∨ w = HawkinsGweonGoodman2021.VisObj.d1)

def HawkinsGweonGoodman2021.MontaguGrounding.textureP (w : VisObj) : Prop

Texture adjective: holds of the objects sharing the target's texture (target, d1).

Equations

• HawkinsGweonGoodman2021.MontaguGrounding.textureP w = (w = HawkinsGweonGoodman2021.VisObj.target ∨ w = HawkinsGweonGoodman2021.VisObj.d1)

def HawkinsGweonGoodman2021.MontaguGrounding.compositionalMeaning : Utt → VisObj → Prop

Compositional utterance denotation: each mentioned feature is an intersective adjective (Modifier.intersective), composed over the trivial base property.

Equations

• One or more equations did not get rendered due to their size.
• HawkinsGweonGoodman2021.MontaguGrounding.compositionalMeaning HawkinsGweonGoodman2021.Utt.null = fun (x : HawkinsGweonGoodman2021.VisObj) => True

theorem HawkinsGweonGoodman2021.MontaguGrounding.grounding_ego_meaning (u : Utt) (w : VisObj) : egoMeaning u w = true ↔ compositionalMeaning u w

Grounding: the RSA literal meaning egoMeaning holds exactly when the intersective predicate modification of the mentioned feature adjectives does.

Predictions

The egocentric model captures the no-occlusion case; the asymmetric model captures occlusion. Predictions are structural PMF proofs over the canonical operators (no interval reflection).

Egocentric predictions

theorem HawkinsGweonGoodman2021.ego_shape_identifies_target : (egoL1 Utt.s) VisObj.target > (egoL1 Utt.s) VisObj.d1

Shape-only uniquely identifies the target among visible objects: it applies to no other visible object, so the listener concentrates on the target.

theorem HawkinsGweonGoodman2021.ego_shape_as_good_as_full : ¬(egoL1 Utt.sct) VisObj.target > (egoL1 Utt.s) VisObj.target

The listener is equally confident about the target whether hearing shape-only or the full description: both apply only to the target among visible objects, so each makes the listener certain.

theorem HawkinsGweonGoodman2021.ego_S1_indifferent : ¬(egoS1 VisObj.target) Utt.sct > (egoS1 VisObj.target) Utt.s

The speaker is indifferent between shape-only and full description at the target: both apply only to the target, so both have L0 = 1 and equal score.

Asymmetric predictions

theorem HawkinsGweonGoodman2021.asym_S1_prefers_specificity_when_shape_matches : (asymS1 (true, false, false) AsymObj.target) Utt.sct > (asymS1 (true, false, false) AsymObj.target) Utt.s

Paper prediction: when the hidden object matches the target's shape but not its color or texture, the speaker prefers the full description over shape-only — shape-only fails to distinguish the target from the hidden object (L0 = 1/2), while the full description succeeds (L0 = 1).

theorem HawkinsGweonGoodman2021.asym_S1_indifferent_when_no_match : ¬(asymS1 (false, false, false) AsymObj.target) Utt.sct > (asymS1 (false, false, false) AsymObj.target) Utt.s

When the hidden object matches no features, the speaker is indifferent: both shape-only and the full description apply only to the target (L0 = 1).

theorem HawkinsGweonGoodman2021.asym_L1_identifies_target : (asymL1 Utt.s) AsymObj.target > (asymL1 Utt.s) AsymObj.d1

Even under asymmetry, the listener identifies the target over d1: s applies to no d1 profile (it differs in shape), so the speaker never produces s at d1, and the marginal speaker puts zero mass there.

theorem HawkinsGweonGoodman2021.asym_full_desc_better_reference : (asymL1 Utt.sct) AsymObj.target > (asymL1 Utt.s) AsymObj.target

Paper prediction: under asymmetry, the full description yields a higher listener posterior for the target than shape-only — the hidden object can match individual features, so a more specific utterance is more reliably informative.

TODO: this compares two latent-marginalized posteriors at different conditioning utterances (L1 .sct vs L1 .s), with distinct normalizing constants. It reduces to a finite ℝ≥0∞ comparison over the eight hidden profiles but is beyond hand-discharge; it awaits the planned pmf_score_compare tactic (cf. Studies/TesslerFranke2020PMF).

theorem HawkinsGweonGoodman2021.asym_shape_color_beats_shape : (asymL1 Utt.sc) AsymObj.target > (asymL1 Utt.s) AsymObj.target

Shape+color also beats shape-only: each additional feature narrows the set of possible hidden distractors.

TODO: same shape as asym_full_desc_better_reference (cross-utterance latent-marginalized posterior comparison); awaits pmf_score_compare.

Resource-rational extensions

The mixture model and resource-rational optimization sit outside the standard RSA loop. They are defined in ℝ, grounded in the PMF literal listener (egoL0, asymL0, via .toReal) and the hidden-profile prior latentPrior.

The mixture operates in log-space (over utilities, not probabilities): the mixture speaker uses a weighted geometric mean of L0 values, exp(w_S · E[log L0^asym] + (1 − w_S) · log L0^ego). The model uses α = 2 and a uniform cost that cancels in the S1 normalization. See [HGG21] for the asymmetric/egocentric speaker utilities, the mixture, and the resource-rational utility.

L0 success rates

noncomputable def HawkinsGweonGoodman2021.egoInfR (u : Utt) : ℝ

Egocentric L0 success rate: the literal listener's target probability given u, read off egoL0.

Equations

• HawkinsGweonGoodman2021.egoInfR u = ((HawkinsGweonGoodman2021.egoL0 u) HawkinsGweonGoodman2021.VisObj.target).toReal

noncomputable def HawkinsGweonGoodman2021.asymInfR (u : Utt) : ℝ

Asymmetric L0 success rate: the literal listener's target probability averaged over hidden profiles, weighted by latentPrior.

Equations

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

Log-space mixture utilities

noncomputable def HawkinsGweonGoodman2021.asymLogInfR (u : Utt) : ℝ

Expected log-L0 under the asymmetric model (the asymmetric-utility component): E_l[log P_L0(target | u, l)]. By Jensen's inequality this is ≤ log (asymInfR u).

Equations

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

noncomputable def HawkinsGweonGoodman2021.mixUtility (u : Utt) (wS : ℝ) : ℝ

Mixture speaker utility (Eq. 5): U^mix(u; w_S) = w_S · E_h[log P_L0^asym(target|u,h)] + (1−w_S) · log P_L0^ego(target|u) Uniform cost (0.03) omitted: it cancels in S1 normalization.

Equations

• HawkinsGweonGoodman2021.mixUtility u wS = wS * HawkinsGweonGoodman2021.asymLogInfR u + (1 - wS) * Real.log (HawkinsGweonGoodman2021.egoInfR u)

noncomputable def HawkinsGweonGoodman2021.mixS1Score (u : Utt) (wS α : ℝ) : ℝ

Mixture S1 score: P_S1^mix(u | target, w_S) ∝ exp(α · U^mix(u; w_S)). Paper Eq. 1 with the mixture utility from Eq. 5.

Equations

• HawkinsGweonGoodman2021.mixS1Score u wS α = Real.exp (α * HawkinsGweonGoodman2021.mixUtility u wS)

Full resource-rational model

The full model marginalizes over listener perspective-taking weight w_L.

The simplified model (Eqs 2–5) treats w_L as fixed at 1. The full model
(Eqs 7–9) has the speaker consider a range of listener weights, and the
resource-rational analysis (Eq. 10) measures accuracy averaged over w_L.

**Mixture L0** (Eq. 8): P_{L_0}^{mix}(target|u, l, w_L) =
  w_L · P_{L_0}^{asym}(target|u, l) + (1−w_L) · P_{L_0}^{ego}(target|u).
At w_L = 0, the listener ignores hidden objects. At w_L = 1, the listener
accounts for all potential hidden distractors.

**Marginalized S1** (Eq. 9): the speaker's utility integrates over w_L,
discretized to 5 grid points {0, 1/4, 1/2, 3/4, 1} with uniform weight.

**Accuracy** (Eq. 10): since listener accuracy is linear in w_L,
E_{uniform w_L}[accuracy] = (egoInfR + asymInfR) / 2. 

noncomputable def HawkinsGweonGoodman2021.mixL0Target (u : Utt) (l : Profile) (wL : ℝ) : ℝ

Mixture L0 accuracy: probability the mixture listener at weight w_L correctly identifies the target, given hidden object profile l.

Equations

• HawkinsGweonGoodman2021.mixL0Target u l wL = wL * ((HawkinsGweonGoodman2021.asymL0 l u) HawkinsGweonGoodman2021.AsymObj.target).toReal + (1 - wL) * HawkinsGweonGoodman2021.egoInfR u

noncomputable def HawkinsGweonGoodman2021.asymUtilityAtWL (u : Utt) (wL : ℝ) : ℝ

Asymmetric speaker utility at a specific listener weight: U^asym(u; w_L) = Σ_l P(l) · log P_L0^mix(target | u, l, w_L).

Equations

• HawkinsGweonGoodman2021.asymUtilityAtWL u wL = ∑ l : HawkinsGweonGoodman2021.Profile, (HawkinsGweonGoodman2021.latentPrior l).toReal * Real.log (HawkinsGweonGoodman2021.mixL0Target u l wL)

noncomputable def HawkinsGweonGoodman2021.mixUtilityFull (u : Utt) (wS wL : ℝ) : ℝ

Mixed speaker utility at specific (w_S, w_L) (Eq. 8).

Equations

• HawkinsGweonGoodman2021.mixUtilityFull u wS wL = wS * HawkinsGweonGoodman2021.asymUtilityAtWL u wL + (1 - wS) * Real.log (HawkinsGweonGoodman2021.egoInfR u)

noncomputable def HawkinsGweonGoodman2021.mixUtilityMarg (u : Utt) (wS : ℝ) : ℝ

W_L-marginalized speaker utility (Eq. 9 inside the exp). Discretized: 5 uniform grid points at w_L ∈ {0, 1/4, 1/2, 3/4, 1}.

Equations

• HawkinsGweonGoodman2021.mixUtilityMarg u wS = 1 / 5 * ∑ k : Fin 5, HawkinsGweonGoodman2021.mixUtilityFull u wS (↑↑k / 4)

noncomputable def HawkinsGweonGoodman2021.mixS1ScoreFull (u : Utt) (wS α : ℝ) : ℝ

Full S1 score with w_L marginalization (Eq. 9).

Equations

• HawkinsGweonGoodman2021.mixS1ScoreFull u wS α = Real.exp (α * HawkinsGweonGoodman2021.mixUtilityMarg u wS)

noncomputable def HawkinsGweonGoodman2021.avgListenerAccuracy (u : Utt) : ℝ

Listener accuracy averaged over uniform w_L (for Eq. 10). Since accuracy(u, w_L) = w_L·asymInfR(u) + (1−w_L)·egoInfR(u) is linear in w_L, the expectation under uniform P(w_L) is the midpoint.

Equations

• HawkinsGweonGoodman2021.avgListenerAccuracy u = (HawkinsGweonGoodman2021.egoInfR u + HawkinsGweonGoodman2021.asymInfR u) / 2

noncomputable def HawkinsGweonGoodman2021.expectedAccuracyFull (wS α : ℝ) : ℝ

Full expected accuracy (Eq. 10) with w_L marginalization. Uses the w_L-marginalized S1 for speaker production and the w_L-averaged listener accuracy for evaluation.

Equations

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

noncomputable def HawkinsGweonGoodman2021.rrUtilityFull (wS α β : ℝ) : ℝ

Full resource-rational utility (Eqs 10–11). U_RR(w_S) = ExpAccuracy_full(w_S) − β · w_S

Equations

• HawkinsGweonGoodman2021.rrUtilityFull wS α β = HawkinsGweonGoodman2021.expectedAccuracyFull wS α - β * wS

Structural properties

theorem HawkinsGweonGoodman2021.mixUtility_at_zero (u : Utt) : mixUtility u 0 = Real.log (egoInfR u)

At w_S = 0, the simplified mixture utility reduces to egocentric log-L0.

theorem HawkinsGweonGoodman2021.mixUtility_at_one (u : Utt) : mixUtility u 1 = asymLogInfR u

At w_S = 1, the simplified mixture utility reduces to asymmetric expected log-L0.

Resource-rational predictions

These three are transcendental ℝ inequalities over Real.exp/Real.log of the L0 success rates. The retired interval-reflection tactic discharged them with its numeric/interval backend; the PMF migration has no equivalent, so they are stated with sorry per CLAUDE.md "prefer sorry over weakening". They reduce to finite real arithmetic and await real-analysis/interval lemmas (or a pmf_score_compare-style numeric tactic).

theorem HawkinsGweonGoodman2021.no_cost_prefers_full_pt : rrUtilityFull 1 2 0 > rrUtilityFull 0 2 0

Paper prediction (β = 0): when perspective-taking is free, full PT (w_S = 1) achieves higher expected accuracy than no PT (w_S = 0) — the asymmetric speaker produces more specific utterances, improving listener accuracy.

TODO: transcendental ℝ inequality (exp/log of L0 rates); awaits numeric tactic.

theorem HawkinsGweonGoodman2021.high_cost_penalizes_full_pt : rrUtilityFull 0 2 (1 / 2) > rrUtilityFull 1 2 (1 / 2)

Paper prediction (high β): when perspective-taking is costly, the cost term β · w_S dominates, making w_S = 0 preferable to w_S = 1.

TODO: transcendental ℝ inequality (exp/log of L0 rates); awaits numeric tactic.

theorem HawkinsGweonGoodman2021.simplified_game_no_interior_optimum : rrUtilityFull 0 2 (1 / 50) > rrUtilityFull 1 2 (1 / 50)

Interior-optimum limitation: the paper's central result is that at moderate cost (β = 0.2) an intermediate weight w*_S ≈ 0.36 outperforms both extremes. This 3+1-object reference game is too simple to produce that effect: shape alone identifies the target among visible objects (egoInfR .s = 1), so the egocentric baseline accuracy is near-ceiling and the marginal gain from perspective-taking is far below the β = 0.2 cost. So instead no-PT beats full-PT for all tested β ≥ 1/50.

TODO: transcendental ℝ inequality (exp/log of L0 rates); awaits numeric tactic.

Listener belief adaptation

structure HawkinsGweonGoodman2021.ListenerBeliefs : Type

Listener's belief about speaker's perspective-taking weight. Over time, listeners update their expectation of w_S based on observed utterance informativity.

• wS_expectation : ℝ
• observations : ℕ

noncomputable def HawkinsGweonGoodman2021.initialBeliefs : ListenerBeliefs

Initial uniform belief: E[w_S] = 1/2

Equations

• HawkinsGweonGoodman2021.initialBeliefs = { wS_expectation := 1 / 2, observations := 0 }

noncomputable def HawkinsGweonGoodman2021.updateBeliefs (beliefs : ListenerBeliefs) (shortUtterance : Bool) : ListenerBeliefs

Update beliefs after observing utterance informativity. Short/uninformative utterances → lower w_S estimate; long/informative utterances → higher w_S estimate.

Equations

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

noncomputable def HawkinsGweonGoodman2021.beliefsAfterShortUtterances : ListenerBeliefs

After seeing short utterances, listener expects lower w_S

Equations

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

theorem HawkinsGweonGoodman2021.listener_infers_low_wS_from_short_utterances : beliefsAfterShortUtterances.wS_expectation < initialBeliefs.wS_expectation

Paper prediction ([HGG21] §2.4.1): Listeners infer low speaker effort from under-informative utterances.

noncomputable def HawkinsGweonGoodman2021.optimalListenerWeight (speakerWS β : ℝ) : ℝ

Optimal listener weight: compensate for low speaker effort. When the speaker uses low w_S, the listener should increase their own perspective-taking to compensate.

Equations

• HawkinsGweonGoodman2021.optimalListenerWeight speakerWS β = min 1 (max 0 (1 - speakerWS + β))

theorem HawkinsGweonGoodman2021.listener_compensates_for_low_speaker_effort : optimalListenerWeight (3 / 10) (2 / 10) > optimalListenerWeight (7 / 10) (2 / 10)

Paper prediction ([HGG21] §2.4.1): Listener increases effort when speaker decreases theirs.