[And21]: conversation update for RSA

[Luc59] [Sta02] [FG12]

Tell me everything you know (SCiL 2021, 244–253): multi-turn conversation in RSA. The common ground is a probability distribution over worlds substituted for the RSA world prior (Figure 4), updated each turn by convex combination with the pragmatic-listener posterior at a learning rate, with weighted, thresholded, and difference sampling for cooperative observation selection.

Main results

• updateCG_matches_linear_learning: the update rule is [Luc59]'s linear learning rule — multi-turn conversation is iterated learning over distributions.
• lr_one_excludes_false_worlds / graded_update_keeps_false_world: set-intersection update is the lr = 1 degenerate limit; the graded common ground is non-monotonic by design (fn. 7).
• Turn-1 and turn-2 predictions over the MutualFriends worlds (individuals typed by major × location), including turn2_breaks_symmetry: an updated common ground changes what the same utterance conveys.
• toBToMSharedUpdate: Shared := PMF W instantiates BToMModel.sharedUpdate — BToM discourse dynamics with a distributional shared state.

Implementation notes

The Figure-4 chain is exact ℚ≥0, parameterized by common-ground weights: each agent (l0Score/s1Score/l1Score/s2Score) is one PMF.normalizeScores application over the agent below it, the distributions are PMF.ofScores, and every prediction closes by the ofScores comparison family with one kernel certificate.

Distributional common ground

PMF W wraps PMF W: [Sta02]'s context set with graded plausibility summing to one (§3.2), so entropy — Anderson's success criterion — and KL divergence are available on the carrier. toContextSet projects to the positive-mass worlds (PMF.support), PMF.uniformOfFintype is the empty common ground; ofWeights renormalizes non-negative weights (fn. 3). Unlike the classical context set, worlds can regain probability (fn. 7); intersection update survives only at lr = 1.

The common ground as a distribution

Anderson's distributional common ground is a PMF W ([And21] §3.2): graded plausibility summing to one, with PMF.entropy — the success criterion — and PMF.toRealFn (the ℝ-valued masses every RSA consumer reads) already on the carrier. The classical context set is the support.

@[implicit_reducible]

instance Discourse.instHasContextSetPMF {W : Type u_1} : CommonGround.HasContextSet (PMF W) W

A distribution projects to [Sta02]'s context set: the positive-mass worlds.

Equations

• Discourse.instHasContextSetPMF = { toContextSet := fun (p : PMF W) (w : W) => w ∈ p.support }

@[simp]

theorem Discourse.pmf_toContextSet {W : Type u_1} (p : PMF W) (w : W) : CommonGround.HasContextSet.toContextSet p w ↔ 0 < p.toRealFn w

MutualFriends Domain

inductive Anderson2021.MFWorld : Type

Worlds in the MutualFriends domain: four individuals with different feature combinations.

• ina : MFWorld
• katie : MFWorld
• nancy : MFWorld
• sally : MFWorld

@[implicit_reducible]

instance Anderson2021.instDecidableEqMFWorld : DecidableEq MFWorld

Equations

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

def Anderson2021.instReprMFWorld.repr : MFWorld → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Anderson2021.instReprMFWorld.repr Anderson2021.MFWorld.ina prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Anderson2021.MFWorld.ina")).group prec✝

@[implicit_reducible]

instance Anderson2021.instReprMFWorld : Repr MFWorld

Equations

• Anderson2021.instReprMFWorld = { reprPrec := Anderson2021.instReprMFWorld.repr }

@[implicit_reducible]

instance Anderson2021.instInhabitedMFWorld : Inhabited MFWorld

Equations

• Anderson2021.instInhabitedMFWorld = { default := Anderson2021.instInhabitedMFWorld.default }

@[implicit_reducible]

instance Anderson2021.instFintypeMFWorld : Fintype MFWorld

Equations

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

theorem Anderson2021.card_mfworld : Fintype.card MFWorld = 4

inductive Anderson2021.Major : Type

• astronomy : Major
• german : Major

@[implicit_reducible]

instance Anderson2021.instDecidableEqMajor : DecidableEq Major

Equations

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

def Anderson2021.instReprMajor.repr : Major → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Anderson2021.instReprMajor.repr Anderson2021.Major.german prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Anderson2021.Major.german")).group prec✝

@[implicit_reducible]

instance Anderson2021.instReprMajor : Repr Major

Equations

• Anderson2021.instReprMajor = { reprPrec := Anderson2021.instReprMajor.repr }

inductive Anderson2021.Location : Type

• indoors : Location
• outdoors : Location

@[implicit_reducible]

instance Anderson2021.instDecidableEqLocation : DecidableEq Location

Equations

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

def Anderson2021.instReprLocation.repr : Location → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Anderson2021.instReprLocation : Repr Location

Equations

• Anderson2021.instReprLocation = { reprPrec := Anderson2021.instReprLocation.repr }

def Anderson2021.worldMajor : MFWorld → Major

Equations

• Anderson2021.worldMajor Anderson2021.MFWorld.ina = Anderson2021.Major.astronomy
• Anderson2021.worldMajor Anderson2021.MFWorld.katie = Anderson2021.Major.astronomy
• Anderson2021.worldMajor Anderson2021.MFWorld.nancy = Anderson2021.Major.german
• Anderson2021.worldMajor Anderson2021.MFWorld.sally = Anderson2021.Major.german

def Anderson2021.worldLocation : MFWorld → Location

Equations

• Anderson2021.worldLocation Anderson2021.MFWorld.ina = Anderson2021.Location.indoors
• Anderson2021.worldLocation Anderson2021.MFWorld.sally = Anderson2021.Location.indoors
• Anderson2021.worldLocation Anderson2021.MFWorld.katie = Anderson2021.Location.outdoors
• Anderson2021.worldLocation Anderson2021.MFWorld.nancy = Anderson2021.Location.outdoors

inductive Anderson2021.MFUtterance : Type

Utterances available to speakers. Includes a null utterance for passing when the speaker has no confident observation to share.

• studyHumanity : MFUtterance
• studyScience : MFUtterance
• likeIndoors : MFUtterance
• likeOutdoors : MFUtterance
• null : MFUtterance

@[implicit_reducible]

instance Anderson2021.instDecidableEqMFUtterance : DecidableEq MFUtterance

Equations

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

def Anderson2021.instReprMFUtterance.repr : MFUtterance → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Anderson2021.instReprMFUtterance : Repr MFUtterance

Equations

• Anderson2021.instReprMFUtterance = { reprPrec := Anderson2021.instReprMFUtterance.repr }

@[implicit_reducible]

instance Anderson2021.instInhabitedMFUtterance : Inhabited MFUtterance

Equations

• Anderson2021.instInhabitedMFUtterance = { default := Anderson2021.instInhabitedMFUtterance.default }

@[implicit_reducible]

instance Anderson2021.instFintypeMFUtterance : Fintype MFUtterance

Equations

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

def Anderson2021.mfMeaning : MFUtterance → MFWorld → Bool

Truth-conditional semantics for MutualFriends utterances.

Equations

• Anderson2021.mfMeaning Anderson2021.MFUtterance.studyHumanity x✝ = (Anderson2021.worldMajor x✝ == Anderson2021.Major.german)
• Anderson2021.mfMeaning Anderson2021.MFUtterance.studyScience x✝ = (Anderson2021.worldMajor x✝ == Anderson2021.Major.astronomy)
• Anderson2021.mfMeaning Anderson2021.MFUtterance.likeIndoors x✝ = (Anderson2021.worldLocation x✝ == Anderson2021.Location.indoors)
• Anderson2021.mfMeaning Anderson2021.MFUtterance.likeOutdoors x✝ = (Anderson2021.worldLocation x✝ == Anderson2021.Location.outdoors)
• Anderson2021.mfMeaning Anderson2021.MFUtterance.null x✝ = true

theorem Anderson2021.studyHumanity_partition : mfMeaning MFUtterance.studyHumanity MFWorld.nancy = true ∧ mfMeaning MFUtterance.studyHumanity MFWorld.sally = true ∧ mfMeaning MFUtterance.studyHumanity MFWorld.ina = false ∧ mfMeaning MFUtterance.studyHumanity MFWorld.katie = false

Each non-null utterance partitions the world space in half.

Distributional Common Ground (re-exported from substrate)

The PMF substrate above supplies the weights; the conversation-update and RSA content below consume them.

CommonGround Update

noncomputable def Anderson2021.updateCG {W : Type u_1} (cg post : PMF W) (lr : ℝ) (hlr : 0 ≤ lr) (hlr1 : lr ≤ 1) : PMF W

Common-ground update ([And21] §6, Figure 2): the lr-mixture of the current common ground with the pragmatic-listener posterior — PMF.mix at the learning rate.

Equations

• Anderson2021.updateCG cg post lr hlr hlr1 = PMF.mix ⟨lr, hlr⟩ ⋯ cg post

theorem Anderson2021.updateCG_eq {W : Type u_1} (cg post : PMF W) (lr : ℝ) (h0 : 0 ≤ lr) (h1 : lr ≤ 1) (w : W) : (updateCG cg post lr h0 h1).toRealFn w = (1 - lr) * cg.toRealFn w + lr * post.toRealFn w

The update in ℝ: (1 − lr)·CG + lr·posterior, no rescaling needed.

theorem Anderson2021.updateCG_matches_linear_learning {W : Type u_1} (cg post : PMF W) (lr : ℝ) (h0 : 0 ≤ lr) (h1 : lr ≤ 1) (w : W) : (updateCG cg post lr h0 h1).toRealFn w = (1 - lr) * cg.toRealFn w + (1 - (1 - lr)) * post.toRealFn w

Bridge to [Luc59] linear learning: the CommonGround update has the same algebraic form as LinearLearner.update with retention rate 1 - lr and reinforcement target posterior:

CommonGround'(w) = (1 - lr) · CommonGround(w) + lr · posterior(w)     [Anderson]
v'(a)  = α · v(a) + (1 - α) · r(a)                [Luce §4.C]

Setting α = 1 - lr and r = posterior makes the formulas identical. Multi-turn conversation IS iterated learning over distributions.

theorem Anderson2021.updateCG_lr_zero {W : Type u_1} (cg post : PMF W) (w : W) : (updateCG cg post 0 ⋯ ⋯).toRealFn w = cg.toRealFn w

With learning rate 0, the CommonGround is unchanged (full retention).

theorem Anderson2021.updateCG_lr_one {W : Type u_1} (cg post : PMF W) (w : W) : (updateCG cg post 1 ⋯ ⋯).toRealFn w = post.toRealFn w

With learning rate 1, the CommonGround is replaced by the posterior.

Conversation State

structure Anderson2021.ConversationState (W : Type u_1) : Type u_1

The state of a two-participant conversation (Figure 2).

Tracks the common ground (distributional), each participant's private beliefs, and the learning rate for updates. In the shared CommonGround model (§5.1, Figure 4), both participants access the same cg. In the approximate CommonGround model (§5.2, Figure 6), each maintains a separate approximation (not yet formalized).

The distributional CommonGround enters the RSA model at two points (Figure 4): inside the literal listener and as the pragmatic listener's prior. At each turn the chain is rebuilt at the current CommonGround (conversationStep).

• cg : PMF W
• belA : PMF W
• belB : PMF W
• lr : ℝ
• speakerIsA : Bool

noncomputable def Anderson2021.ConversationState.initial {W : Type u_1} [Fintype W] [Nonempty W] (belA belB : PMF W) (lr : ℝ) : ConversationState W

Initial conversation state: uniform CommonGround, specified beliefs, A speaks first.

Equations

• Anderson2021.ConversationState.initial belA belB lr = { cg := PMF.uniformOfFintype W, belA := belA, belB := belB, lr := lr, speakerIsA := true }

Observation Sampling

noncomputable def Anderson2021.weightedSample {W : Type u_1} (bel : PMF W) : W → ℝ

Weighted sampling (§7.1): a world sampled in proportion to the speaker's belief — truthful (zero-probability worlds never sampled) but flip-flop-prone for noncommittal speakers (Figure 12).

Equations

• Anderson2021.weightedSample bel = bel.toRealFn

noncomputable def Anderson2021.thresholdedSample {W : Type u_1} (bel : PMF W) (θ : ℝ) : W → ℝ

Thresholded sampling (§7.1.1): worlds below the confidence threshold are filtered out; with none left the speaker passes with the null utterance and "all updates are skipped" (Figure 13).

Equations

• Anderson2021.thresholdedSample bel θ w = if bel.toRealFn w ≥ θ then bel.toRealFn w else 0

noncomputable def Anderson2021.differenceSample {W : Type u_1} (bel cg : PMF W) : W → ℝ

Difference-based sampling (§7.2.1): worlds weighted by "the largest (positive) difference in probability between the speaker's beliefs and the Common Ground" — the paper's own truncation at zero (its fn. 14: probability reductions are also informative but assertions can't convey them). Non-redundancy as Gricean Quantity.

Equations

• Anderson2021.differenceSample bel cg w = max 0 (bel.toRealFn w - cg.toRealFn w)

theorem Anderson2021.differenceSample_nonneg {W : Type u_1} (bel cg : PMF W) (w : W) : 0 ≤ differenceSample bel cg w

BToM Shared-State Update

noncomputable def Anderson2021.toBToMSharedUpdate {W : Type u_1} {U : Type u_2} [Fintype W] (posteriorFn : U → PMF W) (lr : ℝ) (hlr : 0 ≤ lr) (hlr1 : lr ≤ 1) : PMF W → U → W → PMF W

Linglib bridge (not in the paper): the common-ground update has the type BToMModel.sharedUpdate expects (Shared → Action → World → Shared at Shared := PMF W), instantiating BToM's discourse dynamics with a distributional shared state. The World argument is unused — the update reads the utterance-derived posterior, never the true world.

Equations

• Anderson2021.toBToMSharedUpdate posteriorFn lr hlr hlr1 cg u _w = Anderson2021.updateCG cg (posteriorFn u) lr hlr hlr1

The Figure-5 beliefs

The §5.1.1 scenario — A thinks the person is Nancy, B thinks Katie — is qualitative in the paper; the 3:1 peak (renormalised to ½ there, 1/6 elsewhere) is this file's illustrative instantiation.

noncomputable def Anderson2021.peakedBeliefs (p : MFWorld) : PMF MFWorld

Beliefs peaked on one world: illustrative 3:1 weights, renormalised.

Equations

• Anderson2021.peakedBeliefs p = PMF.ofRealWeightFn (fun (w : Anderson2021.MFWorld) => if w = p then 3 else 1) ⋯ ⋯

noncomputable def Anderson2021.beliefsA : PMF MFWorld

A believes Nancy; B believes Katie (Figure 5).

Equations

• Anderson2021.beliefsA = Anderson2021.peakedBeliefs Anderson2021.MFWorld.nancy

noncomputable def Anderson2021.beliefsB : PMF MFWorld

See beliefsA.

Equations

• Anderson2021.beliefsB = Anderson2021.peakedBeliefs Anderson2021.MFWorld.katie

theorem Anderson2021.peakedBeliefs_weight (p w : MFWorld) : (peakedBeliefs p).toRealFn w = (if w = p then 3 else 1) / 6

theorem Anderson2021.peakedBeliefs_favors (p w : MFWorld) (hw : w ≠ p) : (peakedBeliefs p).toRealFn w < (peakedBeliefs p).toRealFn p

Peaked beliefs favor their peak over every other world.

The Figure-4 model on ℚ≥0 scores

The Figure-4 chain

Shared-CG RSA: L0 ∝ ⟦u⟧·CG, S1 ∝ LitList (α = 1, fn. 3), L1 ∝ PragSpeak·CG, with the endorsement speaker S2 ∝ L1.

The score chain

def Anderson2021.l0Score (cg : MFWorld → ℚ≥0) (u : MFUtterance) : MFWorld → ℚ≥0

CG-weighted literal listener ([And21] Figure 4: L0 ∝ ⟦u⟧·CG).

Equations

• Anderson2021.l0Score cg u = PMF.normalizeScores fun (w : Anderson2021.MFWorld) => if Anderson2021.mfMeaning u w = true then cg w else 0

def Anderson2021.s1Score (cg : MFWorld → ℚ≥0) (w : MFWorld) : MFUtterance → ℚ≥0

Pragmatic speaker ([And21] Figure 4: S1 ∝ LitList; fn. 3: the softmax terms are omitted and probabilities renormalized, i.e. α = 1 and no cost — the speaker weight IS the literal-listener value).

Equations

• Anderson2021.s1Score cg w = PMF.normalizeScores fun (u : Anderson2021.MFUtterance) => Anderson2021.l0Score cg u w

def Anderson2021.l1Score (cg : MFWorld → ℚ≥0) (u : MFUtterance) : MFWorld → ℚ≥0

Pragmatic listener ([And21] Figure 4: L1 ∝ PragSpeak·CG).

Equations

• Anderson2021.l1Score cg u = PMF.normalizeScores fun (w : Anderson2021.MFWorld) => cg w * Anderson2021.s1Score cg w u

def Anderson2021.s2Score (cg : MFWorld → ℚ≥0) (w : MFWorld) : MFUtterance → ℚ≥0

Endorsement speaker: S2(u|w) ∝ L1(w|u) (uniform utterance prior), the standard endorsement inversion of L1 over utterances.

Equations

• Anderson2021.s2Score cg w = PMF.normalizeScores fun (u : Anderson2021.MFUtterance) => Anderson2021.l1Score cg u w

The prior-transparency mechanism

Worlds with the same truth profile get identical speaker columns — the common-ground factor cancels out of S1's normalization (PMF.normalizeScores_mul_left) — so L1 orders them purely by their common-ground weights. Every tie and tie-break below is an instance.

theorem Anderson2021.s1Score_congr (cg : MFWorld → ℚ≥0) {w₁ w₂ : MFWorld} (h₁ : cg w₁ ≠ 0) (h₂ : cg w₂ ≠ 0) (hw : ∀ (u : MFUtterance), mfMeaning u w₁ = mfMeaning u w₂) : s1Score cg w₁ = s1Score cg w₂

Same truth profile, same speaker column: the CG weight scales the whole L0 row and cancels under normalization.

theorem Anderson2021.l1Score_lt_iff (cg : MFWorld → ℚ≥0) {u : MFUtterance} {w₁ w₂ : MFWorld} (h₁ : cg w₁ ≠ 0) (h₂ : cg w₂ ≠ 0) (hw : ∀ (u' : MFUtterance), mfMeaning u' w₁ = mfMeaning u' w₂) (hu : s1Score cg w₁ u ≠ 0) : l1Score cg u w₁ < l1Score cg u w₂ ↔ cg w₁ < cg w₂

L1 orders same-profile worlds by their CG weights alone.

noncomputable def Anderson2021.s1Turn1 : MFWorld → PMF MFUtterance

Turn-1 speaker (uniform CommonGround, [And21] Figure 2: CG = Uniform(worlds)).

Equations

• Anderson2021.s1Turn1 w = PMF.ofScores PMF.Fallback.uniform (Anderson2021.s1Score (fun (x : Anderson2021.MFWorld) => 1) w)

noncomputable def Anderson2021.l1Turn1 : MFUtterance → PMF MFWorld

Turn-1 pragmatic listener.

Equations

• Anderson2021.l1Turn1 u = PMF.ofScores PMF.Fallback.uniform (Anderson2021.l1Score (fun (x : Anderson2021.MFWorld) => 1) u)

noncomputable def Anderson2021.s2Turn1 : MFWorld → PMF MFUtterance

Turn-1 endorsement speaker.

Equations

• Anderson2021.s2Turn1 w = PMF.ofScores PMF.Fallback.uniform (Anderson2021.s2Score (fun (x : Anderson2021.MFWorld) => 1) w)

theorem Anderson2021.s1Turn1_true {u : MFUtterance} {w : MFWorld} (hw : mfMeaning u w = true) (hn : u ≠ MFUtterance.null) : (s1Turn1 w) u = ↑↑(2 / 5)

Turn-1 speaker values ([And21] Figure-4 equations at the uniform CG; derived exact rationals — Figure 5 reports the qualitative profile): 2/5 on each true specific utterance, 1/5 on null, 0 off support.

theorem Anderson2021.s1Turn1_null (w : MFWorld) : (s1Turn1 w) MFUtterance.null = ↑↑(1 / 5)

theorem Anderson2021.s1Turn1_false {u : MFUtterance} {w : MFWorld} (hw : mfMeaning u w = false) : (s1Turn1 w) u = 0

theorem Anderson2021.l1Turn1_true {u : MFUtterance} {w : MFWorld} (hw : mfMeaning u w = true) (hn : u ≠ MFUtterance.null) : (l1Turn1 u) w = ↑↑(1 / 2)

Turn-1 listener values (derived; L1 ∝ PragSpeak·CG, Figure 4): 1/2 on each world satisfying a specific utterance, 1/4 on every world after null, 0 off support.

theorem Anderson2021.l1Turn1_null (w : MFWorld) : (l1Turn1 MFUtterance.null) w = ↑↑(1 / 4)

theorem Anderson2021.l1Turn1_false {u : MFUtterance} {w : MFWorld} (hw : mfMeaning u w = false) : (l1Turn1 u) w = 0

Turn-1 predictions

theorem Anderson2021.s1_turn1_informativity : (s1Turn1 MFWorld.nancy) MFUtterance.studyScience < (s1Turn1 MFWorld.nancy) MFUtterance.studyHumanity ∧ (s1Turn1 MFWorld.nancy) MFUtterance.null < (s1Turn1 MFWorld.nancy) MFUtterance.studyHumanity ∧ (s1Turn1 MFWorld.nancy) MFUtterance.studyHumanity = (s1Turn1 MFWorld.nancy) MFUtterance.likeOutdoors ∧ ¬(s1Turn1 MFWorld.nancy) MFUtterance.null < (s1Turn1 MFWorld.nancy) MFUtterance.studyScience ∧ (s1Turn1 MFWorld.ina) MFUtterance.studyHumanity < (s1Turn1 MFWorld.ina) MFUtterance.studyScience ∧ (s1Turn1 MFWorld.ina) MFUtterance.studyScience = (s1Turn1 MFWorld.ina) MFUtterance.likeIndoors

The turn-1 speaker: true-and-specific beats false or uninformative; equal literal posteriors tie (s1Score_congr at the uniform CG).

theorem Anderson2021.l1_turn1_inferences : (l1Turn1 MFUtterance.studyHumanity) MFWorld.ina < (l1Turn1 MFUtterance.studyHumanity) MFWorld.nancy ∧ (l1Turn1 MFUtterance.likeOutdoors) MFWorld.sally < (l1Turn1 MFUtterance.likeOutdoors) MFWorld.nancy ∧ (l1Turn1 MFUtterance.studyHumanity) MFWorld.nancy = (l1Turn1 MFUtterance.studyHumanity) MFWorld.sally ∧ (l1Turn1 MFUtterance.studyScience) MFWorld.ina = (l1Turn1 MFUtterance.studyScience) MFWorld.katie

The turn-1 listener: utterances favor the worlds they discriminate and tie same-profile worlds at the uniform CG (l1Score_lt_iff).

theorem Anderson2021.l1_null_uniform (w₁ w₂ : MFWorld) : (l1Turn1 MFUtterance.null) w₁ = (l1Turn1 MFUtterance.null) w₂

The null utterance conveys nothing: L1 stays uniform.

Turn 2 (Post-Update Prior)

def Anderson2021.cgTurn2 : MFWorld → ℚ≥0

CommonGround weights after hearing "studyHumanity" at turn 1.

After L1 processes "studyHumanity" with uniform prior, the posterior concentrates on nancy and sally (the German-studying worlds): L1(studyHumanity) = [0, 0, 1/2, 1/2]. Updating the normalized uniform CommonGround [1/4, 1/4, 1/4, 1/4] via updateCG with lr=0.2 (footnote 9) gives:

CommonGround'(w) = 0.8 · 1/4 + 0.2 · L1(w)
CommonGround' = [1/5, 1/5, 3/10, 3/10]

The weights [2, 2, 3, 3] are proportional to [1/5, 1/5, 3/10, 3/10], which is the exact post-update CommonGround from the paper's Figure 5, panel 1A. Since RSA normalizes, proportional weights give identical predictions.

Equations

• Anderson2021.cgTurn2 Anderson2021.MFWorld.ina = 2
• Anderson2021.cgTurn2 Anderson2021.MFWorld.katie = 2
• Anderson2021.cgTurn2 Anderson2021.MFWorld.nancy = 3
• Anderson2021.cgTurn2 Anderson2021.MFWorld.sally = 3

noncomputable def Anderson2021.s1Turn2 : MFWorld → PMF MFUtterance

Turn-2 speaker at the post-update CommonGround.

Equations

• Anderson2021.s1Turn2 w = PMF.ofScores PMF.Fallback.uniform (Anderson2021.s1Score Anderson2021.cgTurn2 w)

noncomputable def Anderson2021.l1Turn2 : MFUtterance → PMF MFWorld

Turn-2 pragmatic listener.

Equations

• Anderson2021.l1Turn2 u = PMF.ofScores PMF.Fallback.uniform (Anderson2021.l1Score Anderson2021.cgTurn2 u)

Turn-2 predictions

theorem Anderson2021.l1_turn2_prior_effects : (l1Turn2 MFUtterance.likeOutdoors) MFWorld.katie < (l1Turn2 MFUtterance.likeOutdoors) MFWorld.nancy ∧ (l1Turn2 MFUtterance.likeIndoors) MFWorld.ina < (l1Turn2 MFUtterance.likeIndoors) MFWorld.sally ∧ (l1Turn2 MFUtterance.studyScience) MFWorld.ina = (l1Turn2 MFUtterance.studyScience) MFWorld.katie ∧ (l1Turn2 MFUtterance.studyHumanity) MFWorld.nancy = (l1Turn2 MFUtterance.studyHumanity) MFWorld.sally

After the "studyHumanity" update, L1 orders same-profile worlds by their new CG weights (l1Score_lt_iff): the outdoor pair breaks toward Nancy, the indoor pair toward Sally, equal-weight pairs stay tied.

theorem Anderson2021.turn2_breaks_symmetry : (l1Turn1 MFUtterance.likeOutdoors) MFWorld.nancy = (l1Turn1 MFUtterance.likeOutdoors) MFWorld.katie ∧ (l1Turn2 MFUtterance.likeOutdoors) MFWorld.katie < (l1Turn2 MFUtterance.likeOutdoors) MFWorld.nancy

The key multi-turn prediction: turn 1 ties Nancy and Katie under "likeOutdoors"; the CG update breaks the tie toward Nancy.

The CG-adapted speaker

theorem Anderson2021.s1_turn2_cg_adapted : (s1Turn2 MFWorld.nancy) MFUtterance.studyHumanity < (s1Turn2 MFWorld.nancy) MFUtterance.likeOutdoors ∧ (s1Turn2 MFWorld.ina) MFUtterance.likeIndoors < (s1Turn2 MFWorld.ina) MFUtterance.studyScience

The CG-weighted L0 makes speakers prefer new over redundant information: after the update, Nancy's speaker switches to "likeOutdoors" (re-asserting "studyHumanity" is redundant at 3:3 weights) and Ina's to "studyScience" (Sally now dominates the indoor partition). At turn 1 both pairs were symmetric (s1_turn1_informativity).

theorem Anderson2021.s2_endorsement : (s2Turn1 MFWorld.nancy) MFUtterance.studyScience < (s2Turn1 MFWorld.nancy) MFUtterance.studyHumanity ∧ (s2Turn1 MFWorld.nancy) MFUtterance.studyHumanity = (s2Turn1 MFWorld.nancy) MFUtterance.likeOutdoors

The endorsement speaker inverts L1: for Nancy, "studyHumanity" beats the false "studyScience" and ties the symmetric "likeOutdoors".

Parametric RSA and Conversation Step

noncomputable def Anderson2021.conversationStep (cg : MFWorld → ℚ≥0) (u : MFUtterance) (lr : ℝ) (hlr : 0 ≤ lr) (hlr1 : lr ≤ 1) : PMF MFWorld

One Figure-2 loop step on the ℚ≥0 face: build the chain at the current common ground, take the L1 posterior, and mix it in at the learning rate. A dead score row — an utterance contradicting the whole common ground — skips the update (§7.1's null behaviour).

Equations

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

theorem Anderson2021.conversationStep_lr_zero (cg : MFWorld → ℚ≥0) (u : MFUtterance) (w : MFWorld) : (conversationStep cg u 0 ⋯ ⋯).toRealFn w = (PMF.ofScores PMF.Fallback.uniform cg).toRealFn w

With lr = 0, the conversation step leaves the CommonGround unchanged.

Qualitative information-sharing properties

theorem Anderson2021.l1_concentrates_after_utterance : (l1Turn1 MFUtterance.null) MFWorld.nancy < (l1Turn1 MFUtterance.studyHumanity) MFWorld.nancy

An informative utterance concentrates L1 above the uniform null baseline (1/2 vs 1/4 on Nancy).

Bridge to Classical CommonGround Update

theorem Anderson2021.lr_one_excludes_false_worlds (cg post : PMF MFWorld) (w : MFWorld) (h : post.toRealFn w = 0) : ¬CommonGround.HasContextSet.toContextSet (updateCG cg post 1 ⋯ ⋯) w

The [Sta02] set-intersection update survives only at the lr = 1 limit: with the prior discarded, a zero-posterior world leaves the context set.

theorem Anderson2021.graded_update_keeps_false_world (cg post : PMF MFWorld) (w : MFWorld) (hcg : 0 < cg.toRealFn w) (lr : ℝ) (h0 : 0 ≤ lr) (h1 : lr < 1) : CommonGround.HasContextSet.toContextSet (updateCG cg post lr h0 ⋯) w

The graded divergence (fn. 7: "worlds can regain probability"): at any lr < 1 the prior keeps a ruled-out world alive with mass (1 − lr)·cg w — the update never deletes a world the prior supports.

Exact Numerical Predictions (turn 1)

Exact turn-1 values

theorem Anderson2021.s1_nancy_studyHumanity_val : (s1Turn1 MFWorld.nancy) MFUtterance.studyHumanity = ↑↑(2 / 5)

theorem Anderson2021.s1_nancy_studyScience_val : (s1Turn1 MFWorld.nancy) MFUtterance.studyScience = 0

theorem Anderson2021.s1_nancy_likeIndoors_val : (s1Turn1 MFWorld.nancy) MFUtterance.likeIndoors = 0

theorem Anderson2021.s1_nancy_likeOutdoors_val : (s1Turn1 MFWorld.nancy) MFUtterance.likeOutdoors = ↑↑(2 / 5)

theorem Anderson2021.s1_nancy_null_val : (s1Turn1 MFWorld.nancy) MFUtterance.null = ↑↑(1 / 5)

theorem Anderson2021.l1_studyHumanity_nancy_val : (l1Turn1 MFUtterance.studyHumanity) MFWorld.nancy = ↑↑(1 / 2)

theorem Anderson2021.l1_studyHumanity_sally_val : (l1Turn1 MFUtterance.studyHumanity) MFWorld.sally = ↑↑(1 / 2)

theorem Anderson2021.l1_studyHumanity_ina_val : (l1Turn1 MFUtterance.studyHumanity) MFWorld.ina = 0

theorem Anderson2021.l1_studyHumanity_katie_val : (l1Turn1 MFUtterance.studyHumanity) MFWorld.katie = 0

theorem Anderson2021.l1_null_val (w : MFWorld) : (l1Turn1 MFUtterance.null) w = ↑↑(1 / 4)

Null gives uniform L1: every world has the same S1(null|w) by the domain's symmetry, so L1(w|null) = CommonGround(w)/Σ CommonGround = 1/4.

Approximate CommonGround Model (§5.2, Figure 6)

Approximate common ground

Separate speaker/listener CG representations (Figure 6): the listener's Pragmatic Listener runs on their own beliefs, so divergence can arise when those differ from the common ground.

structure Anderson2021.ApproxCGState (W : Type u_1) : Type u_1

State for the Approximate CommonGround model (§5.2, Figure 6).

• cgA : PMF W
• cgB : PMF W
• belA : PMF W
• belB : PMF W
• lr : ℝ
• speakerIsA : Bool

noncomputable def Anderson2021.ApproxCGState.initial {W : Type u_1} [Fintype W] [Nonempty W] (belA belB : PMF W) (lr : ℝ) : ApproxCGState W

Equations

• Anderson2021.ApproxCGState.initial belA belB lr = { cgA := PMF.uniformOfFintype W, cgB := PMF.uniformOfFintype W, belA := belA, belB := belB, lr := lr, speakerIsA := true }

noncomputable def Anderson2021.approxL1 (cgL belL : MFWorld → ℚ≥0) (u : MFUtterance) : PMF MFWorld

Approximate comprehension listener ([And21] Figure 6): L0/S1 run over the listener's CommonGround approximation CG_L, but the Bayesian inversion uses the listener's private beliefs B_L as the prior.

Equations

• Anderson2021.approxL1 cgL belL u = PMF.ofScores PMF.Fallback.uniform (PMF.normalizeScores fun (w : Anderson2021.MFWorld) => belL w * Anderson2021.s1Score cgL w u)

theorem Anderson2021.approx_reduces_to_shared (cg : MFWorld → ℚ≥0) (u : MFUtterance) : approxL1 cg cg u = PMF.ofScores PMF.Fallback.uniform (l1Score cg u)

When beliefs equal the CommonGround, the approximate model reduces to the shared CommonGround model — the split is only meaningful when they diverge.

Belief Update Model (§6, Figure 8)

The belief update model extends the conversation system by also updating participants' private beliefs. After comprehension, the listener updates their beliefs via the same linear rule as CommonGround update:

Bel'(w) = (1 - lr_bel) · Bel(w) + lr_bel · posterior(w)

The speaker does not update beliefs (they already knew the info). Different learning rates for CommonGround vs beliefs allow modeling:

• §6.2: skeptical listeners (low belief lr, high CommonGround lr)
• §6.3: uncertainty-based rates (lr scales with entropy)

structure Anderson2021.BeliefUpdateState (W : Type u_1) : Type u_1

State for the belief update model (Figure 8). Extends approximate CommonGround with separate learning rates for CommonGround and beliefs.

• cgA : PMF W
• cgB : PMF W
• belA : PMF W
• belB : PMF W
• cgLR : ℝ

  Learning rate for CommonGround updates.

• belLR : ℝ

  Learning rate for belief updates (may be lower for skeptical agents).

• speakerIsA : Bool

noncomputable def Anderson2021.BeliefUpdateState.initial {W : Type u_1} [Fintype W] [Nonempty W] (belA belB : PMF W) (cgLR belLR : ℝ) : BeliefUpdateState W

Equations

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

theorem Anderson2021.belief_update_is_linear_learning {W : Type u_1} [Fintype W] (bel post : PMF W) (lr : ℝ) (h0 : 0 ≤ lr) (h1 : lr ≤ 1) (w : W) : (updateCG bel post lr h0 h1).toRealFn w = (1 - lr) * bel.toRealFn w + lr * post.toRealFn w

Belief update is algebraically identical to CommonGround update — both are instances of [Luc59]'s linear learning rule. The only difference is the learning rate parameter and the interpretation (private vs shared).

Noncommittal Speaker Problem (§7.1)

A speaker with uniform beliefs (no private information) assigns equal weight to all worlds under weighted sampling. Since no observation is more probable than any other, the speaker makes random assertions about worlds they don't know, causing the CommonGround to flip-flop (Figure 12).

Solutions:

1. Threshold sampling (§7.1.1): filter out low-confidence worlds; a noncommittal speaker passes (null utterance) instead of guessing.
2. Uncertainty-based lr (§6.3): scale the CommonGround update rate by the listener's uncertainty, so confident listeners resist random input.

theorem Anderson2021.uniform_weighted_constant (w₁ w₂ : MFWorld) : weightedSample (PMF.uniformOfFintype MFWorld) w₁ = weightedSample (PMF.uniformOfFintype MFWorld) w₂

Uniform beliefs assign equal weight to all worlds under weighted sampling — a noncommittal speaker has no basis for choosing.

theorem Anderson2021.threshold_filters_uniform (θ : ℝ) (hθ : 1 < θ) (w : MFWorld) : thresholdedSample (PMF.uniformOfFintype MFWorld) θ w = 0

Threshold sampling filters out all worlds when beliefs don't exceed the threshold. Every mass of a distribution is ≤ 1, so any θ > 1 produces zero weight everywhere — the speaker passes (Figure 13).

theorem Anderson2021.threshold_preserves_confident {W : Type u_1} (bel : PMF W) (θ : ℝ) (w : W) (h : bel.toRealFn w ≥ θ) : thresholdedSample bel θ w = bel.toRealFn w

Threshold preserves confident worlds: weights above θ pass through.

Redundancy and Difference Sampling (§7.2)

Under weighted sampling, a speaker whose beliefs match the CommonGround keeps repeating already-shared information (Figure 14). Difference-based sampling fixes this by weighting worlds by max(0, Bel(w) - CommonGround(w)): worlds already established in the CommonGround get zero weight.

Combined with thresholding, thresholded difference-based sampling gives the best behavior (Figure 15): informed speakers contribute new information, noncommittal speakers pass.

theorem Anderson2021.difference_zero_when_aligned {W : Type u_1} (cg : PMF W) (w : W) : differenceSample cg cg w = 0

When beliefs match the CommonGround exactly, difference sampling assigns zero weight to all worlds — nothing new to contribute.

theorem Anderson2021.difference_positive_when_exceeds {W : Type u_1} (bel cg : PMF W) (w : W) (h : cg.toRealFn w < bel.toRealFn w) : 0 < differenceSample bel cg w

Difference sampling assigns positive weight when belief exceeds CommonGround — these worlds carry new information not yet in the common ground.