Rohde, Hoek, Keshev and Franke (2022): This better be interesting

This file formalizes the paper's Bayesian conceptualization of a listener's expectations about upcoming content: the probability of a meaning given that a speaker chose to report it combines the prior probability of the situation with the likelihood that a speaker would articulate it, and the two are separable, the likelihood varying with the context of speech. Over the two values of the paper's forced choice, one near the pretest mean and one a standard deviation above it, the posterior on the atypical value given a report exceeds its prior exactly when the atypical situation is the likelier to be reported, prior_lt_posterior_iff, and between two contexts the posterior is larger where the atypical situation is relatively likelier to be reported, posterior_lt_posterior_iff. An informativity speaker who may also stay silent, silence conveying only the prior, derives the direction of the likelihood: because silence is the more attractive the likelier the situation, a report is likelier at the atypical value, S_report_lt, so a report shifts the guess toward the atypical value relative to the prior, prior_lt_posterior, the more so the more available silence is, posterior_lt_of_silence_lt, and not at all when the speaker was asked and silence was not an option, posterior_eq_prior_of_asked.

Implementation notes

The paper gives the conceptualization in prose and its predictions through four forced-choice experiments; the speaker with a null message is the model the paper takes from its precursors, on the substrate's kernel pipeline, and the null message's cost is the parameter the paper's contexts vary; when the speaker is asked, the null message is absent. The experiments' selection rates are not represented.

References

• H. Rohde, J. Hoek, M. Keshev, M. Franke, This better be interesting: a speaker's decision to speak cues listeners to expect informative content (2022)
• L. Bergen, R. Levy, N. D. Goodman, Pragmatic reasoning through semantic inference (2016)

inductive RohdeEtAl2022.Value : Type

The forced choice offers two values, one near the mean of the pretest and one a standard deviation above it.

• typical : Value
• atypical : Value

@[instance_reducible]

instance RohdeEtAl2022.instDecidableEqValue : DecidableEq Value

Equations

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

@[instance_reducible]

instance RohdeEtAl2022.instFintypeValue : Fintype Value

Equations

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

@[instance_reducible]

instance RohdeEtAl2022.instInhabitedValue : Inhabited Value

Equations

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

@[instance_reducible]

instance RohdeEtAl2022.instMeasurableSpaceValue : MeasurableSpace Value

Equations

• RohdeEtAl2022.instMeasurableSpaceValue = ⊤

instance RohdeEtAl2022.instDiscreteMeasurableSpaceValue : DiscreteMeasurableSpace Value

The Bayesian conceptualization

theorem RohdeEtAl2022.prior_lt_posterior_iff (μ : MeasureTheory.Measure Value) [MeasureTheory.IsProbabilityMeasure μ] (report : ProbabilityTheory.Kernel Value Bool) [ProbabilityTheory.IsFiniteKernel report] (hx : (μ.bind ⇑report) {true} ≠ 0) (ht : μ {Value.typical} ≠ 0) (ha : μ {Value.atypical} ≠ 0) : μ.real {Value.atypical} < ((RSA.listener μ ⇑report) true).real {Value.atypical} ↔ (report Value.typical).real {true} < (report Value.atypical).real {true}

In guessing a reported value, the posterior on the atypical value given that the speaker reported exceeds its prior exactly when the atypical situation is the likelier to be reported. The think condition asks for the prior, the announce condition for the posterior.

theorem RohdeEtAl2022.posterior_lt_posterior_iff (μ : MeasureTheory.Measure Value) [MeasureTheory.IsProbabilityMeasure μ] (report₁ report₂ : ProbabilityTheory.Kernel Value Bool) [ProbabilityTheory.IsFiniteKernel report₁] [ProbabilityTheory.IsFiniteKernel report₂] (hx₁ : (μ.bind ⇑report₁) {true} ≠ 0) (hx₂ : (μ.bind ⇑report₂) {true} ≠ 0) (ht : μ {Value.typical} ≠ 0) (ha : μ {Value.atypical} ≠ 0) : ((RSA.listener μ ⇑report₁) true).real {Value.atypical} < ((RSA.listener μ ⇑report₂) true).real {Value.atypical} ↔ (report₁ Value.atypical).real {true} * (report₂ Value.typical).real {true} < (report₂ Value.atypical).real {true} * (report₁ Value.typical).real {true}

The likelihood is separable from the prior and manipulable. Between two contexts, the posterior on the atypical value given a report is larger in the context where the atypical situation is relatively likelier to be reported.

Informativity and the null message

@[reducible, inline]

abbrev RohdeEtAl2022.Utterance : Type

A report of a value, or silence.

Equations

• RohdeEtAl2022.Utterance = Option RohdeEtAl2022.Value

@[instance_reducible]

instance RohdeEtAl2022.instMeasurableSpaceUtterance : MeasurableSpace Utterance

Equations

• RohdeEtAl2022.instMeasurableSpaceUtterance = ⊤

instance RohdeEtAl2022.instDiscreteMeasurableSpaceUtterance : DiscreteMeasurableSpace Utterance

def RohdeEtAl2022.extension : Utterance → Set Value

A report is true of the value it reports; silence is true of both.

Equations

• RohdeEtAl2022.extension (some v) = {v}
• RohdeEtAl2022.extension none = Set.univ

noncomputable def RohdeEtAl2022.L0 (μ : MeasureTheory.Measure Value) : ProbabilityTheory.Kernel Utterance Value

To the literal listener a report conveys its value and silence conveys the prior.

Equations

• RohdeEtAl2022.L0 μ = RSA.listener μ (RSA.truthful RohdeEtAl2022.extension)

theorem RohdeEtAl2022.L0_some_of_ne (μ : MeasureTheory.Measure Value) {v w : Value} (h : v ≠ w) : ((L0 μ) (some v)) {w} = 0

instance RohdeEtAl2022.instIsFiniteKernelUtteranceValueL0 (μ : MeasureTheory.Measure Value) : ProbabilityTheory.IsFiniteKernel (L0 μ)

noncomputable def RohdeEtAl2022.S (μ : MeasureTheory.Measure Value) (α cs cn : ℝ) : ProbabilityTheory.Kernel Value Utterance

The speaker is the informativity speaker over reports, each costing cs, with silence costing cn.

Equations

• RohdeEtAl2022.S μ α cs cn = RSA.speaker α (fun (x : RohdeEtAl2022.Utterance) => Option.elim x cn fun (x : RohdeEtAl2022.Value) => cs) (⇑(RohdeEtAl2022.L0 μ)) MeasureTheory.Measure.dirac

instance RohdeEtAl2022.instIsFiniteKernelValueUtteranceS (μ : MeasureTheory.Measure Value) (α cs cn : ℝ) : ProbabilityTheory.IsFiniteKernel (S μ α cs cn)

noncomputable def RohdeEtAl2022.askedS (μ : MeasureTheory.Measure Value) (α cs : ℝ) : ProbabilityTheory.Kernel Value Value

When asked, the speaker has no silence option and chooses among the reports.

Equations

• RohdeEtAl2022.askedS μ α cs = RSA.speaker α (fun (x : RohdeEtAl2022.Value) => cs) (⇑(RSA.listener μ (RSA.truthful fun (v : RohdeEtAl2022.Value) => {v}))) MeasureTheory.Measure.dirac

instance RohdeEtAl2022.instIsFiniteKernelValueAskedS (μ : MeasureTheory.Measure Value) (α cs : ℝ) : ProbabilityTheory.IsFiniteKernel (askedS μ α cs)

The decision to speak as the observation

noncomputable def RohdeEtAl2022.spoke (μ : MeasureTheory.Measure Value) (α cs cn : ℝ) : ProbabilityTheory.Kernel Value Bool

spoke records the report's form, whether a value was reported or the speaker stayed silent.

Equations

• RohdeEtAl2022.spoke μ α cs cn = (RohdeEtAl2022.S μ α cs cn).map Option.isSome

instance RohdeEtAl2022.instIsFiniteKernelValueBoolSpoke (μ : MeasureTheory.Measure Value) (α cs cn : ℝ) : ProbabilityTheory.IsFiniteKernel (spoke μ α cs cn)

theorem RohdeEtAl2022.spoke_apply_true (μ : MeasureTheory.Measure Value) (α cs cn : ℝ) (hα : 0 < α) (v : Value) : ((spoke μ α cs cn) v) {true} = ((S μ α cs cn) v) {some v}

The probability of speaking at a value is the share of the report of that value, the other report being false there.

theorem RohdeEtAl2022.L0_some_self (μ : MeasureTheory.Measure Value) [MeasureTheory.IsProbabilityMeasure μ] {v : Value} (hv : μ {v} ≠ 0) : ((L0 μ) (some v)) {v} = 1

theorem RohdeEtAl2022.L0_none (μ : MeasureTheory.Measure Value) [MeasureTheory.IsProbabilityMeasure μ] (v : Value) : ((L0 μ) none) {v} = μ {v}

Newsworthiness

theorem RohdeEtAl2022.S_report (μ : MeasureTheory.Measure Value) (α cs cn : ℝ) [MeasureTheory.IsProbabilityMeasure μ] (hα : 0 < α) {v : Value} (hv : μ {v} ≠ 0) : ((S μ α cs cn) v).real {some v} = Real.exp (-(α * cs)) / (Real.exp (-(α * cs)) + Real.exp (-(α * cn)) * (μ {v} ^ α).toReal)

At its value a report competes with silence only, and silence is weighted by the prior of the value.

theorem RohdeEtAl2022.S_report_pos (μ : MeasureTheory.Measure Value) (α cs cn : ℝ) [MeasureTheory.IsProbabilityMeasure μ] (hα : 0 < α) {v : Value} (hv : μ {v} ≠ 0) : 0 < ((S μ α cs cn) v).real {some v}

The share of a report is positive.

theorem RohdeEtAl2022.S_report_lt (μ : MeasureTheory.Measure Value) (α cs cn : ℝ) [MeasureTheory.IsProbabilityMeasure μ] (hα : 0 < α) (ht : μ {Value.typical} ≠ 0) (ha : μ {Value.atypical} ≠ 0) (h : μ {Value.atypical} < μ {Value.typical}) : ((S μ α cs cn) Value.typical).real {some Value.typical} < ((S μ α cs cn) Value.atypical).real {some Value.atypical}

Improbable situations yield likely utterances. The share of a report is greater at the value with the smaller prior, since silence, which conveys the prior, is the more attractive the likelier the value.

theorem RohdeEtAl2022.spoke_apply_true_ne_zero (μ : MeasureTheory.Measure Value) (α cs cn : ℝ) [MeasureTheory.IsProbabilityMeasure μ] (hα : 0 < α) {v : Value} (hv : μ {v} ≠ 0) : ((spoke μ α cs cn) v) {true} ≠ 0

theorem RohdeEtAl2022.prior_lt_posterior (μ : MeasureTheory.Measure Value) (α cs cn : ℝ) [MeasureTheory.IsProbabilityMeasure μ] (hα : 0 < α) (ht : μ {Value.typical} ≠ 0) (ha : μ {Value.atypical} ≠ 0) (h : μ {Value.atypical} < μ {Value.typical}) : μ.real {Value.atypical} < ((RSA.listener μ ⇑(spoke μ α cs cn)) true).real {Value.atypical}

A report shifts the guess toward the atypical value. Given that the speaker spoke, the posterior on the atypical value exceeds the prior that the think condition returns.

theorem RohdeEtAl2022.posterior_eq_prior_of_asked (μ : MeasureTheory.Measure Value) (α cs : ℝ) [MeasureTheory.IsProbabilityMeasure μ] (hα : 0 < α) (ht : μ {Value.typical} ≠ 0) (ha : μ {Value.atypical} ≠ 0) : ((RSA.listener μ ⇑((askedS μ α cs).map fun (x : Value) => true)) true).real {Value.atypical} = μ.real {Value.atypical}

When the speaker was asked, so that silence was not an option, she speaks at every value, and a report carries no information about typicality. The posterior is the prior, as the when-asked and think conditions align.

theorem RohdeEtAl2022.posterior_lt_of_silence_lt (μ : MeasureTheory.Measure Value) (α cs : ℝ) [MeasureTheory.IsProbabilityMeasure μ] (hα : 0 < α) {cn₁ cn₂ : ℝ} (hlt : cn₂ < cn₁) (ht : μ {Value.typical} ≠ 0) (ha : μ {Value.atypical} ≠ 0) (h : μ {Value.atypical} < μ {Value.typical}) : ((RSA.listener μ ⇑(spoke μ α cs cn₁)) true).real {Value.atypical} < ((RSA.listener μ ⇑(spoke μ α cs cn₂)) true).real {Value.atypical}

The likelihood of speech is malleable. The cheaper silence is, the more a report shifts the guess toward the atypical value, as the out-of-the-blue and large-audience conditions increase the emphasis on information exchange.