[FG12] reference game (Measure/Kernel-native)

[FG12]

"Predicting Pragmatic Reasoning in Language Games", Science 336, 998.

The Rational Speech Act model of the paper, on the Measure/Kernel-native analytic foundation of Pragmatics/RSA/Gibbs.lean. The informative speaker (the paper's eq. 2) is a MeasureTheory.Measure.tilted Gibbs measure: Measure.count restricted to the applicable utterances W(r), tilted by the surprisal utility score w = log (1 / |w|). The closed form is exactly

S₁(w | r) ∝ |w|⁻¹ over w ∈ W(r),

[FG12]'s eq. (2). The architectural content — the speaker is a Gibbs measure, monotone in utility, and the rational optimizer of expected-utility-minus- KL (RSA.Gibbs.speaker_isGreatest) — is the substrate; here it is instantiated at the paper's stimulus (Fig. 1A).

The pragmatic listener (eq. 1) is the Bayesian posterior of the speaker against the salience prior, RSA.Gibbs.listener; its pragmatic inferences are driven by the speaker asymmetries proved below (narrowing, unique reference). Empirical fit (speaker r = 0.98, listener r = 0.99) is reported in the paper, not as a theorem here.

Main statements

• prefers_informative — the speaker prefers the uniquely-identifying circle over the ambiguous blue for the target (Fig. 1A); prefers_informative_alpha shows this holds at every rationality α > 0, and fully_rational_picks_circle that the α → ∞ speaker concentrates all its mass on circle (consuming RSA.Gibbs.speakerAlpha and its zero-temperature limit).
• size_principle — generally, the speaker prefers the smaller-extension applicable utterance.
• narrowing_blue / narrowing_square — pragmatic narrowing: the speaker is less likely to use an ambiguous word at a referent that has a uniquely-identifying alternative; this asymmetry is what lets the listener narrow.
• unique_green / unique_circle — unique reference: a uniquely-applying word gets zero mass where it does not apply, so the listener recovers the referent.

Stimulus (Fig. 1A)

Three objects and four feature-words. Two features (green, circle) are uniquely identifying; two (blue, square) are ambiguous between two objects each.

inductive FrankGoodman2012.Object : Type

The three objects in the reference context.

• blueSquare : Object
• blueCircle : Object
• greenSquare : Object

@[implicit_reducible]

instance FrankGoodman2012.instDecidableEqObject : DecidableEq Object

Equations

• FrankGoodman2012.instDecidableEqObject x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance FrankGoodman2012.instFintypeObject : Fintype Object

Equations

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

def FrankGoodman2012.instReprObject.repr : Object → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance FrankGoodman2012.instReprObject : Repr Object

Equations

• FrankGoodman2012.instReprObject = { reprPrec := FrankGoodman2012.instReprObject.repr }

@[implicit_reducible]

instance FrankGoodman2012.instInhabitedObject : Inhabited Object

Equations

• FrankGoodman2012.instInhabitedObject = { default := FrankGoodman2012.instInhabitedObject.default }

inductive FrankGoodman2012.Feature : Type

The four feature-word utterances.

• blue : Feature
• green : Feature
• square : Feature
• circle : Feature

@[implicit_reducible]

instance FrankGoodman2012.instDecidableEqFeature : DecidableEq Feature

Equations

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

@[implicit_reducible]

instance FrankGoodman2012.instFintypeFeature : Fintype Feature

Equations

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

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

Equations

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

@[implicit_reducible]

instance FrankGoodman2012.instReprFeature : Repr Feature

Equations

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

@[implicit_reducible]

instance FrankGoodman2012.instInhabitedFeature : Inhabited Feature

Equations

• FrankGoodman2012.instInhabitedFeature = { default := FrankGoodman2012.instInhabitedFeature.default }

@[implicit_reducible]

instance FrankGoodman2012.instMeasurableSpaceFeature : MeasurableSpace Feature

Equations

• FrankGoodman2012.instMeasurableSpaceFeature = ⊤

instance FrankGoodman2012.instMeasurableSingletonClassFeature : MeasurableSingletonClass Feature

def FrankGoodman2012.appliesTo : Feature → Object → Bool

The denotation matrix: which feature applies to which object.

Equations

• FrankGoodman2012.appliesTo FrankGoodman2012.Feature.blue FrankGoodman2012.Object.blueSquare = true
• FrankGoodman2012.appliesTo FrankGoodman2012.Feature.blue FrankGoodman2012.Object.blueCircle = true
• FrankGoodman2012.appliesTo FrankGoodman2012.Feature.green FrankGoodman2012.Object.greenSquare = true
• FrankGoodman2012.appliesTo FrankGoodman2012.Feature.square FrankGoodman2012.Object.blueSquare = true
• FrankGoodman2012.appliesTo FrankGoodman2012.Feature.square FrankGoodman2012.Object.greenSquare = true
• FrankGoodman2012.appliesTo FrankGoodman2012.Feature.circle FrankGoodman2012.Object.blueCircle = true
• FrankGoodman2012.appliesTo x✝¹ x✝ = false

def FrankGoodman2012.applicable (r : Object) : Finset Feature

The applicable utterances at a referent — [FG12]'s W(r), the support over which the speaker normalizes.

Equations

• FrankGoodman2012.applicable r = {w : FrankGoodman2012.Feature | FrankGoodman2012.appliesTo w r = true}

def FrankGoodman2012.numApplies (w : Feature) : ℕ

The extension size |w| — the number of objects the feature applies to.

Equations

• FrankGoodman2012.numApplies w = {o : FrankGoodman2012.Object | FrankGoodman2012.appliesTo w o = true}.card

noncomputable def FrankGoodman2012.score (w : Feature) : ℝ

Informativity utility (rationality α = 1, no cost): the surprisal score w = log (1 / |w|) = - log |w|. Tilting by this realizes eq. (2)'s |w|⁻¹.

Equations

• FrankGoodman2012.score w = -Real.log ↑(FrankGoodman2012.numApplies w)

noncomputable def FrankGoodman2012.speakerAt (r : Object) : MeasureTheory.Measure Feature

The informative speaker (eq. 2): the Gibbs measure tilting Measure.count restricted to the applicable utterances W(r) by the surprisal score.

Equations

• FrankGoodman2012.speakerAt r = RSA.Gibbs.speaker (MeasureTheory.Measure.count.restrict ↑(FrankGoodman2012.applicable r)) FrankGoodman2012.score

Speaker API at this stimulus

These wrappers carry by decide defaults for the applicability side-conditions, so the concrete predictions below never spell out w ∈ applicable r proofs.

theorem FrankGoodman2012.speakerAt_apply (r : Object) (w : Feature) (h : w ∈ applicable r := by decide) : (speakerAt r) {w} = ENNReal.ofReal (Real.exp (score w) / ∑ x ∈ applicable r, Real.exp (score x))

At an applicable utterance, the speaker mass is the softmax over W(r).

theorem FrankGoodman2012.speakerAt_apply_zero (r : Object) (w : Feature) (h : w ∉ applicable r := by decide) : (speakerAt r) {w} = 0

A non-applicable utterance gets zero speaker mass.

theorem FrankGoodman2012.speakerAt_lt_iff (r : Object) (w₁ w₂ : Feature) (h₁ : w₁ ∈ applicable r := by decide) (h₂ : w₂ ∈ applicable r := by decide) : (speakerAt r) {w₁} < (speakerAt r) {w₂} ↔ score w₁ < score w₂

Speaker preference at a referent reduces to the surprisal comparison.

theorem FrankGoodman2012.speakerAtAlpha_lt_iff (r : Object) {α : ℝ} (hα : 0 < α) (w₁ w₂ : Feature) (h₁ : w₁ ∈ applicable r := by decide) (h₂ : w₂ ∈ applicable r := by decide) : (RSA.Gibbs.speakerAlpha (MeasureTheory.Measure.count.restrict ↑(applicable r)) α score) {w₁} < (RSA.Gibbs.speakerAlpha (MeasureTheory.Measure.count.restrict ↑(applicable r)) α score) {w₂} ↔ score w₁ < score w₂

α-speaker preference at a referent (α > 0) reduces to the surprisal comparison.

Numerical bookkeeping

Predictions

theorem FrankGoodman2012.prefers_informative : (speakerAt Object.blueCircle) {Feature.blue} < (speakerAt Object.blueCircle) {Feature.circle}

The speaker prefers the uniquely-identifying description (Fig. 1A): for the target (blueCircle), circle (which uniquely identifies it) gets strictly more mass than the ambiguous blue. Reduces via speaker_countRestrict_lt_iff_score_lt to the surprisal comparison score blue < score circle.

theorem FrankGoodman2012.prefers_informative_alpha {α : ℝ} (hα : 0 < α) : (RSA.Gibbs.speakerAlpha (MeasureTheory.Measure.count.restrict ↑(applicable Object.blueCircle)) α score) {Feature.blue} < (RSA.Gibbs.speakerAlpha (MeasureTheory.Measure.count.restrict ↑(applicable Object.blueCircle)) α score) {Feature.circle}

Robustness to rationality: the informativeness preference holds at every rationality level α > 0, not just the canonical α = 1 (prefers_informative). A consumer of the α-generalized speaker RSA.Gibbs.speakerAlpha.

theorem FrankGoodman2012.fully_rational_picks_circle : Filter.Tendsto (fun (α : ℝ) => (RSA.Gibbs.speakerAlpha (MeasureTheory.Measure.count.restrict ↑(applicable Object.blueCircle)) α score) {Feature.circle}) Filter.atTop (nhds 1)

The fully-rational speaker is deterministic (α → ∞): at the target, the speaker concentrates all its mass on the uniquely-identifying circle. The zero-temperature limit of prefers_informative, via RSA.Gibbs.speakerAlpha_countRestrict_tendsto_one_of_isMax.

theorem FrankGoodman2012.size_principle (r : Object) (w₁ w₂ : Feature) (h₁ : w₁ ∈ applicable r) (h₂ : w₂ ∈ applicable r) (h : numApplies w₂ < numApplies w₁) : (speakerAt r) {w₁} < (speakerAt r) {w₂}

Size principle: among applicable utterances, the speaker prefers the one with the smaller extension (lower numApplies).

theorem FrankGoodman2012.narrowing_blue : (speakerAt Object.blueCircle) {Feature.blue} < (speakerAt Object.blueSquare) {Feature.blue}

Pragmatic narrowing for "blue": the speaker assigns less mass to "blue" at blueCircle (where "circle" uniquely identifies, raising the partition) than at blueSquare (where the only alternative "square" is equally ambiguous). The numerators are equal; the comparison is the partition comparison 3/2 > 1 — which is what lets a listener hearing "blue" narrow toward blueSquare.

theorem FrankGoodman2012.narrowing_square : (speakerAt Object.greenSquare) {Feature.square} < (speakerAt Object.blueSquare) {Feature.square}

Pragmatic narrowing for "square": symmetrically, "square" is less likely at greenSquare (where "green" uniquely identifies) than at blueSquare.

theorem FrankGoodman2012.unique_green : (speakerAt Object.blueSquare) {Feature.green} < (speakerAt Object.greenSquare) {Feature.green}

Unique reference for "green": "green" applies only to greenSquare, so it gets zero mass at blueSquare and positive mass at greenSquare — the listener hearing "green" identifies greenSquare.

theorem FrankGoodman2012.unique_circle : (speakerAt Object.blueSquare) {Feature.circle} < (speakerAt Object.blueCircle) {Feature.circle}

Unique reference for "circle": "circle" applies only to blueCircle.