@cite{frank-goodman-2012} reference game (concrete instance)

@cite{frank-goodman-2012}

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

What this file is

A concrete instance of the parametric reference-game substrate (Theories/Pragmatics/RSA/ReferenceGame.lean). Everything architectural — the size principle, pragmatic narrowing, unique reference — is proved generically there, parametric in the meaning matrix and world prior. Here we only need to:

1. Define the specific stimulus (3 objects, 4 features, denotation matrix).
2. Verify it satisfies IsCovering.
3. Compute three partition function values.
4. Derive the 4 paper findings as one-liner corollaries.

Why split it this way

Every RSA paper using a "speaker normalises inverse-extension-size" pattern inherits the substrate theorems unchanged. The pragmatic-narrowing theorem is proved once, parametric in everything; FG12's specific findings are its instantiation at the paper's stimulus. Per-stimulus arithmetic is a small section of bookkeeping; the architectural content lives in the substrate.

For RSA practitioners: this is the version where you don't re-derive Eq. S1 → S4 per paper. You instantiate.

§1. Stimulus

Fig. 1C of the paper: three objects (blue square, blue circle, green square) and four feature-words (blue, green, square, circle). 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.

• blue_square : Object
• blue_circle : Object
• green_square : 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.instReprObject : Repr Object

Equations

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

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

Equations

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

@[implicit_reducible]

instance FrankGoodman2012.instInhabitedObject : Inhabited Object

Equations

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

def FrankGoodman2012.instInhabitedObject.default : Object

Equations

• FrankGoodman2012.instInhabitedObject.default = FrankGoodman2012.Object.blue_square

@[implicit_reducible]

instance FrankGoodman2012.instFintypeObject : Fintype Object

Equations

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

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 ⋯

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 }

def FrankGoodman2012.instInhabitedFeature.default : Feature

Equations

• FrankGoodman2012.instInhabitedFeature.default = FrankGoodman2012.Feature.blue

@[implicit_reducible]

instance FrankGoodman2012.instFintypeFeature : Fintype Feature

Equations

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

def FrankGoodman2012.Feature.appliesTo : Feature → Object → Bool

The denotation matrix: which feature applies to which object.

Equations

• FrankGoodman2012.Feature.blue.appliesTo FrankGoodman2012.Object.blue_square = true
• FrankGoodman2012.Feature.blue.appliesTo FrankGoodman2012.Object.blue_circle = true
• FrankGoodman2012.Feature.green.appliesTo FrankGoodman2012.Object.green_square = true
• FrankGoodman2012.Feature.square.appliesTo FrankGoodman2012.Object.blue_square = true
• FrankGoodman2012.Feature.square.appliesTo FrankGoodman2012.Object.green_square = true
• FrankGoodman2012.Feature.circle.appliesTo FrankGoodman2012.Object.blue_circle = true
• x✝¹.appliesTo x✝ = false

instance FrankGoodman2012.instCovering : RSA.ReferenceGame.IsCovering Feature.appliesTo

The stimulus is covering: every feature names some object, and every object is named by some feature.

§2. Numerical bookkeeping (partition function values)

The partition function partition w = Σ_u L0 u w measures the size-principle weight of all alternatives at world w. Three distinct values arise on this stimulus, each corresponding to a different alternative-set composition.

theorem FrankGoodman2012.partition_blue_square : RSA.ReferenceGame.partition Feature.appliesTo Object.blue_square = 1

Partition at .blue_square: alternatives {blue, square} each with extension size 2 contribute 1/2 each; total 1.

theorem FrankGoodman2012.partition_blue_circle : RSA.ReferenceGame.partition Feature.appliesTo Object.blue_circle = 3 / 2

Partition at .blue_circle: {blue, circle} with extension sizes 2 and 1 — circle is uniquely identifying; total 1/2 + 1 = 3/2.

theorem FrankGoodman2012.partition_green_square : RSA.ReferenceGame.partition Feature.appliesTo Object.green_square = 3 / 2

Partition at .green_square: {green, square} with extension sizes 1 and 2 — green is uniquely identifying; total 1 + 1/2 = 3/2.

§3. The four paper findings — one-liner corollaries

Each finding follows from one architectural theorem in the substrate applied to one partition comparison.

theorem FrankGoodman2012.blue_pragmatic_narrowing : (RSA.ReferenceGame.S1 Feature.appliesTo Object.blue_circle) Feature.blue < (RSA.ReferenceGame.S1 Feature.appliesTo Object.blue_square) Feature.blue

Pragmatic narrowing for "blue": a speaker wanting .blue_circle would say "circle" (uniquely identifying — its partition contribution is 1). Saying "blue" instead signals .blue_square, where the alternative- set partition is smaller.

theorem FrankGoodman2012.square_pragmatic_narrowing : (RSA.ReferenceGame.S1 Feature.appliesTo Object.green_square) Feature.square < (RSA.ReferenceGame.S1 Feature.appliesTo Object.blue_square) Feature.square

Pragmatic narrowing for "square": a speaker wanting .green_square would say "green" (uniquely identifying). Saying "square" instead signals .blue_square.

theorem FrankGoodman2012.green_unique_reference : (RSA.ReferenceGame.S1 Feature.appliesTo Object.blue_square) Feature.green < (RSA.ReferenceGame.S1 Feature.appliesTo Object.green_square) Feature.green

Unique reference for "green": "green" applies only to .green_square, so the speaker prefers it there over any other world.

theorem FrankGoodman2012.circle_unique_reference : (RSA.ReferenceGame.S1 Feature.appliesTo Object.blue_square) Feature.circle < (RSA.ReferenceGame.S1 Feature.appliesTo Object.blue_circle) Feature.circle

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