Anderson (2021): Tell Me Everything You Know

A single RSA turn leaves no trace. Anderson makes the common ground a distribution over worlds, substitutes it for the world prior of every agent in the chain (the literal listener conditions the common ground on the utterance, the pragmatic listener inverts the speaker against it), and after each turn increments it with the pragmatic listener's posterior, discounted by a learning rate. Worlds can then regain probability, since the update is a mixture and not an intersection, which is its limit at learning rate one, and a speaker whose literal listener reads the common ground prefers what is new to what is already established. Observations are sampled from the speaker's private beliefs: by weight, above a confidence threshold (a speaker with nothing to say passes with the null utterance), or by their positive difference from the common ground. On the MutualFriends worlds, they like being outdoors leaves Nancy and Katie tied at the first turn and favours Nancy once they study a humanity is in the common ground.

References

• [And21]
• [FG12]
• [Sta02]

Updating the common ground

noncomputable def Anderson2021.updateCG {W : Type u_1} [MeasurableSpace W] (cg post : MeasureTheory.Measure W) (lr : NNReal) : MeasureTheory.Measure W

The common ground of §6 is incremented by the pragmatic listener's posterior, discounted by the learning rate lr, as the convex mixture of the two.

Equations

• Anderson2021.updateCG cg post lr = (1 - lr) • cg + lr • post

instance Anderson2021.instIsFiniteMeasureUpdateCG {W : Type u_1} [MeasurableSpace W] (cg post : MeasureTheory.Measure W) [MeasureTheory.IsFiniteMeasure cg] [MeasureTheory.IsFiniteMeasure post] (lr : NNReal) : MeasureTheory.IsFiniteMeasure (updateCG cg post lr)

theorem Anderson2021.updateCG_apply {W : Type u_1} [MeasurableSpace W] (cg post : MeasureTheory.Measure W) (lr : NNReal) (s : Set W) : (updateCG cg post lr) s = ↑(1 - lr) * cg s + ↑lr * post s

theorem Anderson2021.updateCG_zero {W : Type u_1} [MeasurableSpace W] (cg post : MeasureTheory.Measure W) : updateCG cg post 0 = cg

theorem Anderson2021.updateCG_one {W : Type u_1} [MeasurableSpace W] (cg post : MeasureTheory.Measure W) : updateCG cg post 1 = post

theorem Anderson2021.notMem_contextSet_updateCG_one {W : Type u_1} [MeasurableSpace W] (cg post : MeasureTheory.Measure W) {w : W} (h : post {w} = 0) : w ∉ HasCommonGround.contextSet (updateCG cg post 1)

At learning rate one the update is Stalnakerian intersection, so a world the posterior rules out leaves the context set.

theorem Anderson2021.mem_contextSet_updateCG {W : Type u_1} [MeasurableSpace W] (cg post : MeasureTheory.Measure W) {lr : NNReal} (hlr : lr < 1) {w : W} (hcg : cg {w} ≠ 0) : w ∈ HasCommonGround.contextSet (updateCG cg post lr)

Below learning rate one the prior keeps every world it supports, so a world the posterior rules out can regain probability (footnote 7).

Selecting observations (§7)

noncomputable def Anderson2021.weightedSample {W : Type u_1} [MeasurableSpace W] (bel : MeasureTheory.Measure W) (w : W) : ℝ

In weighted sampling a world's weight is its probability under the speaker's beliefs.

Equations

• Anderson2021.weightedSample bel w = bel.real {w}

noncomputable def Anderson2021.thresholdedSample {W : Type u_1} [MeasurableSpace W] (bel : MeasureTheory.Measure W) (θ : ℝ) (w : W) : ℝ

Thresholded sampling drops the worlds below the confidence threshold.

Equations

• Anderson2021.thresholdedSample bel θ w = if θ ≤ bel.real {w} then bel.real {w} else 0

noncomputable def Anderson2021.differenceSample {W : Type u_1} [MeasurableSpace W] (bel cg : MeasureTheory.Measure W) (w : W) : ℝ

In difference-based sampling a world's weight is its positive gain over the common ground, since reductions are not assertable (footnote 14).

Equations

• Anderson2021.differenceSample bel cg w = max 0 (bel.real {w} - cg.real {w})

theorem Anderson2021.weightedSample_uniformOn {W : Type u_1} [MeasurableSpace W] [Fintype W] [MeasurableSingletonClass W] (w w' : W) : weightedSample (ProbabilityTheory.uniformOn Set.univ) w = weightedSample (ProbabilityTheory.uniformOn Set.univ) w'

A speaker with uniform beliefs weights every world alike — the noncommittal speaker of Figure 12.

theorem Anderson2021.thresholdedSample_eq_zero {W : Type u_1} [MeasurableSpace W] (bel : MeasureTheory.Measure W) [MeasureTheory.IsProbabilityMeasure bel] {θ : ℝ} (hθ : 1 < θ) (w : W) : thresholdedSample bel θ w = 0

A threshold above one drops every world, and the speaker passes (Figure 13).

theorem Anderson2021.differenceSample_self {W : Type u_1} [MeasurableSpace W] (cg : MeasureTheory.Measure W) (w : W) : differenceSample cg cg w = 0

Beliefs already in the common ground contribute nothing (Figure 14).

theorem Anderson2021.differenceSample_pos {W : Type u_1} [MeasurableSpace W] {bel cg : MeasureTheory.Measure W} {w : W} (h : cg.real {w} < bel.real {w}) : 0 < differenceSample bel cg w

The MutualFriends worlds

inductive Anderson2021.World : Type

The four individuals of Figure 3.

• ina : World
• katie : World
• nancy : World
• sally : World

@[instance_reducible]

instance Anderson2021.instDecidableEqWorld : DecidableEq World

Equations

• Anderson2021.instDecidableEqWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Anderson2021.instFintypeWorld : Fintype World

Equations

• Anderson2021.instFintypeWorld = { elems := { val := ↑Anderson2021.World.enumList, nodup := Anderson2021.World.enumList_nodup }, complete := Anderson2021.instFintypeWorld._proof_1 }

@[instance_reducible]

instance Anderson2021.instMeasurableSpaceWorld : MeasurableSpace World

Equations

• Anderson2021.instMeasurableSpaceWorld = ⊤

instance Anderson2021.instDiscreteMeasurableSpaceWorld : DiscreteMeasurableSpace World

instance Anderson2021.instNonemptyWorld : Nonempty World

inductive Anderson2021.Major : Type

• astronomy : Major
• german : Major

@[instance_reducible]

instance Anderson2021.instDecidableEqMajor : DecidableEq Major

Equations

• Anderson2021.instDecidableEqMajor x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Anderson2021.Location : Type

• indoors : Location
• outdoors : Location

@[instance_reducible]

instance Anderson2021.instDecidableEqLocation : DecidableEq Location

Equations

• Anderson2021.instDecidableEqLocation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Anderson2021.World.major : World → Major

Equations

• Anderson2021.World.ina.major = Anderson2021.Major.astronomy
• Anderson2021.World.katie.major = Anderson2021.Major.astronomy
• Anderson2021.World.nancy.major = Anderson2021.Major.german
• Anderson2021.World.sally.major = Anderson2021.Major.german

def Anderson2021.World.location : World → Location

Equations

• Anderson2021.World.ina.location = Anderson2021.Location.indoors
• Anderson2021.World.sally.location = Anderson2021.Location.indoors
• Anderson2021.World.katie.location = Anderson2021.Location.outdoors
• Anderson2021.World.nancy.location = Anderson2021.Location.outdoors

inductive Anderson2021.Utterance : Type

The utterances of Figure 5, plus the null utterance of §7.1.1.

• studyHumanity : Utterance
• studyScience : Utterance
• likeIndoors : Utterance
• likeOutdoors : Utterance
• null : Utterance

@[instance_reducible]

instance Anderson2021.instDecidableEqUtterance : DecidableEq Utterance

Equations

• Anderson2021.instDecidableEqUtterance x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Anderson2021.instFintypeUtterance : Fintype Utterance

Equations

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

@[instance_reducible]

instance Anderson2021.instMeasurableSpaceUtterance : MeasurableSpace Utterance

Equations

• Anderson2021.instMeasurableSpaceUtterance = ⊤

instance Anderson2021.instDiscreteMeasurableSpaceUtterance : DiscreteMeasurableSpace Utterance

def Anderson2021.Utterance.holds : Utterance → World → Prop

Equations

• Anderson2021.Utterance.studyHumanity.holds x✝ = (x✝.major = Anderson2021.Major.german)
• Anderson2021.Utterance.studyScience.holds x✝ = (x✝.major = Anderson2021.Major.astronomy)
• Anderson2021.Utterance.likeIndoors.holds x✝ = (x✝.location = Anderson2021.Location.indoors)
• Anderson2021.Utterance.likeOutdoors.holds x✝ = (x✝.location = Anderson2021.Location.outdoors)
• Anderson2021.Utterance.null.holds x✝ = True

@[instance_reducible]

instance Anderson2021.instDecidablePredWorldHolds (u : Utterance) : DecidablePred u.holds

Equations

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

def Anderson2021.sem (u : Utterance) : Finset World

The extension of each utterance.

Equations

• Anderson2021.sem u = Finset.filter u.holds Finset.univ

@[reducible, inline]

abbrev Anderson2021.semSet (u : Utterance) : Set World

The extension as a set.

Equations

• Anderson2021.semSet u = ↑(Anderson2021.sem u)

The Figure-4 agents at a common ground

@[reducible, inline]

noncomputable abbrev Anderson2021.L0 (cg : MeasureTheory.Measure World) : ProbabilityTheory.Kernel Utterance World

The literal listener conditions the common ground on the utterance.

Equations

• Anderson2021.L0 cg = RSA.listener cg (RSA.truthful Anderson2021.semSet)

@[reducible, inline]

noncomputable abbrev Anderson2021.S1 (cg : MeasureTheory.Measure World) : ProbabilityTheory.Kernel World Utterance

The pragmatic speaker, without softmax terms or costs (footnote 3).

Equations

• Anderson2021.S1 cg = RSA.speaker 1 0 (⇑(Anderson2021.L0 cg)) MeasureTheory.Measure.dirac

@[reducible, inline]

noncomputable abbrev Anderson2021.L1 (cg : MeasureTheory.Measure World) : ProbabilityTheory.Kernel Utterance World

The pragmatic listener inverts the speaker against the common ground.

Equations

• Anderson2021.L1 cg = RSA.listener cg ⇑(Anderson2021.S1 cg)

noncomputable def Anderson2021.step (cg : MeasureTheory.Measure World) [MeasureTheory.IsFiniteMeasure cg] (u : Utterance) (lr : NNReal) : MeasureTheory.Measure World

In one Figure-2 turn the listener's posterior is mixed into the common ground unless the speaker passed (§7.1.1).

Equations

• Anderson2021.step cg u lr = if u = Anderson2021.Utterance.null then cg else Anderson2021.updateCG cg ((Anderson2021.L1 cg) u) lr

theorem Anderson2021.L1_apply_singleton_eq_zero {cg : MeasureTheory.Measure World} {u : Utterance} {w : World} (hw : w ∉ sem u) : ((L1 cg) u) {w} = 0

A world the utterance rules out gets no listener mass.

theorem Anderson2021.S1_real_singleton {cg : MeasureTheory.Measure World} (w : World) (u : Utterance) : ((S1 cg) w).real {u} = (((L0 cg) u) {w}).toReal / ∑ u' : Utterance, (((L0 cg) u') {w}).toReal

The speaker's real share of an utterance, as a ratio of literal-listener values.

theorem Anderson2021.L0_toReal_of_notMem {cg : MeasureTheory.Measure World} {u : Utterance} {w : World} (hw : w ∉ sem u) : (((L0 cg) u) {w}).toReal = 0

theorem Anderson2021.L0_apply_singleton_ne_zero {cg : MeasureTheory.Measure World} [MeasureTheory.IsFiniteMeasure cg] {u : Utterance} {w : World} (hw : w ∈ sem u) (hcg : cg {w} ≠ 0) : ((L0 cg) u) {w} ≠ 0

theorem Anderson2021.S1_apply_singleton_ne_zero {cg : MeasureTheory.Measure World} [MeasureTheory.IsFiniteMeasure cg] {u : Utterance} {w : World} (hw : w ∈ sem u) (hcg : cg {w} ≠ 0) : ((S1 cg) w) {u} ≠ 0

theorem Anderson2021.L1_apply_singleton_ne_zero {cg : MeasureTheory.Measure World} [MeasureTheory.IsFiniteMeasure cg] {u : Utterance} {w : World} (hw : w ∈ sem u) (hcg : cg {w} ≠ 0) : ((L1 cg) u) {w} ≠ 0

A world the utterance allows, with positive prior mass, keeps positive listener mass.

theorem Anderson2021.L0_toReal {cg : MeasureTheory.Measure World} [MeasureTheory.IsFiniteMeasure cg] {u : Utterance} {w : World} (hw : w ∈ sem u) : (((L0 cg) u) {w}).toReal = cg.real {w} / ∑ x ∈ sem u, cg.real {x}

The first turn

@[reducible, inline]

noncomputable abbrev Anderson2021.cg₁ : MeasureTheory.Measure World

The empty common ground (Figure 2).

Equations

• Anderson2021.cg₁ = ProbabilityTheory.uniformOn Set.univ

theorem Anderson2021.s1_turn1_informativity : ((S1 cg₁) World.nancy).real {Utterance.studyScience} = 0 ∧ ((S1 cg₁) World.nancy).real {Utterance.null} < ((S1 cg₁) World.nancy).real {Utterance.studyHumanity} ∧ ((S1 cg₁) World.nancy).real {Utterance.studyHumanity} = ((S1 cg₁) World.nancy).real {Utterance.likeOutdoors}

The first speaker never produces a false utterance, prefers a specific true utterance to the null one, and ties the two specific true utterances.

theorem Anderson2021.profile_eq (w w' : World) : RSA.profile sem Finset.univ w = RSA.profile sem Finset.univ w'

At the first turn every world has the same profile, two true specific utterances of extension size two and the null utterance.

theorem Anderson2021.l1_turn1_inferences : ((L1 cg₁) Utterance.studyHumanity) {World.ina} = 0 ∧ ((L1 cg₁) Utterance.studyHumanity) {World.nancy} ≠ 0 ∧ ((L1 cg₁) Utterance.likeOutdoors) {World.katie} = ((L1 cg₁) Utterance.likeOutdoors) {World.nancy}

For the first listener, they study a humanity rules out Ina and keeps Nancy, and they like being outdoors leaves Katie and Nancy tied.

theorem Anderson2021.l1_null_uniform (w w' : World) : ((L1 cg₁) Utterance.null) {w} = ((L1 cg₁) Utterance.null) {w'}

The null utterance conveys nothing, and the listener stays uniform.

The second turn

noncomputable def Anderson2021.cg₂ : MeasureTheory.Measure World

The common ground after they study a humanity at learning rate 0.2 (footnote 9).

Equations

• Anderson2021.cg₂ = Anderson2021.updateCG Anderson2021.cg₁ ((Anderson2021.L1 Anderson2021.cg₁) Anderson2021.Utterance.studyHumanity) (1 / 5)

instance Anderson2021.instIsFiniteMeasureWorldCg₂ : MeasureTheory.IsFiniteMeasure cg₂

theorem Anderson2021.cg₂_ina_eq_katie : cg₂ {World.ina} = cg₂ {World.katie}

theorem Anderson2021.cg₂_nancy_eq_sally : cg₂ {World.nancy} = cg₂ {World.sally}

theorem Anderson2021.cg₂_ina_ne_zero : cg₂ {World.ina} ≠ 0

theorem Anderson2021.cg₂_ina_lt_nancy : cg₂ {World.ina} < cg₂ {World.nancy}

Predictions at any common ground favouring the German-studying worlds by a common margin, as cg₂ does.

theorem Anderson2021.sum_L0_toReal (μ : MeasureTheory.Measure World) [MeasureTheory.IsFiniteMeasure μ] (w : World) : ∑ u : Utterance, (((L0 μ) u) {w}).toReal = ∑ u : Utterance with w ∈ sem u, μ.real {w} / ∑ x ∈ sem u, μ.real {x}

theorem Anderson2021.real_univ (μ : MeasureTheory.Measure World) [MeasureTheory.IsFiniteMeasure μ] : μ.real Set.univ = μ.real {World.ina} + μ.real {World.katie} + μ.real {World.nancy} + μ.real {World.sally}

theorem Anderson2021.s1_prefers_new (μ : MeasureTheory.Measure World) [MeasureTheory.IsFiniteMeasure μ] (hik : μ {World.ina} = μ {World.katie}) (hns : μ {World.nancy} = μ {World.sally}) (hlt : μ {World.ina} < μ {World.nancy}) (hi : μ {World.ina} ≠ 0) : ((S1 μ) World.nancy).real {Utterance.studyHumanity} < ((S1 μ) World.nancy).real {Utterance.likeOutdoors} ∧ ((S1 μ) World.ina).real {Utterance.likeIndoors} < ((S1 μ) World.ina).real {Utterance.studyScience}

Nancy's speaker now prefers they like being outdoors to re-asserting they study a humanity, and Ina's they study a science to they like being indoors. This is redundancy aversion, since the literal listener reads the common ground and an established utterance discriminates less.

theorem Anderson2021.l1_katie_lt_nancy (μ : MeasureTheory.Measure World) [MeasureTheory.IsFiniteMeasure μ] (hik : μ {World.ina} = μ {World.katie}) (hns : μ {World.nancy} = μ {World.sally}) (hlt : μ {World.ina} < μ {World.nancy}) (hi : μ {World.ina} ≠ 0) : ((L1 μ) Utterance.likeOutdoors).real {World.katie} < ((L1 μ) Utterance.likeOutdoors).real {World.nancy}

They like being outdoors now favours Nancy over Katie. Nancy's world carries more of the common ground, and Nancy's speaker also produces the utterance more readily, since her other true utterance discriminates less than Katie's.

theorem Anderson2021.turn2_breaks_symmetry : ((L1 cg₁) Utterance.likeOutdoors) {World.katie} = ((L1 cg₁) Utterance.likeOutdoors) {World.nancy} ∧ ((L1 cg₂) Utterance.likeOutdoors).real {World.katie} < ((L1 cg₂) Utterance.likeOutdoors).real {World.nancy}

They like being outdoors tied Katie and Nancy at the first turn, and at the updated common ground it favours Nancy, the key multi-turn prediction.