================================================================ PART I: EMPIRICAL DATA ================================================================

Experimental Design

Experiment 1: Speaker Production

• 83 dyads on Amazon MTurk
• 2×2 design: occlusions (present/absent) × distractor (present/absent)
• DV: Number of words in referring expression

Experiment 2: Listener Comprehension

• 116 dyads
• Scripted vs unscripted speaker condition
• Replication of @cite{keysar-etal-2003} materials

Key Empirical Findings

1. Speakers increase informativity with occlusions (Exp 1)

• Occlusion effect: +1.3 words (t(120.3) = 8.8, p < .001)
• Distractor effect: +0.6 words (t(206) = 5.7, p < .001)
• Significant interaction (b = -0.49, t(1742) = 4.1, p < .001)

2. Scripted utterances cause more errors (Exp 2)

• Scripted condition: 51% critical errors
• Unscripted condition: 20% critical errors
• χ²(1) = 43, p < .001

3. Listeners adapt over time

• Error rate decreases across trials: z = 2.6, p < 0.01
• From 43% on first critical trial to 30% on fourth trial

4. Speaker informativity predicts listener accuracy

• Correlation: ρ = -0.81, 95% CI = [-0.9, -0.7]
• More informative utterances → fewer errors

inductive HawkinsGweonGoodman2021.PerspectiveState : Type

Visual perspective state in director-matcher task

• ownPrivate : PerspectiveState
• shared : PerspectiveState
• partnerPrivate : PerspectiveState

@[implicit_reducible]

instance HawkinsGweonGoodman2021.instDecidableEqPerspectiveState : DecidableEq PerspectiveState

Equations

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

def HawkinsGweonGoodman2021.instReprPerspectiveState.repr : PerspectiveState → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance HawkinsGweonGoodman2021.instReprPerspectiveState : Repr PerspectiveState

Equations

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

structure HawkinsGweonGoodman2021.Exp1TrialType : Type

Trial type in Experiment 1

• occlusionPresent : Bool
• distractorPresent : Bool

@[implicit_reducible]

instance HawkinsGweonGoodman2021.instDecidableEqExp1TrialType : DecidableEq Exp1TrialType

Equations

• HawkinsGweonGoodman2021.instDecidableEqExp1TrialType = HawkinsGweonGoodman2021.instDecidableEqExp1TrialType.decEq

def HawkinsGweonGoodman2021.instDecidableEqExp1TrialType.decEq (x✝ x✝¹ : Exp1TrialType) : Decidable (x✝ = x✝¹)

Equations

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

def HawkinsGweonGoodman2021.instReprExp1TrialType.repr : Exp1TrialType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance HawkinsGweonGoodman2021.instReprExp1TrialType : Repr Exp1TrialType

Equations

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

def HawkinsGweonGoodman2021.exp1TrialTypes : List Exp1TrialType

All trial types in 2×2 design

Equations

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

def HawkinsGweonGoodman2021.exp1MeanWords : Exp1TrialType → ℚ

Mean words produced in each condition

Equations

• HawkinsGweonGoodman2021.exp1MeanWords { occlusionPresent := false, distractorPresent := false } = 15 / 10
• HawkinsGweonGoodman2021.exp1MeanWords { occlusionPresent := false, distractorPresent := true } = 21 / 10
• HawkinsGweonGoodman2021.exp1MeanWords { occlusionPresent := true, distractorPresent := false } = 28 / 10
• HawkinsGweonGoodman2021.exp1MeanWords { occlusionPresent := true, distractorPresent := true } = 31 / 10

def HawkinsGweonGoodman2021.occlusionEffect : ℚ

Occlusion effect size (distractor-absent): +1.3 words

Equations

• HawkinsGweonGoodman2021.occlusionEffect = 13 / 10

def HawkinsGweonGoodman2021.distractorEffect : ℚ

Distractor effect size (occlusion-absent): +0.6 words

Equations

• HawkinsGweonGoodman2021.distractorEffect = 6 / 10

structure HawkinsGweonGoodman2021.FeatureMentionRates : Type

Feature mention rates by condition (Exp 1, Figure 4B)

• shape : ℚ
• color : ℚ
• texture : ℚ

def HawkinsGweonGoodman2021.instReprFeatureMentionRates.repr : FeatureMentionRates → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance HawkinsGweonGoodman2021.instReprFeatureMentionRates : Repr FeatureMentionRates

Equations

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

def HawkinsGweonGoodman2021.featureRates_noOcclusion_noDistractor : FeatureMentionRates

Occlusion increases feature mention rates (distractor-absent)

Equations

• HawkinsGweonGoodman2021.featureRates_noOcclusion_noDistractor = { shape := 99 / 100, color := 25 / 100, texture := 5 / 100 }

def HawkinsGweonGoodman2021.featureRates_occlusion_noDistractor : FeatureMentionRates

Equations

• HawkinsGweonGoodman2021.featureRates_occlusion_noDistractor = { shape := 99 / 100, color := 50 / 100, texture := 65 / 100 }

inductive HawkinsGweonGoodman2021.SpeakerCondition : Type

Speaker condition in Experiment 2

• scripted : SpeakerCondition
• unscripted : SpeakerCondition

@[implicit_reducible]

instance HawkinsGweonGoodman2021.instDecidableEqSpeakerCondition : DecidableEq SpeakerCondition

Equations

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

def HawkinsGweonGoodman2021.instReprSpeakerCondition.repr : SpeakerCondition → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance HawkinsGweonGoodman2021.instReprSpeakerCondition : Repr SpeakerCondition

Equations

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

def HawkinsGweonGoodman2021.criticalErrorRate : SpeakerCondition → ℚ

Critical error rate by condition

Equations

• HawkinsGweonGoodman2021.criticalErrorRate HawkinsGweonGoodman2021.SpeakerCondition.scripted = 51 / 100
• HawkinsGweonGoodman2021.criticalErrorRate HawkinsGweonGoodman2021.SpeakerCondition.unscripted = 20 / 100

def HawkinsGweonGoodman2021.errorRateByTrial : ℕ → ℚ

Error rate by trial number (adaptation over time)

Equations

• HawkinsGweonGoodman2021.errorRateByTrial 1 = 43 / 100
• HawkinsGweonGoodman2021.errorRateByTrial 2 = 38 / 100
• HawkinsGweonGoodman2021.errorRateByTrial 3 = 34 / 100
• HawkinsGweonGoodman2021.errorRateByTrial 4 = 30 / 100
• HawkinsGweonGoodman2021.errorRateByTrial x✝ = 30 / 100

theorem HawkinsGweonGoodman2021.errors_decrease_over_trials : errorRateByTrial 4 < errorRateByTrial 1

Listeners adapt: errors decrease over trials

structure HawkinsGweonGoodman2021.InformativityRating : Type

Informativity: how well utterance fits target vs distractor

• targetFit : ℚ
• distractorFit : ℚ

def HawkinsGweonGoodman2021.instReprInformativityRating.repr : InformativityRating → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance HawkinsGweonGoodman2021.instReprInformativityRating : Repr InformativityRating

Equations

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

def HawkinsGweonGoodman2021.informativityDiff (r : InformativityRating) : ℚ

Informativity difference: target fit - distractor fit

Equations

• HawkinsGweonGoodman2021.informativityDiff r = r.targetFit - r.distractorFit

def HawkinsGweonGoodman2021.scriptedInformativity : InformativityRating

Scripted utterances: roughly equal fit (by design)

Equations

• HawkinsGweonGoodman2021.scriptedInformativity = { targetFit := 50 / 100, distractorFit := 52 / 100 }

def HawkinsGweonGoodman2021.unscriptedInformativity : InformativityRating

Unscripted utterances: much better target fit

Equations

• HawkinsGweonGoodman2021.unscriptedInformativity = { targetFit := 75 / 100, distractorFit := 25 / 100 }

theorem HawkinsGweonGoodman2021.unscripted_more_informative : informativityDiff unscriptedInformativity > informativityDiff scriptedInformativity

Unscripted speakers are more informative

def HawkinsGweonGoodman2021.informativityErrorCorrelation : ℚ

Informativity-error correlation: ρ = -0.81

Equations

• HawkinsGweonGoodman2021.informativityErrorCorrelation = -81 / 100

inductive HawkinsGweonGoodman2021.KeyPrediction : Type

The paper identifies these key qualitative predictions:

1. Speakers hedge against known unknowns: Increase informativity with occlusions
2. Division of labor depends on expectations: Optimal effort = f(partner's expected effort)
3. Listeners adapt to speaker behavior: Update beliefs about speaker's effort over time
4. Intermediate weights are optimal: When perspective-taking is costly, partial weighting is best

• speakersHedgeUnknowns : KeyPrediction
• divisionDependsOnPartner : KeyPrediction
• listenersAdaptOverTime : KeyPrediction
• intermediateWeightsOptimal : KeyPrediction

@[implicit_reducible]

instance HawkinsGweonGoodman2021.instDecidableEqKeyPrediction : DecidableEq KeyPrediction

Equations

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

def HawkinsGweonGoodman2021.instReprKeyPrediction.repr : KeyPrediction → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance HawkinsGweonGoodman2021.instReprKeyPrediction : Repr KeyPrediction

Equations

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

def HawkinsGweonGoodman2021.keyPredictions : List KeyPrediction

All key predictions from the paper

Equations

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

structure HawkinsGweonGoodman2021.CriticalItem : Type

Critical item from @cite{keysar-etal-2003} replication

• instruction : String
• target : String
• hiddenDistractor : String

@[implicit_reducible]

instance HawkinsGweonGoodman2021.instReprCriticalItem : Repr CriticalItem

Equations

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

def HawkinsGweonGoodman2021.instReprCriticalItem.repr : CriticalItem → ℕ → Std.Format

Equations

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

def HawkinsGweonGoodman2021.criticalItems : List CriticalItem

The 8 critical items used in Experiment 2

Equations

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

theorem HawkinsGweonGoodman2021.eight_critical_items : criticalItems.length = 8

Number of critical items

================================================================ PART II: RSA MODEL ================================================================

Two RSAConfig instances formalize the reference game:

• cfgEgo (egocentric): 3 visible objects, no hidden. Belief-based S1.
• cfgAsym (asymmetric): 3 visible + 1 hidden object. Latent variable encodes the hidden object's match profile (which features match target). Prior reflects P(match) = 1/4 per feature (uniform over 4 values).

Utterance semantics derive from predicate modification (Part III): each feature word is an intersective adjective, composed via predMod.

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 }

def HawkinsGweonGoodman2021.instInhabitedVisObj.default : VisObj

Equations

• HawkinsGweonGoodman2021.instInhabitedVisObj.default = HawkinsGweonGoodman2021.VisObj.target

@[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 ⋯

@[implicit_reducible]

instance HawkinsGweonGoodman2021.instReprAsymObj : Repr AsymObj

Equations

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

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

Equations

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

def HawkinsGweonGoodman2021.instInhabitedAsymObj.default : AsymObj

Equations

• HawkinsGweonGoodman2021.instInhabitedAsymObj.default = HawkinsGweonGoodman2021.AsymObj.target

@[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 }

def HawkinsGweonGoodman2021.instInhabitedUtt.default : Utt

Equations

• HawkinsGweonGoodman2021.instInhabitedUtt.default = HawkinsGweonGoodman2021.Utt.null

@[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

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

noncomputable def HawkinsGweonGoodman2021.cfgEgo : RSA.RSAConfig Utt VisObj

Egocentric RSA: reference game among 3 visible objects. Belief-based scoring (S1 score = L0^α), α = 2, uniform priors.

Equations

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

noncomputable def HawkinsGweonGoodman2021.cfgAsym : RSA.RSAConfig Utt AsymObj

Asymmetric RSA: reference game with hidden object behind occlusion. Latent = (matchShape, matchColor, matchTexture) for hidden object. Prior: each feature independently matches target with probability 1/4, encoded as unnormalized weights (1 for match, 3 for non-match).

Equations

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

================================================================ PART III: COMPOSITIONAL GROUNDING ================================================================

The utterance semantics derive from predicate modification (H&K Ch. 4):

⟦α β⟧ = λx. ⟦α⟧(x) ∧ ⟦β⟧(x)

Each feature mention (shape, color, texture) is an intersective adjective that denotes a characteristic function of type e → t:

• ⟦square⟧ = λx. shape(x) = target.shape
• ⟦blue⟧ = λx. color(x) = target.color
• ⟦checked⟧ = λx. texture(x) = target.texture

This is exactly Semantics.Composition.Modification.predMod applied iteratively.

def HawkinsGweonGoodman2021.MontaguGrounding.shapePred : VisObj → Bool

Shape predicate: matches target's shape (only target has shape=0)

Equations

• HawkinsGweonGoodman2021.MontaguGrounding.shapePred HawkinsGweonGoodman2021.VisObj.target = true
• HawkinsGweonGoodman2021.MontaguGrounding.shapePred x✝ = false

def HawkinsGweonGoodman2021.MontaguGrounding.colorPred : VisObj → Bool

Color predicate: matches target's color (target + d1 have color=0)

Equations

• HawkinsGweonGoodman2021.MontaguGrounding.colorPred HawkinsGweonGoodman2021.VisObj.target = true
• HawkinsGweonGoodman2021.MontaguGrounding.colorPred HawkinsGweonGoodman2021.VisObj.d1 = true
• HawkinsGweonGoodman2021.MontaguGrounding.colorPred HawkinsGweonGoodman2021.VisObj.d2 = false

def HawkinsGweonGoodman2021.MontaguGrounding.texturePred : VisObj → Bool

Texture predicate: matches target's texture (target + d1 have texture=0)

Equations

• HawkinsGweonGoodman2021.MontaguGrounding.texturePred HawkinsGweonGoodman2021.VisObj.target = true
• HawkinsGweonGoodman2021.MontaguGrounding.texturePred HawkinsGweonGoodman2021.VisObj.d1 = true
• HawkinsGweonGoodman2021.MontaguGrounding.texturePred HawkinsGweonGoodman2021.VisObj.d2 = false

def HawkinsGweonGoodman2021.MontaguGrounding.compositionalMeaning (u : Utt) : VisObj → Bool

Compositional utterance denotation via intersective predicate modification. Each mentioned feature contributes an intersective adjective, composed left-to-right via predMod.

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

Grounding theorem: egoMeaning equals the compositional derivation. The ad-hoc semantics match Montague intersective predicate modification.

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

The RSA meaning function is grounded in compositional semantics

================================================================ PART IV: PREDICTIONS VIA rsa_predict ================================================================

Core RSA predictions verified via rsa_predict. The egocentric model captures the no-occlusion case; the asymmetric model captures occlusion.

theorem HawkinsGweonGoodman2021.ego_shape_identifies_target : cfgEgo.L1 Utt.s VisObj.target > cfgEgo.L1 Utt.s VisObj.d1

Shape-only uniquely identifies target among visible objects.

theorem HawkinsGweonGoodman2021.ego_shape_as_good_as_full : ¬cfgEgo.L1 Utt.sct VisObj.target > cfgEgo.L1 Utt.s VisObj.target

In the egocentric model, the listener is equally confident about the target whether hearing shape-only or full description. Both uniquely identify target among visible objects, so additional features add nothing.

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

S1 is indifferent between shape-only and full description for target (both have L0 = 1 among visible objects).

theorem HawkinsGweonGoodman2021.asym_full_desc_better_reference : cfgAsym.L1 Utt.sct AsymObj.target > cfgAsym.L1 Utt.s AsymObj.target

Paper Prediction 1: Full description produces higher L1 posterior for target than shape-only under asymmetry. Hidden objects can match individual features (P(match_shape) = 1/4), so more specific utterances are more reliably informative.

theorem HawkinsGweonGoodman2021.asym_shape_color_beats_shape : cfgAsym.L1 Utt.sc AsymObj.target > cfgAsym.L1 Utt.s AsymObj.target

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

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

When hidden object matches target's shape (but not color or texture), S1 prefers full description over shape-only. Shape-only fails to distinguish target from hidden; full description succeeds.

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

When hidden matches no features, S1 is indifferent: both shape-only and full description have L0 = 1 for target.

theorem HawkinsGweonGoodman2021.asym_L1_identifies_target : cfgAsym.L1 Utt.s AsymObj.target > cfgAsym.L1 Utt.s AsymObj.d1

Even under asymmetry, L1 correctly identifies target over d1 (which differs in shape).

================================================================ PART V: EXTENSIONS (Mixture Model & Resource-Rational Analysis) ================================================================

The mixture model (Eq. 5) and resource-rational optimization (Eq. 10-11) sit outside the standard RSA loop. These are paper-specific extensions, defined in ℝ and grounded in RSAConfig.L0.

Key equations from the paper:

• Eq. 2: U^asym_S1(u;o,C) = Σ_{o_h} P(o_h) log P_L0(o|u,C ∪ {o_h}) − cost(u)
• Eq. 3: U^ego_S1(u;o,C) = log P_L0(o|u,C) − cost(u)
• Eq. 5: U^mix_S1 = w_S · U^asym + (1−w_S) · U^ego
• Eq. 10: U_{S_RR}(w_S) = E_{P(w_L)}[P_L0(o|u*,C,w_L)] − β × w_S

The mixture operates in log-space (over utilities, not probabilities). This means the mixture speaker uses a weighted geometric mean of L0 values, not an arithmetic mean: exp(w_S · E[log L0^asym] + (1−w_S) · log L0^ego).

Parameters: α = 2, cost(u) = 0.03 (uniform, cancels in S1 normalization).

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

Egocentric L0 success rate: P_L0^ego(target | u). Grounded directly in cfgEgo.L0.

Equations

• HawkinsGweonGoodman2021.egoInfR u = HawkinsGweonGoodman2021.cfgEgo.L0 () u HawkinsGweonGoodman2021.VisObj.target

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

Asymmetric L0 success rate: E_l[P_L0^asym(target | u, l)]. Marginalizes the literal listener's success over hidden object profiles, weighted by the latent prior.

Equations

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

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

Expected log-L0 under the asymmetric model (Eq. 2, utility component): E_h[log P_L0(target | u, C ∪ {h})]. This is inside the expectation, so by Jensen's inequality asymLogInfR(u) ≤ 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)

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 : Bool × Bool × Bool) (wL : ℝ) : ℝ

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

Equations

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

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

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

Equations

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

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

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.

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. (Paper Figure 2, rightmost point of β = 0 curve.)

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. (Paper Figure 2, β = 0.5 curve.)

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 (§2.4, Figure 2) is that at moderate cost (β = 0.2), an intermediate weight w*_S ≈ 0.36 outperforms both extremes.

Our 3+1 object reference game is too simple to produce this effect. Shape alone uniquely identifies the target among visible objects (egoInfR .s = 1), so the egocentric baseline accuracy is ≈97%. The marginal accuracy gain from perspective-taking is ≈0.3%, far below the β = 0.2 cost. The interior optimum requires a richer display where egocentric accuracy is substantially lower, creating a larger incentive for specific utterances that disambiguate from hidden objects.

Verified: rrUtilityFull 0 2 β > rrUtilityFull 1 2 β for all tested β ≥ 1/50 (even with the full w_L-marginalized model).

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 (@cite{hawkins-gweon-goodman-2021} §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 (@cite{hawkins-gweon-goodman-2021} §2.4.1): Listener increases effort when speaker decreases theirs.