Linglib.Theories.Pragmatics.RSA.Implementations.EgreEtAl2023

For a speaker who observed 3, "around 3" has better utility than "between 0 6" (same support, but flat). This is the paper's key result: peaked shape yields lower KL from peaked belief.

source

def RSA.EgreEtAl2023.SameSupport {α : Type} (d₁ d₂ : α → ℚ) :

Prop

Same support: P(w|o₁) > 0 ↔ P(w|o₂) > 0.

Equations

RSA.EgreEtAl2023.SameSupport d₁ d₂ = ∀ (x : α), d₁ x > 0 ↔ d₂ x > 0

Instances For

source

def RSA.EgreEtAl2023.RespectsQuality {W I : Type} (m_true : I → W → Bool) (obs : W → ℚ) (i : I) :

Prop

Quality: ∀ w, P(w|o) > 0 → ⟦m⟧ⁱ(w) = 1.

Equations

RSA.EgreEtAl2023.RespectsQuality m_true obs i = ∀ (w : W), obs w > 0 → m_true i w = true

Instances For

source

def RSA.EgreEtAl2023.RespectsWeakQuality {W I : Type} (m_true : I → W → Bool) (obs : W → ℚ) :

Prop

Weak Quality: ∃ i, Quality(m, o, i).

Equations

RSA.EgreEtAl2023.RespectsWeakQuality m_true obs = ∃ (i : I), RSA.EgreEtAl2023.RespectsQuality m_true obs i

Instances For

source

theorem RSA.EgreEtAl2023.quality_preserved_by_same_support {W I : Type} (m_true : I → W → Bool) (d₁ d₂ : W → ℚ) (i : I) (h_same : SameSupport d₁ d₂) :

RespectsQuality m_true d₁ i ↔ RespectsQuality m_true d₂ i

(A-1a) Quality preserved under same support.

source

theorem RSA.EgreEtAl2023.weak_quality_preserved_by_same_support {W I : Type} (m_true : I → W → Bool) (d₁ d₂ : W → ℚ) (h_same : SameSupport d₁ d₂) :

RespectsWeakQuality m_true d₁ ↔ RespectsWeakQuality m_true d₂

(A-1b) Weak Quality preserved under same support.

source

def RSA.EgreEtAl2023.softMaxScore (utilities : List ℚ) (k : ℕ) (alpha : ℚ) :

ℚ

SoftMax(x_k, x, λ) = exp(λx_k) / Σ_j exp(λx_j).

Equations

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

Instances For

source

def RSA.EgreEtAl2023.translateUtilities (utils : List ℚ) (a : ℚ) :

List ℚ

Equations

RSA.EgreEtAl2023.translateUtilities utils a = List.map (fun (x : ℚ) => x + a) utils

Instances For

source

def RSA.EgreEtAl2023.utilityDifferenceConstant {W : Type} [BEq W] (support : List W) (d₁ d₂ : W → ℚ) :

ℚ

K(o₁,o₂): utility difference constant, independent of m and i (Core Lemma A-6).

Equations

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

Instances For

source

def RSA.EgreEtAl2023.U1 {W M I : Type} [BEq W] (l0 : M → I → W → ℚ) (obs : W → ℚ) (m : M) (i : I) (worlds : List W) :

ℚ

U¹(m, o, i) = Σ_w P(w|o) · log L⁰(w | m, i) — speaker utility at level 1. This is the KL-based utility: higher when L⁰ matches the observation.

Equations

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

Instances For

source

def RSA.EgreEtAl2023.S1_score {W M I : Type} [BEq W] [BEq M] (l0 : M → I → W → ℚ) (obs : W → ℚ) (messages : List M) (i : I) (worlds : List W) (alpha : ℚ) (m : M) :

ℚ

S¹(m | o, i) = SoftMax over U¹ utilities across messages.

Equations

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

Instances For

source

theorem RSA.EgreEtAl2023.no_quality_implies_S1_zero {W M I : Type} [BEq W] [BEq M] (l0 : M → I → W → ℚ) (obs : W → ℚ) (_messages : List M) (i : I) (worlds : List W) (_alpha : ℚ) (m : M) (h_nq : ∀ (w : W), obs w > 0 → l0 m i w = 0) :

U1 l0 obs m i worlds = 0

source

theorem RSA.EgreEtAl2023.core_lemma_A6 {W M I : Type} [Fintype W] (f : W → ℝ) (c : M → I → ℝ) (d₁ d₂ : W → ℝ) (h_sum : ∑ w : W, d₁ w = ∑ w : W, d₂ w) (m₁ m₂ : M) (i₁ i₂ : I) :

∑ w : W, d₂ w * (f w + c m₁ i₁) - ∑ w : W, d₁ w * (f w + c m₁ i₁) = ∑ w : W, d₂ w * (f w + c m₂ i₂) - ∑ w : W, d₁ w * (f w + c m₂ i₂)

(A-6) Core Lemma over ℝ: the utility difference U(m,d₂,i) - U(m,d₁,i) is constant across all messages m and interpretations i, provided Σd₁ = Σd₂.

Under Quality, log L⁰(w|m,i) = f(w) + c(m,i) where f(w) = log prior(w) and c(m,i) = −log Z(m,i). Since f doesn't depend on m,i and Σd₁ = Σd₂, the c(m,i) term cancels in the difference, making K independent of m and i.

source

theorem RSA.EgreEtAl2023.same_support_implies_equal_S1 {M : Type} [Fintype M] (u₁ u₂ : M → ℝ) (α : ℝ) (h_shift : ∃ (K : ℝ), ∀ (m : M), u₂ m = u₁ m + K) :

Core.softmax u₂ α = Core.softmax u₁ α

(A-7) Same support → S¹ equal over ℝ: when utility vectors differ by a constant, softmax is invariant by Core.softmax_add_const.

By A-6, U¹(·, d₂, i) = U¹(·, d₁, i) + K for some constant K. By A-5 (translation invariance), softmax(u + K, α) = softmax(u, α).

source

theorem RSA.EgreEtAl2023.lu_limitation {M : Type} [Fintype M] (u₁ u₂ : M → ℝ) (α : ℝ) (h_shift : ∃ (K : ℝ), ∀ (m : M), u₂ m = u₁ m + K) :

Core.softmax u₂ α = Core.softmax u₁ α

(A-8) LU Limitation over ℝ: same support → Sⁿ(m|o₁) = Sⁿ(m|o₂) for all n ≥ 1. At level 1, this is a direct corollary of A-7. The paper's full inductive argument (higher recursion depths) follows the same pattern: each Lⁿ is built from Sⁿ⁻¹ which are equal by inductive hypothesis, so Uⁿ differs by a constant, so Sⁿ is equal by softmax translation invariance.

source

theorem RSA.EgreEtAl2023.wir_peaked_at_center :

RSA.EgreEtAl2023.getScore✝ wir_around3 Value.v3 > RSA.EgreEtAl2023.getScore✝¹ wir_around3 Value.v1

source

theorem RSA.EgreEtAl2023.bir_wir_differ :

RSA.EgreEtAl2023.getScore✝ l0_around3 Value.v2 ≠ RSA.EgreEtAl2023.getScore✝¹ wir_around3 Value.v2

BIR and WIR differ quantitatively under uniform priors.

source

def RSA.EgreEtAl2023.obs_peaked :

Value → ℚ

Equations

RSA.EgreEtAl2023.obs_peaked RSA.EgreEtAl2023.Value.v1 = 1 / 6
RSA.EgreEtAl2023.obs_peaked RSA.EgreEtAl2023.Value.v2 = 1 / 6
RSA.EgreEtAl2023.obs_peaked RSA.EgreEtAl2023.Value.v3 = 1 / 3
RSA.EgreEtAl2023.obs_peaked RSA.EgreEtAl2023.Value.v4 = 1 / 6
RSA.EgreEtAl2023.obs_peaked RSA.EgreEtAl2023.Value.v5 = 1 / 6
RSA.EgreEtAl2023.obs_peaked x✝ = 0

Instances For

source

def RSA.EgreEtAl2023.obs_flat :

Value → ℚ

Equations

RSA.EgreEtAl2023.obs_flat RSA.EgreEtAl2023.Value.v1 = 1 / 5
RSA.EgreEtAl2023.obs_flat RSA.EgreEtAl2023.Value.v2 = 1 / 5
RSA.EgreEtAl2023.obs_flat RSA.EgreEtAl2023.Value.v3 = 1 / 5
RSA.EgreEtAl2023.obs_flat RSA.EgreEtAl2023.Value.v4 = 1 / 5
RSA.EgreEtAl2023.obs_flat RSA.EgreEtAl2023.Value.v5 = 1 / 5
RSA.EgreEtAl2023.obs_flat x✝ = 0

Instances For

source

theorem RSA.EgreEtAl2023.obs_same_support (x : Value) :

obs_peaked x > 0 ↔ obs_flat x > 0

source

def RSA.EgreEtAl2023.U_std (l0_scores obs : Value → ℚ) :

ℚ

C.1: Standard utility U_std(m,o) = Σ_w P(w|o) · log(Σ_{o'} L(w,o')). Under standard utility, U_std differs for same-support observations because the marginal Σ_{o'} L(w,o') washes out observation-specific shape.

Equations

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

Instances For

source

def RSA.EgreEtAl2023.U_bergen (l0_scores obs : Value → ℚ) :

ℚ

C.2: Bergen utility U_bergen(m,o) = Σ_w P(w|o) · log L(w|o). Under Bergen utility, the observation enters both the weight and the listener posterior, so same-support observations yield different utilities (the peaked observation gets higher utility from a peaked L0).

Equations

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

Instances For

source

def RSA.EgreEtAl2023.l0_around3_fn :

Value → ℚ

Equations

RSA.EgreEtAl2023.l0_around3_fn v = RSA.EgreEtAl2023.getScore✝ RSA.EgreEtAl2023.l0_around3 v

Instances For

source

theorem RSA.EgreEtAl2023.peaked_gets_higher_utility_from_around :

U_bergen l0_around3_fn obs_peaked > U_bergen l0_around3_fn obs_flat

Peaked observation has better utility from triangular L0 than flat does. This is because the peaked observation puts more weight on center values where L0 also has higher probability — better KL alignment.

source

def RSA.EgreEtAl2023.l0_between_fn :

Value → ℚ

Both observations get the SAME utility under a uniform L0 (from "between"). This demonstrates the LU limitation: uniform L0 cannot distinguish shapes.

Equations

RSA.EgreEtAl2023.l0_between_fn v = RSA.EgreEtAl2023.getScore✝ RSA.EgreEtAl2023.l0_between1_5 v

Instances For

source

theorem RSA.EgreEtAl2023.same_utility_under_uniform_l0 :

U_bergen l0_between_fn obs_peaked = U_bergen l0_between_fn obs_flat

source

theorem RSA.EgreEtAl2023.bir_from_compositional_meaning (v : Value) :

birWeight 3 v = ↑(List.filter (fun (y : Tolerance) => aroundMeaning 3 y v) (List.filter (fun (y : Tolerance) => decide (y.toNat ≤ 3)) allTolerances)).length / 4

BIR weight = marginalization of aroundMeaning over valid tolerances y ≤ n.

source

BIR (L0) ranking matches closed-form prediction: v3 > v2 > v1 > v0.

source

theorem RSA.EgreEtAl2023.bir_matches_closed_form (v : Value) :

RSA.EgreEtAl2023.getScore✝ l0_around3 v = birClosedForm 3 v.toNat

BIR posterior matches closed-form for each value (n=3).