Égré, Spector, Mortier and Verheyen (2023): On the Optimality of Vagueness: "Around", "Between" and the Gricean Maxims

Égré, Spector, Mortier and Verheyen give a Bayesian account of the approximator "around n" and of why a partially informed speaker may prefer it to a precise "between a and b". "Around n" has an open radius: "x is around n" at radius y means |n − x| ≤ y. The listener's information state is a joint distribution over the value and the radius, and accepting the sentence conditions it on that event and marginalizes the radius (bir). The speaker chooses the message whose literal posterior is closest to her belief in Kullback–Leibler divergence, and the full model iterates speakers and joint listeners from the literal listener (listener). Appendix A treats the lexical uncertainty model of Bergen, Levy and Goodman (luSpeaker), and Appendix B a weighted interpretation rule (wir).

Main statements

• bir_eq_ofDensity, bir_unif_apply_singleton, ratio_inequality: the interpretation rule is the literal listener at the graded meaning "the prior mass of the radii reaching x", under uniform priors its posterior is the triangle (n − |n − k| + 1) / (n + 1)², and whatever the priors it raises the odds of a closer value against a farther one, where "between" leaves them unchanged.
• table1_prefers_around: with a belief peaked at 4 with support [1, 7] the speaker prefers "around 4" to "between 1 and 7".
• luSpeaker_eq_of_sameSupport: in the lexical uncertainty model, beliefs with the same support yield the same speaker at every level.
• bir_eq_bind_radiusPosterior, wir_ne_bir: the Bayesian rule is the weighted rule with the posterior over radii in place of the prior, and the two rules differ.

Implementation notes

• Values are a countable measurable type with a distance d : X → ℕ to the target, so one development serves the scale ℕ of §3–4, where the message "around n" is Nat.dist n, and the nine values of §5–7. Priors are finite measures rather than probability measures: every stage renormalizes, so the uniform priors of §3.2.2 are the counting measures unif and the uniform prior on the nine values is Measure.count.
• Speakers are RSA.speaker at a belief, which for probability beliefs is the softmax of −λ · D(belief ‖ listener) (RSA.speaker_eq_softmax_klDiv). A message that excludes a value the speaker deems possible has zero probability, footnote 17's Quality. In the full model the belief is the joint prior conditioned on the observation and marginalized to the value; in the lexical uncertainty model, whose speaker addresses the listener's joint state, it is that conditioned prior itself.
• Pragmatic listeners are RSA.listener at the joint prior of the speaker read at the observation. A message no observation produces gets the zero measure, the 0 / 0 convention of footnote 28, and on messages heard with positive probability the listener is the posterior kernel (RSA.listener_apply_eq_posterior).
• The lexical uncertainty model is stated over arbitrary finite types of worlds, observations, interpretations and messages. Appendix A's two steps are general: RSA.speaker_cond_listener_truthful_apply_eq, that against a literal listener the speaker depends on what she knows only through the messages it entails, and RSA.speaker_cond_ofDensity_apply_eq, that the prior cancels against a reweighted prior.

TODO

• The amplification across recursion levels reported in Tables 7–10 (a level-5 speaker preferring "around 4" for the peaked belief on [2, 6], which the level-1 speaker does not) is a numerical simulation at λ = 10 and is not represented.

References

• [ESMV23]
• [BLG16]
• [LG17]
• [GS13]

The semantics of "around" and the Bayesian interpretation rule (§3.2)

def EgreEtAl2023.AroundEvent {X : Type u_1} (d : X → ℕ) : Set (X × ℕ)

"x is around n" at radius y is |n − x| ≤ y (5), as an event over the joint state of value and radius; d is the distance to the target.

Equations

• EgreEtAl2023.AroundEvent d = {p : X × ℕ | d p.1 ≤ p.2}

noncomputable def EgreEtAl2023.aroundWeight {X : Type u_1} (ν : MeasureTheory.Measure ℕ) (d : X → ℕ) (x : X) : ENNReal

The graded meaning of "around" is the prior mass of the radii reaching the value.

Equations

• EgreEtAl2023.aroundWeight ν d x = ν (Set.Ici (d x))

theorem EgreEtAl2023.aroundWeight_le_of_le {X : Type u_1} (ν : MeasureTheory.Measure ℕ) (d : X → ℕ) {x x' : X} (h : d x ≤ d x') : aroundWeight ν d x' ≤ aroundWeight ν d x

The closer a value is to the target, the likelier "around" is true of it (§3.2.1).

noncomputable def EgreEtAl2023.bir {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure ℕ) (d : X → ℕ) : MeasureTheory.Measure X

The Bayesian interpretation rule (§3.2.1) conditions the joint prior over value and radius on the value being around the target and marginalizes to the value.

Equations

• EgreEtAl2023.bir μ ν d = MeasureTheory.Measure.map Prod.fst (μ.prod ν)[|EgreEtAl2023.AroundEvent d]

theorem EgreEtAl2023.measurableSet_aroundEvent {X : Type u_1} [MeasurableSpace X] [Countable X] [MeasurableSingletonClass X] (d : X → ℕ) : MeasurableSet (AroundEvent d)

theorem EgreEtAl2023.prod_apply_aroundEvent {X : Type u_1} [MeasurableSpace X] [Countable X] [MeasurableSingletonClass X] (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure ℕ) (d : X → ℕ) [MeasureTheory.SFinite ν] : (μ.prod ν) (AroundEvent d) = ∫⁻ (x : X), aroundWeight ν d x ∂μ

theorem EgreEtAl2023.bir_apply_singleton {X : Type u_1} [MeasurableSpace X] [Countable X] [MeasurableSingletonClass X] (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure ℕ) (d : X → ℕ) [MeasureTheory.SFinite ν] (x : X) : (bir μ ν d) {x} = μ {x} * aroundWeight ν d x / ∫⁻ (x' : X), aroundWeight ν d x' ∂μ

theorem EgreEtAl2023.bir_eq_ofDensity {X : Type u_1} [MeasurableSpace X] [Countable X] [MeasurableSingletonClass X] (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure ℕ) (d : X → ℕ) [MeasureTheory.SFinite ν] {U : Type u_2} [MeasurableSpace U] [Countable U] [MeasurableSingletonClass U] {m : U → X → ENNReal} {u : U} (hm : m u = aroundWeight ν d) : bir μ ν d = (ProbabilityTheory.Kernel.ofDensity μ m) u

By eq. (BIR), the information state after "around" is the literal listener at the graded meaning, P(x = k | around n) ∝ P(x = k) · P(y ≥ |n − k|).

Uniform priors and the triangular posterior (§3.2.2)

noncomputable def EgreEtAl2023.unif (N : ℕ) : MeasureTheory.Measure ℕ

The counting measure on {0, …, N} is the uniform prior on the range up to the normalizing constant, which conditioning absorbs.

Equations

• EgreEtAl2023.unif N = ∑ k ∈ Finset.range (N + 1), MeasureTheory.Measure.dirac k

theorem EgreEtAl2023.unif_apply_singleton (N k : ℕ) : (unif N) {k} = if k ≤ N then 1 else 0

theorem EgreEtAl2023.unif_apply_Ici (N d : ℕ) : (unif N) (Set.Ici d) = ↑(N + 1 - d)

theorem EgreEtAl2023.unif_apply_Icc {N a b : ℕ} (hb : b ≤ N) : (unif N) (Set.Icc a b) = ↑(b + 1 - a)

theorem EgreEtAl2023.lintegral_unif (N : ℕ) (f : ℕ → ENNReal) : ∫⁻ (k : ℕ), f k ∂unif N = ∑ k ∈ Finset.range (N + 1), f k

theorem EgreEtAl2023.aroundWeight_unif (n k : ℕ) : aroundWeight (unif n) n.dist k = ↑(n + 1 - n.dist k)

theorem EgreEtAl2023.sum_range_sub_dist (n : ℕ) : ∑ k ∈ Finset.range (2 * n + 1), (n + 1 - n.dist k) = (n + 1) ^ 2

The triangle normalizes as ∑_{k ≤ 2n} (n + 1 − |n − k|) = (n + 1)².

theorem EgreEtAl2023.bir_unif_apply_singleton (n k : ℕ) : (bir (unif (2 * n)) (unif n) n.dist) {k} = ↑(n + 1 - n.dist k) / ↑(n + 1) ^ 2

Under uniform priors on the values [0, 2n] and on the radii [0, n] the posterior is triangular (§3.2.2), P(x = k | around n) = (n − |n − k| + 1) / (n + 1)².

theorem EgreEtAl2023.bir_unif_symm {n j : ℕ} (h : j ≤ n) : (bir (unif (2 * n)) (unif n) n.dist) {n + j} = (bir (unif (2 * n)) (unif n) n.dist) {n - j}

The posterior is symmetric about the target (§3.2.2 (i)).

theorem EgreEtAl2023.bir_unif_antitone {n k k' : ℕ} (h : n.dist k ≤ n.dist k') : (bir (unif (2 * n)) (unif n) n.dist) {k'} ≤ (bir (unif (2 * n)) (unif n) n.dist) {k}

The farther a value from the target, the less probable it has become (§3.2.2 (i)).

noncomputable def EgreEtAl2023.betweenMeaning (p : ℕ × ℕ) : ℕ → ENNReal

"Between a and b", the crisp interval meaning (§3.1), as a message indexed by its endpoints.

Equations

• EgreEtAl2023.betweenMeaning p = (Set.Icc p.1 p.2).indicator 1

theorem EgreEtAl2023.ofDensity_betweenMeaning (μ : MeasureTheory.Measure ℕ) : ProbabilityTheory.Kernel.ofDensity μ betweenMeaning = RSA.listener μ (RSA.truthful fun (p : ℕ × ℕ) => Set.Icc p.1 p.2)

"Between" is crisp, so its graded literal listener conditions on the interval.

theorem EgreEtAl2023.listener_truthful_unif_betweenMeaning {N a b : ℕ} (hb : b ≤ N) (k : ℕ) : ((ProbabilityTheory.Kernel.ofDensity (unif N) betweenMeaning) (a, b)) {k} = if k ∈ Set.Icc a b then (↑(b + 1 - a))⁻¹ else 0

Under a uniform prior "between" gives the step function uniform on its interval and zero outside it (§3.2.2 (ii)).

The ratio inequality (§4)

theorem EgreEtAl2023.lintegral_aroundWeight_ne_top {μ : MeasureTheory.Measure ℕ} [MeasureTheory.IsFiniteMeasure μ] {ν : MeasureTheory.Measure ℕ} [MeasureTheory.IsFiniteMeasure ν] {n : ℕ} : ∫⁻ (x : ℕ), aroundWeight ν n.dist x ∂μ ≠ ⊤

theorem EgreEtAl2023.ratio_inequality {μ : MeasureTheory.Measure ℕ} [MeasureTheory.IsFiniteMeasure μ] {ν : MeasureTheory.Measure ℕ} [MeasureTheory.IsFiniteMeasure ν] {n k₁ k₂ : ℕ} (h : k₁ < k₂) (hk : k₂ ≤ n) (hμ₁ : μ {n - k₁} ≠ 0) (hμ₂ : μ {n - k₂} ≠ 0) (hν : ν (Set.Ico k₁ k₂) ≠ 0) (hν₂ : ν (Set.Ici k₂) ≠ 0) : μ.real {n - k₁} / μ.real {n - k₂} < (bir μ ν n.dist).real {n - k₁} / (bir μ ν n.dist).real {n - k₂}

For k₁ < k₂, hearing "around n" raises the odds of n − k₁ against n − k₂ above their prior odds, whatever the priors, as soon as the radii between k₁ and k₂ have positive prior mass (the ratio inequality).

theorem EgreEtAl2023.between_ratio {μ : MeasureTheory.Measure ℕ} [MeasureTheory.IsFiniteMeasure μ] {a b k₁ k₂ : ℕ} (hk₁ : k₁ ∈ Set.Icc a b) (hk₂ : k₂ ∈ Set.Icc a b) (hab : μ (Set.Icc a b) ≠ 0) : ((ProbabilityTheory.Kernel.ofDensity μ betweenMeaning) (a, b)).real {k₁} / ((ProbabilityTheory.Kernel.ofDensity μ betweenMeaning) (a, b)).real {k₂} = μ.real {k₁} / μ.real {k₂}

"Between" leaves the odds unchanged, since for two values in its interval the ratio of posteriors is the ratio of priors (§4).

A case where the speaker prefers "around" (§5.2)

inductive EgreEtAl2023.Msg : Type

The six messages of §6.1, all centred on 4; "exactly 4" is "between 4 and 4".

• between0_8 : Msg
• between1_7 : Msg
• between2_6 : Msg
• between3_5 : Msg
• exactly4 : Msg
• around4 : Msg

@[instance_reducible]

instance EgreEtAl2023.instDecidableEqMsg : DecidableEq Msg

Equations

• EgreEtAl2023.instDecidableEqMsg x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance EgreEtAl2023.instFintypeMsg : Fintype Msg

Equations

• EgreEtAl2023.instFintypeMsg = { elems := { val := ↑EgreEtAl2023.Msg.enumList, nodup := EgreEtAl2023.Msg.enumList_nodup }, complete := EgreEtAl2023.instFintypeMsg._proof_1 }

@[instance_reducible]

instance EgreEtAl2023.instMeasurableSpaceMsg : MeasurableSpace Msg

Equations

• EgreEtAl2023.instMeasurableSpaceMsg = ⊤

instance EgreEtAl2023.instDiscreteMeasurableSpaceMsg : DiscreteMeasurableSpace Msg

noncomputable def EgreEtAl2023.Msg.meaning (ν : MeasureTheory.Measure ℕ) : Msg → Fin 9 → ENNReal

The graded meaning (12) gives crisp intervals for "between" and "exactly", and the radius-marginal weight of "around 4" at the radius prior ν.

Equations

• EgreEtAl2023.Msg.meaning ν EgreEtAl2023.Msg.between0_8 = (Set.Icc 0 8).indicator 1
• EgreEtAl2023.Msg.meaning ν EgreEtAl2023.Msg.between1_7 = (Set.Icc 1 7).indicator 1
• EgreEtAl2023.Msg.meaning ν EgreEtAl2023.Msg.between2_6 = (Set.Icc 2 6).indicator 1
• EgreEtAl2023.Msg.meaning ν EgreEtAl2023.Msg.between3_5 = (Set.Icc 3 5).indicator 1
• EgreEtAl2023.Msg.meaning ν EgreEtAl2023.Msg.exactly4 = {4}.indicator 1
• EgreEtAl2023.Msg.meaning ν EgreEtAl2023.Msg.around4 = EgreEtAl2023.aroundWeight ν fun (x : Fin 9) => Nat.dist 4 ↑x

noncomputable def EgreEtAl2023.radiusPrior : MeasureTheory.Measure ℕ

The radius prior of §7.2 is uniform on [0, 4].

Equations

• EgreEtAl2023.radiusPrior = EgreEtAl2023.unif 4

noncomputable def EgreEtAl2023.L0 : ProbabilityTheory.Kernel Msg (Fin 9)

The literal listener of §5.2 has a uniform prior on the nine values.

Equations

• EgreEtAl2023.L0 = ProbabilityTheory.Kernel.ofDensity MeasureTheory.Measure.count (EgreEtAl2023.Msg.meaning EgreEtAl2023.radiusPrior)

instance EgreEtAl2023.instIsZeroOrProbabilityMeasureFinOfNatNatCoeKernelMsgMeasureL0 (m : Msg) : MeasureTheory.IsZeroOrProbabilityMeasure (L0 m)

theorem EgreEtAl2023.L0_around4 : L0 Msg.around4 = bir MeasureTheory.Measure.count radiusPrior fun (x : Fin 9) => Nat.dist 4 ↑x

The "around 4" column is the Bayesian interpretation rule.

theorem EgreEtAl2023.meaning_around4 (y : Fin 9) : Msg.meaning radiusPrior Msg.around4 y = ↑(5 - Nat.dist 4 ↑y)

theorem EgreEtAl2023.L0_around4_apply_singleton (x : Fin 9) : (L0 Msg.around4) {x} = ↑(5 - Nat.dist 4 ↑x) / 25

theorem EgreEtAl2023.L0_between1_7_apply_singleton (x : Fin 9) : (L0 Msg.between1_7) {x} = if x ∈ Set.Icc 1 7 then 7⁻¹ else 0

theorem EgreEtAl2023.L0_exactly4_apply_singleton (x : Fin 9) : (L0 Msg.exactly4) {x} = if x = 4 then 1 else 0

def EgreEtAl2023.table1Weight : Fin 9 → ℕ

The speaker's belief of Table 1 has these weights, peaked at 4 with support [1, 7].

Equations

• EgreEtAl2023.table1Weight = ![0, 1, 1, 16, 64, 16, 1, 1, 0]

noncomputable def EgreEtAl2023.table1 : MeasureTheory.Measure (Fin 9)

The speaker's belief of Table 1.

Equations

• EgreEtAl2023.table1 = 100⁻¹ • ∑ x : Fin 9, ↑(EgreEtAl2023.table1Weight x) • MeasureTheory.Measure.dirac x

theorem EgreEtAl2023.table1_apply_singleton (x : Fin 9) : table1 {x} = 100⁻¹ * ↑(table1Weight x)

theorem EgreEtAl2023.table1_real_singleton (x : Fin 9) : table1.real {x} = ↑(table1Weight x) / 100

instance EgreEtAl2023.instIsProbabilityMeasureFinOfNatNatTable1 : MeasureTheory.IsProbabilityMeasure table1

theorem EgreEtAl2023.lintegral_count_meaning_around4 : ∫⁻ (x : Fin 9), Msg.meaning radiusPrior Msg.around4 x ∂MeasureTheory.Measure.count = 25

theorem EgreEtAl2023.lintegral_count_meaning_between1_7 : ∫⁻ (x : Fin 9), Msg.meaning radiusPrior Msg.between1_7 x ∂MeasureTheory.Measure.count = 7

instance EgreEtAl2023.instIsProbabilityMeasureFinOfNatNatCoeKernelMsgMeasureL0Around4 : MeasureTheory.IsProbabilityMeasure (L0 Msg.around4)

instance EgreEtAl2023.instIsProbabilityMeasureFinOfNatNatCoeKernelMsgMeasureL0Between1_7 : MeasureTheory.IsProbabilityMeasure (L0 Msg.between1_7)

theorem EgreEtAl2023.L0_around4_real_singleton (x : Fin 9) : (L0 Msg.around4).real {x} = ↑(5 - Nat.dist 4 ↑x) / 25

theorem EgreEtAl2023.L0_between1_7_real_singleton (x : Fin 9) : (L0 Msg.between1_7).real {x} = if x ∈ Set.Icc 1 7 then 1 / 7 else 0

theorem EgreEtAl2023.table1_ac_around4 : table1.AbsolutelyContinuous (L0 Msg.around4)

"Around 4" excludes no value, so Quality holds for every belief.

theorem EgreEtAl2023.table1_ac_between1_7 : table1.AbsolutelyContinuous (L0 Msg.between1_7)

"Between 1 and 7" excludes only values the belief of Table 1 excludes.

theorem EgreEtAl2023.table1_speaker_exactly4 {lam : ℝ} (hlam : 0 < lam) : ((RSA.speaker lam 0 ⇑L0 fun (x : Unit) => table1) ()) {Msg.exactly4} = 0

"Exactly 4" excludes values the belief of Table 1 leaves possible, so the speaker never uses it (footnote 17).

theorem EgreEtAl2023.table1_prefers_around {lam : ℝ} (hlam : 0 < lam) : ((RSA.speaker lam 0 ⇑L0 fun (x : Unit) => table1) ()).real {Msg.between1_7} < ((RSA.speaker lam 0 ⇑L0 fun (x : Unit) => table1) ()).real {Msg.around4}

With the belief of Table 1 the speaker prefers "around 4" to the best "between" (§5.2). At every rationality she uses it more than "between 1 and 7", the triangular posterior being closer to her belief than the flat one.

The full model (§6): joint listeners and score speakers

noncomputable def EgreEtAl2023.belief {X : Type u_1} {O : Type u_2} [MeasurableSpace X] [MeasurableSpace O] (P : MeasureTheory.Measure (X × O)) (o : O) : MeasureTheory.Measure X

The speaker's belief after observation o (§6.1) conditions the joint prior on o and marginalizes to the value, P(x = k | o).

Equations

• EgreEtAl2023.belief P o = MeasureTheory.Measure.map Prod.fst P[|Prod.snd ⁻¹' {o}]

theorem EgreEtAl2023.belief_apply_singleton {X : Type u_1} {O : Type u_2} [MeasurableSpace X] [MeasurableSpace O] (P : MeasureTheory.Measure (X × O)) [MeasurableSingletonClass X] (o : O) (x : X) : (belief P o) {x} = P {(x, o)} / P (Prod.snd ⁻¹' {o})

theorem EgreEtAl2023.isProbabilityMeasure_belief {X : Type u_1} {O : Type u_2} [MeasurableSpace X] [MeasurableSpace O] (P : MeasureTheory.Measure (X × O)) [MeasureTheory.IsFiniteMeasure P] {o : O} (ho : P (Prod.snd ⁻¹' {o}) ≠ 0) : MeasureTheory.IsProbabilityMeasure (belief P o)

noncomputable def EgreEtAl2023.jointL0 {X : Type u_1} {O : Type u_2} {M : Type u_3} [MeasurableSpace X] [MeasurableSpace O] [MeasurableSpace M] (P : MeasureTheory.Measure (X × O)) [Fintype M] [MeasurableSingletonClass M] (meaning : M → X → ENNReal) : ProbabilityTheory.Kernel M (X × O)

The literal listener over value and observation (12) reweights the joint prior by the meaning, which constrains the value alone.

Equations

• EgreEtAl2023.jointL0 P meaning = ProbabilityTheory.Kernel.ofDensity P fun (m : M) (p : X × O) => meaning m p.1

theorem EgreEtAl2023.jointL0_map_fst {X : Type u_1} {O : Type u_2} {M : Type u_3} [MeasurableSpace X] [MeasurableSpace O] [MeasurableSpace M] (P : MeasureTheory.Measure (X × O)) [Fintype X] [MeasurableSingletonClass X] [Fintype M] [MeasurableSingletonClass M] (meaning : M → X → ENNReal) (m : M) : MeasureTheory.Measure.map Prod.fst ((jointL0 P meaning) m) = (ProbabilityTheory.Kernel.ofDensity (MeasureTheory.Measure.map Prod.fst P) meaning) m

The value-marginal of the joint literal listener is the literal listener on the value-marginal prior, so eq. (BIR) is recovered inside the full model (footnote 23).

noncomputable def EgreEtAl2023.jointSpeaker {X : Type u_1} {O : Type u_2} {M : Type u_3} [MeasurableSpace X] [MeasurableSpace O] [MeasurableSpace M] (P : MeasureTheory.Measure (X × O)) [Fintype X] [Fintype M] [Fintype O] [MeasurableSingletonClass O] (lam : ℝ) (L : ProbabilityTheory.Kernel M (X × O)) : ProbabilityTheory.Kernel O M

To the speaker answering a joint listener (13) only the listener's value-marginal matters.

Equations

• EgreEtAl2023.jointSpeaker P lam L = RSA.speaker lam 0 (⇑(L.map Prod.fst)) (EgreEtAl2023.belief P)

noncomputable def EgreEtAl2023.listener {X : Type u_1} {O : Type u_2} {M : Type u_3} [MeasurableSpace X] [MeasurableSpace O] [MeasurableSpace M] (P : MeasureTheory.Measure (X × O)) [Fintype X] [Fintype M] [MeasurableSingletonClass M] (meaning : M → X → ENNReal) [Fintype O] [MeasurableSingletonClass O] (lam : ℝ) : ℕ → ProbabilityTheory.Kernel M (X × O)

In the recursion (16)–(17), listener n is the paper's Lⁿ, and jointSpeaker P lam (listener n) its Sⁿ⁺¹. The pragmatic listener answering a speaker, (15) and (17), reweights the joint prior by the speaker's probability of the message given the observation.

Equations

• EgreEtAl2023.listener P meaning lam 0 = EgreEtAl2023.jointL0 P meaning
• EgreEtAl2023.listener P meaning lam n.succ = RSA.listener P fun (p : X × O) => (EgreEtAl2023.jointSpeaker P lam (EgreEtAl2023.listener P meaning lam n)) p.2

Appendix A: the lexical uncertainty model and its limitation

def EgreEtAl2023.SameSupport {W : Type u_1} {O : Type u_2} [MeasurableSpace W] [MeasurableSpace O] (P : MeasureTheory.Measure (W × O)) (o₁ o₂ : O) : Prop

Two observations have the same support when their beliefs leave the same worlds possible.

Equations

• EgreEtAl2023.SameSupport P o₁ o₂ = ∀ (w : W), P {(w, o₁)} = 0 ↔ P {(w, o₂)} = 0

def EgreEtAl2023.Quality {W : Type u_1} {O : Type u_2} {I : Type u_3} {M : Type u_4} [MeasurableSpace W] [MeasurableSpace O] (P : MeasureTheory.Measure (W × O)) (sem : I → M → Set W) (o : O) (i : I) (m : M) : Prop

A message satisfies Quality (A.2) when it is true under the interpretation at every world the observation leaves possible.

Equations

• EgreEtAl2023.Quality P sem o i m = ∀ (w : W), P {(w, o)} ≠ 0 → w ∈ sem i m

theorem EgreEtAl2023.quality_iff_of_sameSupport {W : Type u_1} {O : Type u_2} {I : Type u_3} {M : Type u_4} [MeasurableSpace W] [MeasurableSpace O] (P : MeasureTheory.Measure (W × O)) (sem : I → M → Set W) {o₁ o₂ : O} (hs : SameSupport P o₁ o₂) {i : I} {m : M} : Quality P sem o₁ i m ↔ Quality P sem o₂ i m

Quality is a property of the support (A-1).

theorem EgreEtAl2023.snd_preimage_ae_le_iff_quality {W : Type u_1} {O : Type u_2} {I : Type u_3} {M : Type u_4} [MeasurableSpace W] [MeasurableSpace O] (P : MeasureTheory.Measure (W × O)) (sem : I → M → Set W) [Fintype W] [Fintype O] {o : O} {i : I} {m : M} : Prod.snd ⁻¹' {o} ≤ᵐ[P] sem i m ×ˢ Set.univ ↔ Quality P sem o i m

Quality is almost-sure entailment of the message by the observation.

noncomputable def EgreEtAl2023.luS1 {W : Type u_1} {O : Type u_2} {I : Type u_3} {M : Type u_4} [MeasurableSpace W] [MeasurableSpace O] (P : MeasureTheory.Measure (W × O)) (sem : I → M → Set W) [Fintype W] [Fintype O] [Fintype M] [MeasurableSpace M] [MeasurableSingletonClass O] [MeasurableSingletonClass M] (cost : M → ℝ) (lam : ℝ) (i : I) : ProbabilityTheory.Kernel O M

The level-1 speaker (eq. 3), relativized to an interpretation, answers the literal listener (A.1, eq. 1), who conditions the joint prior on the message's extension under the interpretation. After an observation she believes the joint prior conditioned on it, so her utility (A.1, eqs. 2 and 5) is the expected log of the listener's joint cell under her belief, less the message cost.

Equations

• EgreEtAl2023.luS1 P sem cost lam i = RSA.speaker lam cost ⇑(RSA.listener P (RSA.truthful fun (m : M) => sem i m ×ˢ Set.univ)) fun (o : O) => P[|Prod.snd ⁻¹' {o}]

theorem EgreEtAl2023.luS1_apply_singleton_eq_zero_iff {W : Type u_1} {O : Type u_2} {I : Type u_3} {M : Type u_4} [MeasurableSpace W] [MeasurableSpace O] (P : MeasureTheory.Measure (W × O)) (sem : I → M → Set W) [Fintype W] [Fintype O] [Fintype M] [MeasurableSpace M] [MeasurableSingletonClass W] [MeasurableSingletonClass O] [MeasurableSingletonClass M] [MeasureTheory.IsFiniteMeasure P] (cost : M → ℝ) (lam : ℝ) (hlam : 0 < lam) {o : O} {i : I} {m : M} : ((luS1 P sem cost lam i) o) {m} = 0 ↔ ¬Quality P sem o i m

The level-1 speaker uses exactly the messages that satisfy Quality (A-2a).

theorem EgreEtAl2023.luS1_eq_of_sameSupport {W : Type u_1} {O : Type u_2} {I : Type u_3} {M : Type u_4} [MeasurableSpace W] [MeasurableSpace O] (P : MeasureTheory.Measure (W × O)) (sem : I → M → Set W) [Fintype W] [Fintype O] [Fintype M] [MeasurableSpace M] [MeasurableSingletonClass W] [MeasurableSingletonClass O] [MeasurableSingletonClass M] [MeasureTheory.IsFiniteMeasure P] (cost : M → ℝ) (lam : ℝ) (hlam : 0 < lam) {o₁ o₂ : O} (hs : SameSupport P o₁ o₂) (ho₁ : P (Prod.snd ⁻¹' {o₁}) ≠ 0) (ho₂ : P (Prod.snd ⁻¹' {o₂}) ≠ 0) (i : I) : (luS1 P sem cost lam i) o₂ = (luS1 P sem cost lam i) o₁

The interpretation-relativized level-1 speaker treats same-support observations alike (A-7).

theorem EgreEtAl2023.speaker_ofDensity_snd_eq {W : Type u_1} {O : Type u_2} {M : Type u_4} [MeasurableSpace W] [MeasurableSpace O] (P : MeasureTheory.Measure (W × O)) [Fintype W] [Fintype O] [Fintype M] [MeasurableSpace M] [MeasurableSingletonClass W] [MeasurableSingletonClass O] [MeasurableSingletonClass M] [MeasureTheory.IsFiniteMeasure P] (cost : M → ℝ) (lam : ℝ) (hlam : 0 ≤ lam) {o₁ o₂ : O} (ho₁ : P (Prod.snd ⁻¹' {o₁}) ≠ 0) (ho₂ : P (Prod.snd ⁻¹' {o₂}) ≠ 0) (G : O → M → ENNReal) (hG : ∀ (m : M), G o₂ m = G o₁ m) : (RSA.speaker lam cost ⇑(ProbabilityTheory.Kernel.ofDensity P fun (m : M) (p : W × O) => G p.2 m) fun (o : O) => P[|Prod.snd ⁻¹' {o}]) o₂ = (RSA.speaker lam cost ⇑(ProbabilityTheory.Kernel.ofDensity P fun (m : M) (p : W × O) => G p.2 m) fun (o : O) => P[|Prod.snd ⁻¹' {o}]) o₁

The listeners of level n + 1 and the level-1 listener are the joint prior reweighted by a term in the message and the observation. The speaker answering such a listener treats two observations alike whenever that term does, the prior cancelling from her choice ((A-6), (A-9), (A-10)).

noncomputable def EgreEtAl2023.luListener {W : Type u_1} {O : Type u_2} {I : Type u_3} {M : Type u_4} [MeasurableSpace W] [MeasurableSpace O] (P : MeasureTheory.Measure (W × O)) (sem : I → M → Set W) [Fintype W] [Fintype O] [Fintype M] [MeasurableSpace M] [MeasurableSingletonClass O] [MeasurableSingletonClass M] (cost : M → ℝ) (lam : ℝ) [Fintype I] [MeasurableSpace I] (PI : MeasureTheory.Measure I) : ℕ → ProbabilityTheory.Kernel M (W × O)

The listeners Lⁿ⁺¹. The level-1 listener (eq. 4) reweights the joint prior by the level-1 speaker's use of the message, averaged over interpretations, and each later one (eqs. 5–7) by the previous speaker's.

Equations

• One or more equations did not get rendered due to their size.
• EgreEtAl2023.luListener P sem cost lam PI 0 = RSA.listener P fun (p : W × O) => (∑ i : I, PI {i} • EgreEtAl2023.luS1 P sem cost lam i) p.2

noncomputable def EgreEtAl2023.luSpeaker {W : Type u_1} {O : Type u_2} {I : Type u_3} {M : Type u_4} [MeasurableSpace W] [MeasurableSpace O] (P : MeasureTheory.Measure (W × O)) (sem : I → M → Set W) [Fintype W] [Fintype O] [Fintype M] [MeasurableSpace M] [MeasurableSingletonClass O] [MeasurableSingletonClass M] (cost : M → ℝ) (lam : ℝ) [Fintype I] [MeasurableSpace I] (PI : MeasureTheory.Measure I) (n : ℕ) : ProbabilityTheory.Kernel O M

The speaker Sⁿ⁺² (eq. 6), answering luListener n.

Equations

• EgreEtAl2023.luSpeaker P sem cost lam PI n = RSA.speaker lam cost ⇑(EgreEtAl2023.luListener P sem cost lam PI n) fun (o : O) => P[|Prod.snd ⁻¹' {o}]

theorem EgreEtAl2023.luSpeaker_eq_of_sameSupport {W : Type u_1} {O : Type u_2} {I : Type u_3} {M : Type u_4} [MeasurableSpace W] [MeasurableSpace O] (P : MeasureTheory.Measure (W × O)) (sem : I → M → Set W) [Fintype W] [Fintype O] [Fintype M] [MeasurableSpace M] [MeasurableSingletonClass W] [MeasurableSingletonClass O] [MeasurableSingletonClass M] [MeasureTheory.IsFiniteMeasure P] (cost : M → ℝ) (lam : ℝ) [Fintype I] [MeasurableSpace I] (PI : MeasureTheory.Measure I) (hlam : 0 < lam) {o₁ o₂ : O} (hs : SameSupport P o₁ o₂) (ho₁ : P (Prod.snd ⁻¹' {o₁}) ≠ 0) (ho₂ : P (Prod.snd ⁻¹' {o₂}) ≠ 0) (n : ℕ) : (luSpeaker P sem cost lam PI n) o₂ = (luSpeaker P sem cost lam PI n) o₁

In the lexical uncertainty model, observations with the same support yield the same speaker at every level, so the choice of message depends on the support of the speaker's belief and not on its shape ((A-8), the limitation (18)).

Appendix B: the weighted interpretation rule

def EgreEtAl2023.within {X : Type u_1} (d : X → ℕ) (y : ℕ) : Set X

The values within radius y of the target.

Equations

• EgreEtAl2023.within d y = {x : X | d x ≤ y}

noncomputable def EgreEtAl2023.wir {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure ℕ) (d : X → ℕ) : MeasureTheory.Measure X

The weighted rule (WIR) mixes the prior conditioned on each interval by the prior over radii.

Equations

• EgreEtAl2023.wir μ ν d = ν.bind fun (y : ℕ) => μ[|EgreEtAl2023.within d y]

noncomputable def EgreEtAl2023.radiusPosterior {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure ℕ) (d : X → ℕ) : MeasureTheory.Measure ℕ

The posterior over radii after "around".

Equations

• EgreEtAl2023.radiusPosterior μ ν d = MeasureTheory.Measure.map Prod.snd (μ.prod ν)[|EgreEtAl2023.AroundEvent d]

theorem EgreEtAl2023.radiusPosterior_apply_singleton {X : Type u_1} [MeasurableSpace X] [Countable X] [MeasurableSingletonClass X] (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure ℕ) (d : X → ℕ) [MeasureTheory.SFinite ν] (y : ℕ) : (radiusPosterior μ ν d) {y} = μ (within d y) * ν {y} / ∫⁻ (x : X), aroundWeight ν d x ∂μ

theorem EgreEtAl2023.within_dist (n y : ℕ) : within n.dist y = Set.Icc (n - y) (n + y)

theorem EgreEtAl2023.bir_eq_bind_radiusPosterior {X : Type u_1} [MeasurableSpace X] [Countable X] [MeasurableSingletonClass X] (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure ℕ) (d : X → ℕ) [MeasureTheory.SFinite ν] [MeasureTheory.IsFiniteMeasure μ] : bir μ ν d = (radiusPosterior μ ν d).bind fun (y : ℕ) => μ[|within d y]

The Bayesian rule is the weighted rule with the posterior over radii in place of the prior (BIR′), so the two rules differ exactly in which distribution over radii weights the intervals.

theorem EgreEtAl2023.wir_ne_bir : wir (unif 2) (2⁻¹ • unif 1) (Nat.dist 1) ≠ bir (unif 2) (2⁻¹ • unif 1) (Nat.dist 1)

At n = 1 with uniform priors the weighted rule puts 2/3 on the target where the Bayesian rule puts 1/2, so the two rules differ (Figure 2 against Figure 5).