Sikos, Venhuizen, Drenhaus and Crocker (2021): Reevaluating Pragmatic Reasoning in Language Games

Sikos and colleagues compare Frank and Goodman's rational speech act model with a baseline in one-shot reference games. The baseline keeps the Bayesian listener but replaces the informative speaker by literal meaning alone, a uniform choice among the words true of the referent, so it weighs the objects a word is true of by the prior alone. The two models differ only in the pragmatic conditions, the pairs of a context and a word in which the informative speaker's use of the word varies across the objects it is true of. A pragmatic condition is solvable when the listener then has a single favourite and reducible when it only excludes a competitor.

Main statements

• tendsto_speaker_baselineSpeaker: the baseline speaker is the informative speaker's limit as the rationality goes to zero, the sense in which the baseline is the model at α = 0.
• baselineListener_real_singleton_lt_iff: among the objects a word is true of, the baseline listener follows the prior.
• pragmatic_iff, not_pragmatic_iff: a condition is pragmatic exactly when two objects the word is true of share their other feature with different numbers of objects, and otherwise a listener with a uniform prior is as indifferent as the baseline.
• solvable_blue, solvable_boot, reducible_blue: the conditions of the paper's tables are solvable and reducible at every positive rationality, and not_pragmatic_boot is an ambiguous one.

Implementation notes

• Fit statistics stay in prose. Across three experiments the baseline fit listener choices at least as well as the model overall; the model fit better only for a colour word in pragmatically solvable contexts (Experiments 2 and 3), and in the pragmatically reducible contexts listeners chose the salient competitor, which the model predicts only because the prior reverses its speaker's preference. The theory predicts where the models can differ, not which fits better.
• The model's listener at a prior is FrankGoodman2012.listener, and its preference between two objects compares prior mass times speaker probability (RSA.listener_real_singleton_lt_iff), so a salient competitor wins exactly when its prior advantage exceeds the speaker's ratio.
• The condition types are defined at a uniform prior, as the paper's figure of conditions is.

References

• [SVDC21]
• [FG12]

The baseline

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

The baseline speaker (4) uses literal meaning alone, a uniform choice among the words true of the referent.

Equations

• SikosEtAl2021.baselineSpeaker M = ProbabilityTheory.Kernel.ofWeights fun (r : E) (w : FrankGoodman2012.Word C S) => if r ∈ Semantics.Denotes.denote w M then 1 else 0

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

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

The baseline listener (4) inverts the baseline speaker against the prior.

Equations

• SikosEtAl2021.baselineListener M P = RSA.listener P ⇑(SikosEtAl2021.baselineSpeaker M)

theorem SikosEtAl2021.baselineSpeaker_real_singleton {E C S : Type} [DecidableEq C] [DecidableEq S] [Fintype E] [Fintype C] [Fintype S] [MeasurableSpace E] [DiscreteMeasurableSpace E] (M : E → (a : FrankGoodman2012.Attribute) → FrankGoodman2012.Attribute.Value C S a) [DecidableEq E] (r : E) (w : FrankGoodman2012.Word C S) : ((baselineSpeaker M) r).real {w} = (if r ∈ Semantics.Denotes.denote w M then 1 else 0) / 2

Every object has two true words, so the baseline speaker gives each of them one half.

theorem SikosEtAl2021.tendsto_speaker_baselineSpeaker {E C S : Type} [DecidableEq C] [DecidableEq S] [Fintype E] [Fintype C] [Fintype S] [MeasurableSpace E] [DiscreteMeasurableSpace E] (M : E → (a : FrankGoodman2012.Attribute) → FrankGoodman2012.Attribute.Value C S a) [DecidableEq E] (r : E) (w : FrankGoodman2012.Word C S) : Filter.Tendsto (fun (α : ℝ) => ((FrankGoodman2012.speaker M α) r).real {w}) (nhdsWithin 0 (Set.Ioi 0)) (nhds (((baselineSpeaker M) r).real {w}))

The baseline speaker is the informative speaker's limit as the rationality goes to zero.

theorem SikosEtAl2021.baselineListener_real_singleton_lt_iff {E C S : Type} [DecidableEq C] [DecidableEq S] [Fintype E] [Fintype C] [Fintype S] [MeasurableSpace E] [DiscreteMeasurableSpace E] (M : E → (a : FrankGoodman2012.Attribute) → FrankGoodman2012.Attribute.Value C S a) [DecidableEq E] {w : FrankGoodman2012.Word C S} {r r' : E} (P : MeasureTheory.Measure E) [MeasureTheory.IsFiniteMeasure P] (h : r ∈ Semantics.Denotes.denote w M) (h' : r' ∈ Semantics.Denotes.denote w M) : ((baselineListener M P) w).real {r'} < ((baselineListener M P) w).real {r} ↔ P.real {r'} < P.real {r}

Among the objects a word is true of, the baseline listener follows the prior.

The pragmatic conditions

def SikosEtAl2021.Pragmatic {E C S : Type} [DecidableEq C] [DecidableEq S] [Fintype E] [Fintype C] [Fintype S] [MeasurableSpace E] [DiscreteMeasurableSpace E] (M : E → (a : FrankGoodman2012.Attribute) → FrankGoodman2012.Attribute.Value C S a) (α : ℝ) (w : FrankGoodman2012.Word C S) : Prop

A condition, a word in a context, is pragmatic when a listener with a uniform prior is not indifferent among the objects the word is true of.

Equations

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

def SikosEtAl2021.PragmaticallySolvable {E C S : Type} [DecidableEq C] [DecidableEq S] [Fintype E] [Fintype C] [Fintype S] [MeasurableSpace E] [DiscreteMeasurableSpace E] (M : E → (a : FrankGoodman2012.Attribute) → FrankGoodman2012.Attribute.Value C S a) (α : ℝ) (w : FrankGoodman2012.Word C S) : Prop

A pragmatic condition is solvable when the listener has a single favourite among the objects the word is true of.

Equations

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

def SikosEtAl2021.PragmaticallyReducible {E C S : Type} [DecidableEq C] [DecidableEq S] [Fintype E] [Fintype C] [Fintype S] [MeasurableSpace E] [DiscreteMeasurableSpace E] (M : E → (a : FrankGoodman2012.Attribute) → FrankGoodman2012.Attribute.Value C S a) (α : ℝ) (w : FrankGoodman2012.Word C S) : Prop

A pragmatic condition is reducible when it is not solvable, so that the listener excludes a competitor and stays undecided among the rest.

Equations

• SikosEtAl2021.PragmaticallyReducible M α w = (SikosEtAl2021.Pragmatic M α w ∧ ¬SikosEtAl2021.PragmaticallySolvable M α w)

theorem SikosEtAl2021.not_pragmatic_iff {E C S : Type} [DecidableEq C] [DecidableEq S] [Fintype E] [Fintype C] [Fintype S] [MeasurableSpace E] [DiscreteMeasurableSpace E] (M : E → (a : FrankGoodman2012.Attribute) → FrankGoodman2012.Attribute.Value C S a) {α : ℝ} {w : FrankGoodman2012.Word C S} : ¬Pragmatic M α w ↔ ∀ r ∈ Semantics.Denotes.denote w M, ∀ r' ∈ Semantics.Denotes.denote w M, ((FrankGoodman2012.listener M MeasureTheory.Measure.count α) w).real {r'} = ((FrankGoodman2012.listener M MeasureTheory.Measure.count α) w).real {r}

Outside the pragmatic conditions a listener with a uniform prior is indifferent among the objects the word is true of, as the baseline listener is.

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

A condition is pragmatic exactly when two objects the word is true of share their other feature with different numbers of objects.

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

A condition is pragmatically solvable exactly when it is pragmatic and one object the word is true of shares its other feature with more objects than every other.

The conditions of the tables

inductive SikosEtAl2021.Shape : Type

The shapes of the examples.

• boot : Shape
• mitt : Shape

@[instance_reducible]

instance SikosEtAl2021.instDecidableEqShape : DecidableEq Shape

Equations

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

@[instance_reducible]

instance SikosEtAl2021.instFintypeShape : Fintype Shape

Equations

• SikosEtAl2021.instFintypeShape = { elems := { val := ↑SikosEtAl2021.Shape.enumList, nodup := SikosEtAl2021.Shape.enumList_nodup }, complete := SikosEtAl2021.instFintypeShape._proof_1 }

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

Equations

• SikosEtAl2021.instReprShape.repr SikosEtAl2021.Shape.boot prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "SikosEtAl2021.Shape.boot")).group prec✝
• SikosEtAl2021.instReprShape.repr SikosEtAl2021.Shape.mitt prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "SikosEtAl2021.Shape.mitt")).group prec✝

@[instance_reducible]

instance SikosEtAl2021.instReprShape : Repr Shape

Equations

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

inductive SikosEtAl2021.SolvableObject : Type

The objects of a pragmatically solvable context (Tables 5 and 9).

• referent : SolvableObject
• colourCompetitor : SolvableObject
• shapeCompetitor : SolvableObject

@[instance_reducible]

instance SikosEtAl2021.instDecidableEqSolvableObject : DecidableEq SolvableObject

Equations

• SikosEtAl2021.instDecidableEqSolvableObject x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance SikosEtAl2021.instFintypeSolvableObject : Fintype SolvableObject

Equations

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

def SikosEtAl2021.instReprSolvableObject.repr : SolvableObject → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance SikosEtAl2021.instReprSolvableObject : Repr SolvableObject

Equations

• SikosEtAl2021.instReprSolvableObject = { reprPrec := SikosEtAl2021.instReprSolvableObject.repr }

@[instance_reducible]

instance SikosEtAl2021.instMeasurableSpaceSolvableObject : MeasurableSpace SolvableObject

Equations

• SikosEtAl2021.instMeasurableSpaceSolvableObject = ⊤

instance SikosEtAl2021.instDiscreteMeasurableSpaceSolvableObject : DiscreteMeasurableSpace SolvableObject

def SikosEtAl2021.solvable : SolvableObject → (a : FrankGoodman2012.Attribute) → FrankGoodman2012.Attribute.Value FrankGoodman2012.Colour Shape a

The pragmatically solvable context of Tables 5 and 9 has a blue boot, the pragmatic referent, a blue mitt and a green boot.

Equations

• SikosEtAl2021.solvable SikosEtAl2021.SolvableObject.referent FrankGoodman2012.Attribute.colour = FrankGoodman2012.Colour.blue
• SikosEtAl2021.solvable SikosEtAl2021.SolvableObject.referent FrankGoodman2012.Attribute.shape = SikosEtAl2021.Shape.boot
• SikosEtAl2021.solvable SikosEtAl2021.SolvableObject.colourCompetitor FrankGoodman2012.Attribute.colour = FrankGoodman2012.Colour.blue
• SikosEtAl2021.solvable SikosEtAl2021.SolvableObject.colourCompetitor FrankGoodman2012.Attribute.shape = SikosEtAl2021.Shape.mitt
• SikosEtAl2021.solvable SikosEtAl2021.SolvableObject.shapeCompetitor FrankGoodman2012.Attribute.colour = FrankGoodman2012.Colour.green
• SikosEtAl2021.solvable SikosEtAl2021.SolvableObject.shapeCompetitor FrankGoodman2012.Attribute.shape = SikosEtAl2021.Shape.boot

theorem SikosEtAl2021.solvable_blue {α : ℝ} (hα : 0 < α) : PragmaticallySolvable solvable α ⟨FrankGoodman2012.Attribute.colour, FrankGoodman2012.Colour.blue⟩

On hearing blue the listener singles out the blue boot, since for the blue mitt the speaker had the more informative mitt.

theorem SikosEtAl2021.solvable_boot {α : ℝ} (hα : 0 < α) : PragmaticallySolvable solvable α ⟨FrankGoodman2012.Attribute.shape, Shape.boot⟩

On hearing boot the listener singles out the blue boot as well.

inductive SikosEtAl2021.ReducibleObject : Type

The objects of a pragmatically reducible context (Tables 4 and 8).

• referent₁ : ReducibleObject
• referent₂ : ReducibleObject
• competitor : ReducibleObject

@[instance_reducible]

instance SikosEtAl2021.instDecidableEqReducibleObject : DecidableEq ReducibleObject

Equations

• SikosEtAl2021.instDecidableEqReducibleObject x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance SikosEtAl2021.instFintypeReducibleObject : Fintype ReducibleObject

Equations

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

@[instance_reducible]

instance SikosEtAl2021.instReprReducibleObject : Repr ReducibleObject

Equations

• SikosEtAl2021.instReprReducibleObject = { reprPrec := SikosEtAl2021.instReprReducibleObject.repr }

def SikosEtAl2021.instReprReducibleObject.repr : ReducibleObject → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance SikosEtAl2021.instMeasurableSpaceReducibleObject : MeasurableSpace ReducibleObject

Equations

• SikosEtAl2021.instMeasurableSpaceReducibleObject = ⊤

instance SikosEtAl2021.instDiscreteMeasurableSpaceReducibleObject : DiscreteMeasurableSpace ReducibleObject

def SikosEtAl2021.reducible : ReducibleObject → (a : FrankGoodman2012.Attribute) → FrankGoodman2012.Attribute.Value FrankGoodman2012.Colour Shape a

The pragmatically reducible context of Tables 4 and 8 has two blue boots, the pragmatic referents, and a blue mitt.

Equations

• SikosEtAl2021.reducible SikosEtAl2021.ReducibleObject.referent₁ FrankGoodman2012.Attribute.colour = FrankGoodman2012.Colour.blue
• SikosEtAl2021.reducible SikosEtAl2021.ReducibleObject.referent₁ FrankGoodman2012.Attribute.shape = SikosEtAl2021.Shape.boot
• SikosEtAl2021.reducible SikosEtAl2021.ReducibleObject.referent₂ FrankGoodman2012.Attribute.colour = FrankGoodman2012.Colour.blue
• SikosEtAl2021.reducible SikosEtAl2021.ReducibleObject.referent₂ FrankGoodman2012.Attribute.shape = SikosEtAl2021.Shape.boot
• SikosEtAl2021.reducible SikosEtAl2021.ReducibleObject.competitor FrankGoodman2012.Attribute.colour = FrankGoodman2012.Colour.blue
• SikosEtAl2021.reducible SikosEtAl2021.ReducibleObject.competitor FrankGoodman2012.Attribute.shape = SikosEtAl2021.Shape.mitt

theorem SikosEtAl2021.reducible_blue {α : ℝ} (hα : 0 < α) : PragmaticallyReducible reducible α ⟨FrankGoodman2012.Attribute.colour, FrankGoodman2012.Colour.blue⟩

On hearing blue the listener excludes the blue mitt and stays undecided between the two boots.

theorem SikosEtAl2021.not_pragmatic_boot {α : ℝ} (hα : 0 < α) : ¬Pragmatic reducible α ⟨FrankGoodman2012.Attribute.shape, Shape.boot⟩

On hearing boot the listener is indifferent between the two boots, an ambiguous condition in which the model and the baseline agree.