[RHKF22]: A speaker's decision to speak cues informative content

Rohde, Hoek, Keshev & Franke (2022) argue that comprehenders separate the prior probability of a situation from the likelihood a speaker would choose to describe it: atypical (newsworthy) situations, precisely because their low prior probability makes them mention-worthy, yield likely utterances. This file formalises that Bayesian conceptualisation as a silence-augmented [BLG16]-style speaker: a two-value world (near-mean typical vs. newsworthy atypical), a WithSilence-lifted utterance space, and derived closed forms for the speaker's decision to report vs. stay silent. Exp 1 varies thinks that vs. announced that completion contexts; Exps 2–4 (out-of-the-blue and large-audience conditions) further strengthen the effect.

Main definitions

• Value — the two-outcome value space (typical vs. atypical).
• Utterance — WithSilence Value; none is silence, some v reports v.
• L0 — literal listener: silence returns the prior, some v returns PMF.pure v.
• speaker — rationality-1 S1Belief with κs-weighted content and κn-weighted silence.

Main theorems

• speaker_apply_none, speaker_apply_some_self — closed forms.
• newsworthy_speech, newsworthy_silence — atypical situations yield likelier self-reports; typical situations yield likelier silence.
• announce_shifts_toward_atypical — cross-multiplied odds form of the Exp 1 announce-vs-think shift.
• speech_preferred_of_cheap — when speech is no more expensive than silence and the world is not a priori certain, reporting dominates.

Situations and utterances

inductive RohdeEtAl2022.Value : Type

A situation value: typical (near-mean, a priori likely) vs. atypical (newsworthy, a priori unlikely).

• typical : Value
• atypical : Value

@[implicit_reducible]

instance RohdeEtAl2022.instDecidableEqValue : DecidableEq Value

Equations

• RohdeEtAl2022.instDecidableEqValue x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance RohdeEtAl2022.instReprValue : Repr Value

Equations

• RohdeEtAl2022.instReprValue = { reprPrec := RohdeEtAl2022.instReprValue.repr }

def RohdeEtAl2022.instReprValue.repr : Value → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance RohdeEtAl2022.instInhabitedValue : Inhabited Value

Equations

• RohdeEtAl2022.instInhabitedValue = { default := RohdeEtAl2022.instInhabitedValue.default }

@[implicit_reducible]

instance RohdeEtAl2022.instFintypeValue : Fintype Value

Equations

• RohdeEtAl2022.instFintypeValue = { elems := { val := ↑RohdeEtAl2022.Value.enumList, nodup := RohdeEtAl2022.Value.enumList_nodup }, complete := RohdeEtAl2022.instFintypeValue._proof_1 }

@[reducible, inline]

abbrev RohdeEtAl2022.Utterance : Type

Utterance space: none is silence; some v is a report of value v.

Equations

• RohdeEtAl2022.Utterance = RSA.WithSilence RohdeEtAl2022.Value

Model

Literal listener L0: silence conveys nothing, so the listener falls back on the prior; a report some v picks out v via PMF.pure. Cost factor: silence carries weight κn, content utterances carry weight κs.

noncomputable def RohdeEtAl2022.L0 (p : PMF Value) : Utterance → PMF Value

Literal listener. Silence returns the prior.

Equations

• RohdeEtAl2022.L0 p (some v) = PMF.pure v
• RohdeEtAl2022.L0 p none = p

noncomputable def RohdeEtAl2022.cost (κs κn : ENNReal) : Utterance → ENNReal

Cost factor: κn on silence, κs on every content utterance.

Equations

• RohdeEtAl2022.cost κs κn = RSA.liftCostFactor κn fun (x : RohdeEtAl2022.Value) => κs

Partition function

noncomputable def RohdeEtAl2022.Z (p : PMF Value) (κs κn : ENNReal) (w : Value) : ENNReal

Score sum ∑' u, L0(w|u)^1 · cost u. Collapses to κs + p w · κn.

Equations

• RohdeEtAl2022.Z p κs κn w = ∑' (u : RohdeEtAl2022.Utterance), (RohdeEtAl2022.L0 p u) w ^ 1 * RohdeEtAl2022.cost κs κn u

theorem RohdeEtAl2022.Z_eq (p : PMF Value) (κs κn : ENNReal) (w : Value) : Z p κs κn w = κs + p w * κn

Partition closed form: the value-report matching w scores κs, silence scores p w · κn, and the other value-report scores 0.

Speaker

noncomputable def RohdeEtAl2022.speaker (p : PMF Value) (κs κn : ENNReal) (hκs : κs ≠ 0) (hκsT : κs ≠ ⊤) (hκnT : κn ≠ ⊤) (w : Value) : PMF Utterance

Speaker at world w, rationality 1.

Equations

• RohdeEtAl2022.speaker p κs κn hκs hκsT hκnT w = RSA.S1Belief (RohdeEtAl2022.L0 p) (RohdeEtAl2022.cost κs κn) 1 w ⋯ ⋯

Closed forms

Numerator κs for some w (self-report), p w · κn for none (silence), over the shared partition κs + p w · κn.

theorem RohdeEtAl2022.speaker_apply_none (p : PMF Value) (κs κn : ENNReal) (hκs : κs ≠ 0) (hκsT : κs ≠ ⊤) (hκnT : κn ≠ ⊤) (w : Value) : (speaker p κs κn hκs hκsT hκnT w) none = p w * κn * (κs + p w * κn)⁻¹

Silence probability.

theorem RohdeEtAl2022.speaker_apply_some_self (p : PMF Value) (κs κn : ENNReal) (hκs : κs ≠ 0) (hκsT : κs ≠ ⊤) (hκnT : κn ≠ ⊤) (w : Value) : (speaker p κs κn hκs hκsT hκnT w) (some w) = κs * (κs + p w * κn)⁻¹

Self-report probability.

Newsworthiness

When the atypical value has lower prior mass, the softmax speaker prefers reporting atypical in the atypical world and staying silent in the typical world: "improbable situations yield likely utterances".

theorem RohdeEtAl2022.newsworthy_speech (p : PMF Value) (κs κn : ENNReal) (hκs : κs ≠ 0) (hκsT : κs ≠ ⊤) (hκn : κn ≠ 0) (hκnT : κn ≠ ⊤) (h : p Value.atypical < p Value.typical) : (speaker p κs κn hκs hκsT hκnT Value.typical) (some Value.typical) < (speaker p κs κn hκs hκsT hκnT Value.atypical) (some Value.atypical)

Speech is likelier in the atypical situation than in the typical one.

theorem RohdeEtAl2022.newsworthy_silence (p : PMF Value) (κs κn : ENNReal) (hκs : κs ≠ 0) (hκsT : κs ≠ ⊤) (hκn : κn ≠ 0) (hκnT : κn ≠ ⊤) (h : p Value.atypical < p Value.typical) : (speaker p κs κn hκs hκsT hκnT Value.atypical) none < (speaker p κs κn hκs hκsT hκnT Value.typical) none

Silence is likelier in the typical situation than in the atypical one.

Announce-condition shift (Exp 1)

The paper's key Exp 1 contrast is announced that ... (speech) vs. thinks that ... (bare prior). Conditioning on the speaker having spoken shifts the posterior odds toward atypical: with p atypical > 0, the cross-multiplied form below says the atypical-weighted announce likelihood outweighs the typical-weighted one. See [BLG16] for the null-utterance framework this specialises.

theorem RohdeEtAl2022.announce_shifts_toward_atypical (p : PMF Value) (κs κn : ENNReal) (hκs : κs ≠ 0) (hκsT : κs ≠ ⊤) (hκn : κn ≠ 0) (hκnT : κn ≠ ⊤) (h : p Value.atypical < p Value.typical) (hpa : p Value.atypical ≠ 0) : p Value.typical * (speaker p κs κn hκs hκsT hκnT Value.typical) (some Value.typical) * p Value.atypical < p Value.atypical * (speaker p κs κn hκs hκsT hκnT Value.atypical) (some Value.atypical) * p Value.typical

The announced that ... condition shifts posterior odds toward the newsworthy value: cross-multiplied form.

Regime toggle: cheap speech dominates silence

When the speech cost weight is no less than silence's (κn ≤ κs, i.e., a report is no more expensive than staying silent) and the world is not a priori certain (p w < 1), the speaker at w prefers reporting w to silence. Recovers the [BLG16] regime where silence is a never-preferred honesty fallback.

theorem RohdeEtAl2022.speech_preferred_of_cheap (p : PMF Value) (κs κn : ENNReal) (hκs : κs ≠ 0) (hκsT : κs ≠ ⊤) (hκn : κn ≠ 0) (hκnT : κn ≠ ⊤) (hcost : κn ≤ κs) (w : Value) (hpw : p w < 1) : (speaker p κs κn hκs hκsT hκnT w) none < (speaker p κs κn hκs hκsT hκnT w) (some w)

Speech dominates silence when it is no more expensive and the world is not a priori certain.