Frank and Goodman (2012): Predicting Pragmatic Reasoning in Language Games

Frank and Goodman's rational speech act model of reference games. A context is a model M whose objects vary on two dimensions, colour and shape, and a word names a colour or a shape. The extension ⟦w⟧ᴹ of a word is the set of objects with the colour or the shape it names, so a word is true of the objects in its extension. The literal listener hears a word as the uniform distribution over its extension. A speaker who wants to refer to an object chooses a word in proportion to the literal listener's probability of the object, the reciprocal of the size of the word's extension, and the listener inverts the speaker against a prior, the salience of the objects. The paper reports the fit of speaker and listener bets to the model.

Main statements

• size_principle: of two words true of an object the speaker prefers the one with the smaller extension.
• speaker_real_singleton_lt_iff, listener_real_singleton_lt_iff: of two objects a word is true of, the speaker uses the word more for the one whose other feature more objects share, and a listener with no prior preference between the two infers that one.
• prefers_informative, narrowing_blue, listener_narrows_blue: in the context of the paper's figure the speaker prefers circle to blue for the blue circle and uses blue less for it than for the blue square, so a listener who hears blue favours the blue square.

Implementation notes

• A context gives each object a value on each dimension, and a word is the pair of a dimension and the value it names, so the lexical entries are one clause and no table of words against objects is given.
• The speaker and the literal listener are the uniform-prior pipeline of RSA/Uniform.lean at the extensions. The paper's speaker has rationality one and costless words, and the findings are stated at every positive rationality.

References

• [FG12]

Contexts and words

inductive FrankGoodman2012.Attribute : Type

The two dimensions on which the objects of a context vary.

• colour : Attribute
• shape : Attribute

@[instance_reducible]

instance FrankGoodman2012.instDecidableEqAttribute : DecidableEq Attribute

Equations

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

@[instance_reducible]

instance FrankGoodman2012.instFintypeAttribute : Fintype Attribute

Equations

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

@[instance_reducible]

instance FrankGoodman2012.instReprAttribute : Repr Attribute

Equations

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

def FrankGoodman2012.instReprAttribute.repr : Attribute → ℕ → Std.Format

Equations

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

@[reducible, inline]

abbrev FrankGoodman2012.Attribute.Value (C S : Type) : Attribute → Type

The values of a dimension, for colours C and shapes S.

Equations

• FrankGoodman2012.Attribute.Value C S FrankGoodman2012.Attribute.colour = C
• FrankGoodman2012.Attribute.Value C S FrankGoodman2012.Attribute.shape = S

@[reducible, inline]

abbrev FrankGoodman2012.Word (C S : Type) : Type

A word is a one-place predicate that names a colour or a shape.

Equations

• FrankGoodman2012.Word C S = ((a : FrankGoodman2012.Attribute) × FrankGoodman2012.Attribute.Value C S a)

@[instance_reducible]

instance FrankGoodman2012.instDecidableEqValue {C S : Type} [DecidableEq C] [DecidableEq S] (a : Attribute) : DecidableEq (Attribute.Value C S a)

Equations

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

@[instance_reducible]

instance FrankGoodman2012.instFintypeValue {C S : Type} [Fintype C] [Fintype S] (a : Attribute) : Fintype (Attribute.Value C S a)

Equations

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

@[instance_reducible]

instance FrankGoodman2012.instMeasurableSpaceWord {C S : Type} : MeasurableSpace (Word C S)

Equations

• FrankGoodman2012.instMeasurableSpaceWord = ⊤

instance FrankGoodman2012.instDiscreteMeasurableSpaceWord {C S : Type} : DiscreteMeasurableSpace (Word C S)

@[instance_reducible]

instance FrankGoodman2012.instDenotesWordForallForallFintypeForallForallForallValueFinset {C S : Type} [DecidableEq C] [DecidableEq S] : Semantics.Denotes (Word C S) ({E : Type} → [Fintype E] → (E → (a : Attribute) → Attribute.Value C S a) → Finset E)

The lexical entries. The extension of a word in a context is the set of objects whose colour or shape is the one the word names, so ⟦blue⟧ᴹ is the set of objects that are blue in M.

Equations

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

@[simp]

theorem FrankGoodman2012.mem_denote {E C S : Type} [DecidableEq C] [DecidableEq S] [Fintype E] (M : E → (a : Attribute) → Attribute.Value C S a) {w : Word C S} {x : E} : x ∈ Semantics.Denotes.denote w M ↔ M x w.fst = w.snd

theorem FrankGoodman2012.filter_mem_denote {E C S : Type} [DecidableEq C] [DecidableEq S] [Fintype E] (M : E → (a : Attribute) → Attribute.Value C S a) [Fintype C] [Fintype S] [DecidableEq E] (r : E) : {w : Word C S | r ∈ Semantics.Denotes.denote w M} = {⟨Attribute.colour, M r Attribute.colour⟩, ⟨Attribute.shape, M r Attribute.shape⟩}

The words true of an object are the one that names its colour and the one that names its shape.

theorem FrankGoodman2012.profile_eq {E C S : Type} [DecidableEq C] [DecidableEq S] [Fintype E] (M : E → (a : Attribute) → Attribute.Value C S a) [Fintype C] [Fintype S] [DecidableEq E] (r : E) : RSA.profile (fun (w : Word C S) => Semantics.Denotes.denote w M) Finset.univ r = {(Semantics.Denotes.denote ⟨Attribute.colour, M r Attribute.colour⟩ M).card, (Semantics.Denotes.denote ⟨Attribute.shape, M r Attribute.shape⟩ M).card}

noncomputable def FrankGoodman2012.literal {E C S : Type} [DecidableEq C] [DecidableEq S] [Fintype E] (M : E → (a : Attribute) → Attribute.Value C S a) [Fintype C] [Fintype S] [MeasurableSpace E] : ProbabilityTheory.Kernel (Word C S) E

On hearing a word, the literal listener conditions the uniform prior on its extension.

Equations

• FrankGoodman2012.literal M = RSA.listener (ProbabilityTheory.uniformOn Set.univ) (RSA.truthful fun (w : FrankGoodman2012.Word C S) => ↑(Semantics.Denotes.denote w M))

noncomputable def FrankGoodman2012.speaker {E C S : Type} [DecidableEq C] [DecidableEq S] [Fintype E] (M : E → (a : Attribute) → Attribute.Value C S a) [Fintype C] [Fintype S] [MeasurableSpace E] [DiscreteMeasurableSpace E] (α : ℝ) : ProbabilityTheory.Kernel E (Word C S)

The speaker at rationality α is S(w | r) ∝ L₀(r | w) ^ α, the paper's second equation at α = 1.

Equations

• FrankGoodman2012.speaker M α = RSA.speaker α 0 (⇑(FrankGoodman2012.literal M)) MeasureTheory.Measure.dirac

noncomputable def FrankGoodman2012.listener {E C S : Type} [DecidableEq C] [DecidableEq S] [Fintype E] (M : E → (a : Attribute) → Attribute.Value C S a) [Fintype C] [Fintype S] [MeasurableSpace E] [DiscreteMeasurableSpace E] (P : MeasureTheory.Measure E) (α : ℝ) : ProbabilityTheory.Kernel (Word C S) E

The listener of the paper's first equation inverts the speaker against a prior, the salience of the objects.

Equations

• FrankGoodman2012.listener M P α = RSA.listener P ⇑(FrankGoodman2012.speaker M α)

instance FrankGoodman2012.instIsFiniteKernelWordLiteral {E C S : Type} [DecidableEq C] [DecidableEq S] [Fintype E] (M : E → (a : Attribute) → Attribute.Value C S a) [Fintype C] [Fintype S] [MeasurableSpace E] : ProbabilityTheory.IsFiniteKernel (literal M)

instance FrankGoodman2012.instIsFiniteKernelWordSpeaker {E C S : Type} [DecidableEq C] [DecidableEq S] [Fintype E] (M : E → (a : Attribute) → Attribute.Value C S a) [Fintype C] [Fintype S] [MeasurableSpace E] [DiscreteMeasurableSpace E] (α : ℝ) : ProbabilityTheory.IsFiniteKernel (speaker M α)

theorem FrankGoodman2012.speaker_real_singleton_eq_zero {E C S : Type} [DecidableEq C] [DecidableEq S] [Fintype E] (M : E → (a : Attribute) → Attribute.Value C S a) [Fintype C] [Fintype S] [MeasurableSpace E] [DiscreteMeasurableSpace E] {α : ℝ} {w : Word C S} {r : E} (hα : 0 < α) (h : r ∉ Semantics.Denotes.denote w M) : ((speaker M α) r).real {w} = 0

The speaker never uses a word for an object it is false of.

theorem FrankGoodman2012.speaker_real_singleton_pos {E C S : Type} [DecidableEq C] [DecidableEq S] [Fintype E] (M : E → (a : Attribute) → Attribute.Value C S a) [Fintype C] [Fintype S] [MeasurableSpace E] [DiscreteMeasurableSpace E] {α : ℝ} {w : Word C S} {r : E} (hα : 0 ≤ α) (h : r ∈ Semantics.Denotes.denote w M) : 0 < ((speaker M α) r).real {w}

The speaker uses every word true of an object with positive probability.

theorem FrankGoodman2012.literal_apply_singleton {E C S : Type} [DecidableEq C] [DecidableEq S] [Fintype E] (M : E → (a : Attribute) → Attribute.Value C S a) [Fintype C] [Fintype S] [MeasurableSpace E] [DiscreteMeasurableSpace E] [DecidableEq E] (w : Word C S) (r : E) : ((literal M) w) {r} = if r ∈ Semantics.Denotes.denote w M then (↑(Semantics.Denotes.denote w M).card)⁻¹ else 0

The literal listener gives an object in the extension of a word the reciprocal of the size of the extension, the paper's |w|.

theorem FrankGoodman2012.size_principle {E C S : Type} [DecidableEq C] [DecidableEq S] [Fintype E] (M : E → (a : Attribute) → Attribute.Value C S a) [Fintype C] [Fintype S] [MeasurableSpace E] [DiscreteMeasurableSpace E] {α : ℝ} {w₁ w₂ : Word C S} {r : E} [DecidableEq E] (hα : 0 < α) (h₁ : r ∈ Semantics.Denotes.denote w₁ M) (h₂ : r ∈ Semantics.Denotes.denote w₂ M) (h : (Semantics.Denotes.denote w₂ M).card < (Semantics.Denotes.denote w₁ M).card) : ((speaker M α) r).real {w₁} < ((speaker M α) r).real {w₂}

By the size principle, of two words true of an object the speaker prefers the one with the smaller extension.

theorem FrankGoodman2012.speaker_real_singleton_lt_iff {E C S : Type} [DecidableEq C] [DecidableEq S] [Fintype E] (M : E → (a : Attribute) → Attribute.Value C S a) [Fintype C] [Fintype S] [MeasurableSpace E] [DiscreteMeasurableSpace E] {α : ℝ} {w : Word C S} {r r' : E} [DecidableEq E] (hα : 0 < α) (h : r ∈ Semantics.Denotes.denote w M) (h' : r' ∈ Semantics.Denotes.denote w M) {b : Attribute} (hb : b ≠ w.fst) : ((speaker M α) r').real {w} < ((speaker M α) r).real {w} ↔ (Semantics.Denotes.denote ⟨b, M r' b⟩ M).card < (Semantics.Denotes.denote ⟨b, M r b⟩ M).card

Of two objects a word is true of, the speaker uses the word more for the one whose other feature more objects share, the object whose alternative word is the less informative.

theorem FrankGoodman2012.listener_real_singleton_lt_iff {E C S : Type} [DecidableEq C] [DecidableEq S] [Fintype E] (M : E → (a : Attribute) → Attribute.Value C S a) [Fintype C] [Fintype S] [MeasurableSpace E] [DiscreteMeasurableSpace E] {α : ℝ} {w : Word C S} {r r' : E} [DecidableEq E] (hα : 0 < α) (P : MeasureTheory.Measure E) [MeasureTheory.IsFiniteMeasure P] (h : r ∈ Semantics.Denotes.denote w M) (h' : r' ∈ Semantics.Denotes.denote w M) (hP : P {r'} = P {r}) (hP0 : P {r} ≠ 0) {b : Attribute} (hb : b ≠ w.fst) : ((listener M P α) w).real {r'} < ((listener M P α) w).real {r} ↔ (Semantics.Denotes.denote ⟨b, M r' b⟩ M).card < (Semantics.Denotes.denote ⟨b, M r b⟩ M).card

A listener with no prior preference between two objects a word is true of infers the one whose other feature more objects share, since for the other object the speaker had a more informative word.

The context of the figure (Figure 1A)

inductive FrankGoodman2012.Colour : Type

The colours.

• blue : Colour
• green : Colour

@[instance_reducible]

instance FrankGoodman2012.instDecidableEqColour : DecidableEq Colour

Equations

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

@[instance_reducible]

instance FrankGoodman2012.instFintypeColour : Fintype Colour

Equations

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

def FrankGoodman2012.instReprColour.repr : Colour → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance FrankGoodman2012.instReprColour : Repr Colour

Equations

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

inductive FrankGoodman2012.Shape : Type

The shapes.

• square : Shape
• circle : Shape

@[instance_reducible]

instance FrankGoodman2012.instDecidableEqShape : DecidableEq Shape

Equations

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

@[instance_reducible]

instance FrankGoodman2012.instFintypeShape : Fintype Shape

Equations

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

def FrankGoodman2012.instReprShape.repr : Shape → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance FrankGoodman2012.instReprShape : Repr Shape

Equations

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

inductive FrankGoodman2012.Object : Type

The three objects of the context, the domain of the model.

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

@[instance_reducible]

instance FrankGoodman2012.instDecidableEqObject : DecidableEq Object

Equations

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

@[instance_reducible]

instance FrankGoodman2012.instFintypeObject : Fintype Object

Equations

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

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

@[instance_reducible]

instance FrankGoodman2012.instInhabitedObject : Inhabited Object

Equations

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

@[instance_reducible]

instance FrankGoodman2012.instMeasurableSpaceObject : MeasurableSpace Object

Equations

• FrankGoodman2012.instMeasurableSpaceObject = ⊤

instance FrankGoodman2012.instDiscreteMeasurableSpaceObject : DiscreteMeasurableSpace Object

def FrankGoodman2012.M : Object → (a : Attribute) → Attribute.Value Colour Shape a

The model M gives each object of its domain its colour and its shape.

Equations

• FrankGoodman2012.M FrankGoodman2012.Object.blueSquare FrankGoodman2012.Attribute.colour = FrankGoodman2012.Colour.blue
• FrankGoodman2012.M FrankGoodman2012.Object.blueSquare FrankGoodman2012.Attribute.shape = FrankGoodman2012.Shape.square
• FrankGoodman2012.M FrankGoodman2012.Object.blueCircle FrankGoodman2012.Attribute.colour = FrankGoodman2012.Colour.blue
• FrankGoodman2012.M FrankGoodman2012.Object.blueCircle FrankGoodman2012.Attribute.shape = FrankGoodman2012.Shape.circle
• FrankGoodman2012.M FrankGoodman2012.Object.greenSquare FrankGoodman2012.Attribute.colour = FrankGoodman2012.Colour.green
• FrankGoodman2012.M FrankGoodman2012.Object.greenSquare FrankGoodman2012.Attribute.shape = FrankGoodman2012.Shape.square

@[reducible, inline]

abbrev FrankGoodman2012.Word.blue : Word Colour Shape

The word blue.

Equations

• FrankGoodman2012.Word.blue = ⟨FrankGoodman2012.Attribute.colour, FrankGoodman2012.Colour.blue⟩

@[reducible, inline]

abbrev FrankGoodman2012.Word.green : Word Colour Shape

The word green.

Equations

• FrankGoodman2012.Word.green = ⟨FrankGoodman2012.Attribute.colour, FrankGoodman2012.Colour.green⟩

@[reducible, inline]

abbrev FrankGoodman2012.Word.square : Word Colour Shape

The word square.

Equations

• FrankGoodman2012.Word.square = ⟨FrankGoodman2012.Attribute.shape, FrankGoodman2012.Shape.square⟩

@[reducible, inline]

abbrev FrankGoodman2012.Word.circle : Word Colour Shape

The word circle.

Equations

• FrankGoodman2012.Word.circle = ⟨FrankGoodman2012.Attribute.shape, FrankGoodman2012.Shape.circle⟩

theorem FrankGoodman2012.prefers_informative {α : ℝ} (hα : 0 < α) : ((speaker M α) Object.blueCircle).real {Word.blue} < ((speaker M α) Object.blueCircle).real {Word.circle}

For the blue circle the speaker prefers circle, which identifies it, to the ambiguous blue.

theorem FrankGoodman2012.narrowing_blue {α : ℝ} (hα : 0 < α) : ((speaker M α) Object.blueCircle).real {Word.blue} < ((speaker M α) Object.blueSquare).real {Word.blue}

Blue is used less for the blue circle, where circle competes, than for the blue square, where the only competitor is as ambiguous.

theorem FrankGoodman2012.narrowing_square {α : ℝ} (hα : 0 < α) : ((speaker M α) Object.greenSquare).real {Word.square} < ((speaker M α) Object.blueSquare).real {Word.square}

Square is likewise used less for the green square, which green identifies.

theorem FrankGoodman2012.listener_narrows_blue {α : ℝ} (hα : 0 < α) : ((listener M MeasureTheory.Measure.count α) Word.blue).real {Object.blueCircle} < ((listener M MeasureTheory.Measure.count α) Word.blue).real {Object.blueSquare}

A listener with a uniform prior who hears blue favours the blue square over the blue circle.

theorem FrankGoodman2012.unique_green {α : ℝ} (hα : 0 < α) : ((speaker M α) Object.blueSquare).real {Word.green} < ((speaker M α) Object.greenSquare).real {Word.green}

Green is never used for the blue square and is used for the green square, so a listener hearing it identifies the green square.

theorem FrankGoodman2012.unique_circle {α : ℝ} (hα : 0 < α) : ((speaker M α) Object.blueSquare).real {Word.circle} < ((speaker M α) Object.blueCircle).real {Word.circle}

Unique reference for circle.

theorem FrankGoodman2012.fully_rational_picks_circle : Filter.Tendsto (fun (α : ℝ) => ((speaker M α) Object.blueCircle).real {Word.circle}) Filter.atTop (nhds 1)

As rationality grows without bound the speaker puts all its mass on circle.