Égré et al. (2023)

@cite{egre-etal-2023}

"On the optimality of vagueness: 'around', 'between', and the Sorites" Linguistics and Philosophy 46:1101–1130

Phenomena

1. "Around n" produces triangular (tent-shaped) interpretation distributions
2. "Around n" conveys more shape information than "between a and b"
3. Speakers prefer "around n" for peaked private distributions
4. The round/non-round asymmetry affects "around" acceptability
5. Sorites-like tolerance chains for "around"

RSA Model

"Around n" is interpreted via marginalization over a tolerance parameter y. BIR: P(x=k | around n) ∝ P(x=k) × Σ_{y≥|n-k|} P(y)

The BIR is the literal listener (L0). The RSA layers (S1, higher Ln) build on this via KL-divergence speaker utility and softmax. The paper shows this model produces a triangular posterior, satisfies the Ratio Inequality, and explains why speakers prefer "around n" over "between a b" for peaked private distributions. The LU limitation (Appendix A) proves standard LU models cannot derive the triangular shape.

structure EgreEtAl2023.ShapeInferenceDatum : Type

Shape inference datum: "around n" vs "between a b" interpretation shape.

The key empirical claim: hearing "around n" leads to a peaked (triangular) interpretation centered on n, while "between a b" leads to a flat (uniform) interpretation over [a,b].

• vagueExpression : String

  The vague expression

• preciseAlternative : String

  The precise alternative

• center : ℕ

  Center value n

• vagueIsPeaked : Bool

  Does the vague expression produce peaked interpretation?

• preciseIsPeaked : Bool

  Does the precise alternative produce peaked interpretation?

• notes : String

  Notes

def EgreEtAl2023.instReprShapeInferenceDatum.repr : ShapeInferenceDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance EgreEtAl2023.instReprShapeInferenceDatum : Repr ShapeInferenceDatum

Equations

• EgreEtAl2023.instReprShapeInferenceDatum = { reprPrec := EgreEtAl2023.instReprShapeInferenceDatum.repr }

def EgreEtAl2023.aroundVsBetween : ShapeInferenceDatum

"Around 20" produces peaked interpretation; "between 10 and 30" does not.

Source: Égré et al. 2023, Sections 5-6, Figure 2 vs Figure 5

Equations

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

structure EgreEtAl2023.SpeakerPreferenceDatum : Type

Speaker preference datum: when does a speaker choose "around n" over "between a b"?

• privateDistShape : String

  Speaker's private distribution shape

• preferredMessage : String

  Preferred message

• alternativeMessage : String

  Alternative message

• reason : String

  Why preferred?

@[implicit_reducible]

instance EgreEtAl2023.instReprSpeakerPreferenceDatum : Repr SpeakerPreferenceDatum

Equations

• EgreEtAl2023.instReprSpeakerPreferenceDatum = { reprPrec := EgreEtAl2023.instReprSpeakerPreferenceDatum.repr }

def EgreEtAl2023.instReprSpeakerPreferenceDatum.repr : SpeakerPreferenceDatum → ℕ → Std.Format

Equations

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

def EgreEtAl2023.peakedSpeakerPreference : SpeakerPreferenceDatum

Speakers with peaked beliefs prefer "around n".

Source: Égré et al. 2023, Section 6

Equations

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

def EgreEtAl2023.flatSpeakerPreference : SpeakerPreferenceDatum

Speakers with flat beliefs prefer "between a b".

Source: Égré et al. 2023, Section 6

Equations

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

structure EgreEtAl2023.SoritesAroundDatum : Type

Sorites chain datum for "around".

The sorites for "around n": If k is around n, and k' is close to k, then k' is around n. Applied repeatedly, this would make 0 "around 100".

• center : ℕ

  Center value

• stepSize : ℕ

  Step size in chain

• startValue : ℕ

  Starting value (clearly "around n")

• endValue : ℕ

  Ending value (clearly not "around n")

• individualStepsCompelling : Bool

  Is each individual step compelling?

• conclusionAcceptable : Bool

  Is the conclusion acceptable?

@[implicit_reducible]

instance EgreEtAl2023.instReprSoritesAroundDatum : Repr SoritesAroundDatum

Equations

• EgreEtAl2023.instReprSoritesAroundDatum = { reprPrec := EgreEtAl2023.instReprSoritesAroundDatum.repr }

def EgreEtAl2023.instReprSoritesAroundDatum.repr : SoritesAroundDatum → ℕ → Std.Format

Equations

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

def EgreEtAl2023.soritesAround20 : SoritesAroundDatum

Equations

• EgreEtAl2023.soritesAround20 = { center := 20, stepSize := 1, startValue := 20, endValue := 0, individualStepsCompelling := true, conclusionAcceptable := false }

structure EgreEtAl2023.LULimitationDatum : Type

LU limitation datum: observations that LU cannot distinguish.

The LU model assigns the same speaker probabilities to observations with the same support, even when their shapes differ dramatically.

• observation1 : String

  First observation

• shape1 : String

  First observation shape

• observation2 : String

  Second observation

• shape2 : String

  Second observation shape

• sameSupport : Bool

  Same support?

• luDistinguishes : Bool

  LU distinguishes them?

• birDistinguishes : Bool

  BIR model distinguishes them?

def EgreEtAl2023.instReprLULimitationDatum.repr : LULimitationDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance EgreEtAl2023.instReprLULimitationDatum : Repr LULimitationDatum

Equations

• EgreEtAl2023.instReprLULimitationDatum = { reprPrec := EgreEtAl2023.instReprLULimitationDatum.repr }

def EgreEtAl2023.luFailsOnShape : LULimitationDatum

Peaked vs flat distributions with same support: LU fails, BIR succeeds.

Source: Égré et al. 2023, Section 7, Appendix A

Equations

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

structure EgreEtAl2023.ClosedFormDatum : Type

Closed-form prediction datum: the triangular posterior formula.

Under uniform priors on x in {0,...,N} and y in {0,...,N}: P(x=k | around n) = (n - |n-k| + 1) / (n+1)^2

• domainMax : ℕ

  Domain maximum N

• center : ℕ

  Center n

• value : ℕ

  Value k

• expectedProb : ℚ

  Expected probability (rational)

• notes : String

  Notes

@[implicit_reducible]

instance EgreEtAl2023.instReprClosedFormDatum : Repr ClosedFormDatum

Equations

• EgreEtAl2023.instReprClosedFormDatum = { reprPrec := EgreEtAl2023.instReprClosedFormDatum.repr }

def EgreEtAl2023.instReprClosedFormDatum.repr : ClosedFormDatum → ℕ → Std.Format

Equations

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

def EgreEtAl2023.closedForm_center : ClosedFormDatum

P(x=20 | around 20) under uniform prior on {0,...,40}

Equations

• EgreEtAl2023.closedForm_center = { domainMax := 40, center := 20, value := 20, expectedProb := 21 / 441, notes := "Peak of triangular distribution" }

def EgreEtAl2023.closedForm_offset5 : ClosedFormDatum

P(x=15 | around 20) under uniform prior on {0,...,40}

Equations

• EgreEtAl2023.closedForm_offset5 = { domainMax := 40, center := 20, value := 15, expectedProb := 16 / 441, notes := "5 units from center, probability drops linearly" }

def EgreEtAl2023.shapeInferenceData : List ShapeInferenceDatum

Equations

• EgreEtAl2023.shapeInferenceData = [EgreEtAl2023.aroundVsBetween]

def EgreEtAl2023.speakerPreferenceData : List SpeakerPreferenceDatum

Equations

• EgreEtAl2023.speakerPreferenceData = [EgreEtAl2023.peakedSpeakerPreference, EgreEtAl2023.flatSpeakerPreference]

def EgreEtAl2023.soritesData : List SoritesAroundDatum

Equations

• EgreEtAl2023.soritesData = [EgreEtAl2023.soritesAround20]

def EgreEtAl2023.luLimitationData : List LULimitationDatum

Equations

• EgreEtAl2023.luLimitationData = [EgreEtAl2023.luFailsOnShape]

def EgreEtAl2023.closedFormData : List ClosedFormDatum

Equations

• EgreEtAl2023.closedFormData = [EgreEtAl2023.closedForm_center, EgreEtAl2023.closedForm_offset5]

inductive EgreEtAl2023.Value : Type

• v0 : Value
• v1 : Value
• v2 : Value
• v3 : Value
• v4 : Value
• v5 : Value
• v6 : Value

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

Equations

• EgreEtAl2023.instReprValue.repr EgreEtAl2023.Value.v0 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "EgreEtAl2023.Value.v0")).group prec✝
• EgreEtAl2023.instReprValue.repr EgreEtAl2023.Value.v1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "EgreEtAl2023.Value.v1")).group prec✝
• EgreEtAl2023.instReprValue.repr EgreEtAl2023.Value.v2 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "EgreEtAl2023.Value.v2")).group prec✝
• EgreEtAl2023.instReprValue.repr EgreEtAl2023.Value.v3 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "EgreEtAl2023.Value.v3")).group prec✝
• EgreEtAl2023.instReprValue.repr EgreEtAl2023.Value.v4 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "EgreEtAl2023.Value.v4")).group prec✝
• EgreEtAl2023.instReprValue.repr EgreEtAl2023.Value.v5 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "EgreEtAl2023.Value.v5")).group prec✝
• EgreEtAl2023.instReprValue.repr EgreEtAl2023.Value.v6 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "EgreEtAl2023.Value.v6")).group prec✝

@[implicit_reducible]

instance EgreEtAl2023.instReprValue : Repr Value

Equations

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

@[implicit_reducible]

instance EgreEtAl2023.instDecidableEqValue : DecidableEq Value

Equations

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

@[implicit_reducible]

instance EgreEtAl2023.instFintypeValue : Fintype Value

Equations

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

def EgreEtAl2023.Value.toNat : Value → ℕ

Equations

• EgreEtAl2023.Value.v0.toNat = 0
• EgreEtAl2023.Value.v1.toNat = 1
• EgreEtAl2023.Value.v2.toNat = 2
• EgreEtAl2023.Value.v3.toNat = 3
• EgreEtAl2023.Value.v4.toNat = 4
• EgreEtAl2023.Value.v5.toNat = 5
• EgreEtAl2023.Value.v6.toNat = 6

inductive EgreEtAl2023.Tolerance : Type

Tolerance y: "around n" with tolerance y means x ∈ [n-y, n+y].

• y0 : Tolerance
• y1 : Tolerance
• y2 : Tolerance
• y3 : Tolerance
• y4 : Tolerance
• y5 : Tolerance
• y6 : Tolerance

def EgreEtAl2023.instReprTolerance.repr : Tolerance → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance EgreEtAl2023.instReprTolerance : Repr Tolerance

Equations

• EgreEtAl2023.instReprTolerance = { reprPrec := EgreEtAl2023.instReprTolerance.repr }

@[implicit_reducible]

instance EgreEtAl2023.instDecidableEqTolerance : DecidableEq Tolerance

Equations

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

@[implicit_reducible]

instance EgreEtAl2023.instFintypeTolerance : Fintype Tolerance

Equations

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

def EgreEtAl2023.Tolerance.toNat : Tolerance → ℕ

Equations

• EgreEtAl2023.Tolerance.y0.toNat = 0
• EgreEtAl2023.Tolerance.y1.toNat = 1
• EgreEtAl2023.Tolerance.y2.toNat = 2
• EgreEtAl2023.Tolerance.y3.toNat = 3
• EgreEtAl2023.Tolerance.y4.toNat = 4
• EgreEtAl2023.Tolerance.y5.toNat = 5
• EgreEtAl2023.Tolerance.y6.toNat = 6

def EgreEtAl2023.allValues : List Value

Equations

• EgreEtAl2023.allValues = [EgreEtAl2023.Value.v0, EgreEtAl2023.Value.v1, EgreEtAl2023.Value.v2, EgreEtAl2023.Value.v3, EgreEtAl2023.Value.v4, EgreEtAl2023.Value.v5, EgreEtAl2023.Value.v6]

def EgreEtAl2023.allTolerances : List Tolerance

Equations

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

def EgreEtAl2023.aroundMeaning (n : ℕ) (y : Tolerance) (x : Value) : Bool

⟦around n⟧(y)(x) = 1 iff |n - x| ≤ y

Equations

• EgreEtAl2023.aroundMeaning n y x = decide ((if n ≥ x.toNat then n - x.toNat else x.toNat - n) ≤ y.toNat)

def EgreEtAl2023.betweenMeaning (a b : ℕ) (x : Value) : Bool

Equations

• EgreEtAl2023.betweenMeaning a b x = (decide (a ≤ x.toNat) && decide (x.toNat ≤ b))

def EgreEtAl2023.exactlyMeaning (n : ℕ) (x : Value) : Bool

Equations

• EgreEtAl2023.exactlyMeaning n x = (x.toNat == n)

def EgreEtAl2023.birWeight (n : ℕ) (x : Value) : ℚ

BIR weight: Σ_{y ≥ |n-x|} P(y) under uniform P(y) on {0,...,n}. Section 3.2.2, p.1085: y ranges over {0,...,n}, not the full value domain.

Equations

• EgreEtAl2023.birWeight n x = ↑(if (if n ≥ x.toNat then n - x.toNat else x.toNat - n) ≤ n then (n - if n ≥ x.toNat then n - x.toNat else x.toNat - n) + 1 else 0) / (↑n + 1)

def EgreEtAl2023.birPosterior (n : ℕ) : List (Value × ℚ)

BIR posterior = L0 for "around n".

Equations

• EgreEtAl2023.birPosterior n = EgreEtAl2023.normalize✝ (List.map (fun (v : EgreEtAl2023.Value) => (v, EgreEtAl2023.birWeight n v)) EgreEtAl2023.allValues)

def EgreEtAl2023.birClosedForm (n k : ℕ) : ℚ

Closed form (Section 3.2.2): P(x=k | around n) = (n - |n-k| + 1) / (n+1)²

Equations

• EgreEtAl2023.birClosedForm n k = if (if n ≥ k then n - k else k - n) > n then 0 else ↑(↑n - ↑(if n ≥ k then n - k else k - n) + 1) / (↑(↑n + 1) * ↑(↑n + 1))

def EgreEtAl2023.l0_around3 : List (Value × ℚ)

Equations

• EgreEtAl2023.l0_around3 = EgreEtAl2023.birPosterior 3

def EgreEtAl2023.intervalPosterior (a b : ℕ) : List (Value × ℚ)

L0 for "between a b" = uniform over [a,b].

Equations

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

def EgreEtAl2023.l0_between0_6 : List (Value × ℚ)

Equations

• EgreEtAl2023.l0_between0_6 = EgreEtAl2023.intervalPosterior 0 6

def EgreEtAl2023.l0_between1_5 : List (Value × ℚ)

Equations

• EgreEtAl2023.l0_between1_5 = EgreEtAl2023.intervalPosterior 1 5

def EgreEtAl2023.l0_between2_4 : List (Value × ℚ)

Equations

• EgreEtAl2023.l0_between2_4 = EgreEtAl2023.intervalPosterior 2 4

def EgreEtAl2023.exactPosterior (n : ℕ) : List (Value × ℚ)

L0 for "exactly n" = point mass at n.

Equations

• EgreEtAl2023.exactPosterior n = EgreEtAl2023.normalize✝ (List.map (fun (v : EgreEtAl2023.Value) => (v, if EgreEtAl2023.exactlyMeaning n v = true then 1 else 0)) EgreEtAl2023.allValues)

def EgreEtAl2023.l0_exactly3 : List (Value × ℚ)

Equations

• EgreEtAl2023.l0_exactly3 = EgreEtAl2023.exactPosterior 3

def EgreEtAl2023.birJoint (n : ℕ) : List ((Value × Tolerance) × ℚ)

Equations

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

def EgreEtAl2023.tolerancePosterior (n : ℕ) : List (Tolerance × ℚ)

Tolerance posterior: marginalize BIR joint over values.

Equations

• EgreEtAl2023.tolerancePosterior n = EgreEtAl2023.marginalize✝ (EgreEtAl2023.birJoint n) Prod.snd

def EgreEtAl2023.l0_tolerance_around3 : List (Tolerance × ℚ)

Equations

• EgreEtAl2023.l0_tolerance_around3 = EgreEtAl2023.tolerancePosterior 3

def EgreEtAl2023.wirPosterior (n : ℕ) : List (Value × ℚ)

WIR: L(x=k | around n) = Σ_i P(x=k | x ∈ [n-i,n+i]) × P(y=i). Tolerance y ranges over {0,...,n} (Section 3.2.2).

Equations

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

def EgreEtAl2023.wir_around3 : List (Value × ℚ)

Equations

• EgreEtAl2023.wir_around3 = EgreEtAl2023.wirPosterior 3

theorem EgreEtAl2023.bir_triangular_shape : EgreEtAl2023.getScore✝ l0_around3 Value.v3 > EgreEtAl2023.getScore✝ l0_around3 Value.v2 ∧ EgreEtAl2023.getScore✝ l0_around3 Value.v2 > EgreEtAl2023.getScore✝ l0_around3 Value.v1 ∧ EgreEtAl2023.getScore✝ l0_around3 Value.v1 > EgreEtAl2023.getScore✝ l0_around3 Value.v0

BIR produces triangular posterior: v3 > v2 > v1 > v0.

theorem EgreEtAl2023.bir_symmetry : EgreEtAl2023.getScore✝ l0_around3 Value.v2 = EgreEtAl2023.getScore✝ l0_around3 Value.v4 ∧ EgreEtAl2023.getScore✝ l0_around3 Value.v1 = EgreEtAl2023.getScore✝ l0_around3 Value.v5 ∧ EgreEtAl2023.getScore✝ l0_around3 Value.v0 = EgreEtAl2023.getScore✝ l0_around3 Value.v6

BIR posterior is symmetric: P(n+k) = P(n-k).

theorem EgreEtAl2023.ratio_inequality : EgreEtAl2023.getScore✝ l0_around3 Value.v3 / EgreEtAl2023.getScore✝ l0_around3 Value.v1 > 1 ∧ EgreEtAl2023.getScore✝ l0_around3 Value.v3 / EgreEtAl2023.getScore✝ l0_around3 Value.v0 > 1

Ratio Inequality: posterior concentrates more on center than prior. Under uniform prior, reduces to P(v3|around3) / P(v1|around3) > 1.

theorem EgreEtAl2023.around_conveys_shape_between_does_not : EgreEtAl2023.getScore✝ l0_around3 Value.v3 / EgreEtAl2023.getScore✝ l0_around3 Value.v1 > EgreEtAl2023.getScore✝ l0_between1_5 Value.v3 / EgreEtAl2023.getScore✝ l0_between1_5 Value.v1

"Around" conveys shape (peaked); "between" does not (flat). Peak-to-edge ratio: around = 7/4, between = 1.

theorem EgreEtAl2023.around_wider_support : EgreEtAl2023.getScore✝ l0_around3 Value.v0 > 0 ∧ EgreEtAl2023.getScore✝ l0_between2_4 Value.v0 = 0

"Around" has wider support than narrow "between".

theorem EgreEtAl2023.around_covers_nearby : EgreEtAl2023.getScore✝ l0_around3 Value.v2 > 0 ∧ EgreEtAl2023.getScore✝ l0_around3 Value.v4 > 0 ∧ EgreEtAl2023.getScore✝ l0_exactly3 Value.v2 = 0

"Around 3" covers nearby values; "exactly 3" does not.

theorem EgreEtAl2023.between_is_uniform : EgreEtAl2023.getScore✝ l0_between1_5 Value.v1 = EgreEtAl2023.getScore✝ l0_between1_5 Value.v3 ∧ EgreEtAl2023.getScore✝ l0_between1_5 Value.v3 = EgreEtAl2023.getScore✝ l0_between1_5 Value.v5

"Between 1 5" assigns uniform probability across its interval.

theorem EgreEtAl2023.tolerance_distribution : EgreEtAl2023.getScore✝ l0_tolerance_around3 Tolerance.y3 > EgreEtAl2023.getScore✝ l0_tolerance_around3 Tolerance.y0

BIR joint marginalizes to favor large tolerances (more states compatible). With y ∈ {0,...,3}, y3 has 7 compatible values while y0 has 1.

theorem EgreEtAl2023.sorites_adjacent_similar : have p3 := EgreEtAl2023.getScore✝ l0_around3 Value.v3; have p2 := EgreEtAl2023.getScore✝ l0_around3 Value.v2; have p1 := EgreEtAl2023.getScore✝ l0_around3 Value.v1; p2 > p3 * 1 / 2 ∧ p1 > p2 * 1 / 2

Adjacent values have similar BIR probabilities (each step ≥ 50%).

theorem EgreEtAl2023.sorites_cumulative : EgreEtAl2023.getScore✝ l0_around3 Value.v3 > EgreEtAl2023.getScore✝ l0_around3 Value.v0

Cumulative sorites effect: P(v3) > P(v0).

inductive EgreEtAl2023.Utt : Type

Message alternatives for the RSA model.

• around3 : Utt
• between0_6 : Utt
• between1_5 : Utt
• between2_4 : Utt
• exactly3 : Utt

@[implicit_reducible]

instance EgreEtAl2023.instReprUtt : Repr Utt

Equations

• EgreEtAl2023.instReprUtt = { reprPrec := EgreEtAl2023.instReprUtt.repr }

def EgreEtAl2023.instReprUtt.repr : Utt → ℕ → Std.Format

Equations

• EgreEtAl2023.instReprUtt.repr EgreEtAl2023.Utt.around3 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "EgreEtAl2023.Utt.around3")).group prec✝
• EgreEtAl2023.instReprUtt.repr EgreEtAl2023.Utt.between0_6 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "EgreEtAl2023.Utt.between0_6")).group prec✝
• EgreEtAl2023.instReprUtt.repr EgreEtAl2023.Utt.between1_5 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "EgreEtAl2023.Utt.between1_5")).group prec✝
• EgreEtAl2023.instReprUtt.repr EgreEtAl2023.Utt.between2_4 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "EgreEtAl2023.Utt.between2_4")).group prec✝
• EgreEtAl2023.instReprUtt.repr EgreEtAl2023.Utt.exactly3 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "EgreEtAl2023.Utt.exactly3")).group prec✝

@[implicit_reducible]

instance EgreEtAl2023.instDecidableEqUtt : DecidableEq Utt

Equations

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

@[implicit_reducible]

instance EgreEtAl2023.instFintypeUtt : Fintype Utt

Equations

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

def EgreEtAl2023.aroundWeight : Value → ℕ

Unnormalized BIR weights for "around 3".

Proportional to birWeight 3 w: integer counts of valid tolerances y ∈ {0,...,3} satisfying |3 - w| ≤ y. After L0 normalization (÷ 16), gives the triangular BIR posterior [1/16, 2/16, 3/16, 4/16, 3/16, 2/16, 1/16].

Equations

• EgreEtAl2023.aroundWeight EgreEtAl2023.Value.v0 = 1
• EgreEtAl2023.aroundWeight EgreEtAl2023.Value.v1 = 2
• EgreEtAl2023.aroundWeight EgreEtAl2023.Value.v2 = 3
• EgreEtAl2023.aroundWeight EgreEtAl2023.Value.v3 = 4
• EgreEtAl2023.aroundWeight EgreEtAl2023.Value.v4 = 3
• EgreEtAl2023.aroundWeight EgreEtAl2023.Value.v5 = 2
• EgreEtAl2023.aroundWeight EgreEtAl2023.Value.v6 = 1

noncomputable def EgreEtAl2023.speakerBeliefR (observed w : Value) : ℝ

Speaker belief peaked at observed value (unnormalized).

Weight 2 at center, 1 at ±1, 0 elsewhere. Unnormalized weights preserve S1 ranking because exp is monotone and the normalization constant is independent of u (the inlined klFinite_eq_negEntropy_sub_crossEntropy algebra).

Equations

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

noncomputable def EgreEtAl2023.cfg : RSA.RSAConfig Utt Value

RSA model for imprecision: BIR + KL-divergence speaker.

L0 = BIR (Bayesian Interpretation Rule): graded meaning gives the triangular "around" posterior after normalization, matching birWeight.

S1 = KL speaker: the speaker with peaked beliefs chooses the message whose L0 posterior best matches those beliefs, measured by expected log-likelihood (= negative KL divergence up to constant entropy, the inlined klFinite_eq_negEntropy_sub_crossEntropy algebra).

Equations

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

theorem EgreEtAl2023.s1_prefers_around_peaked : cfg.S1 () Value.v3 Utt.around3 > cfg.S1 () Value.v3 Utt.between0_6

Speaker with peaked belief at v3 prefers "around 3" over "between 0 6".

"Around 3" produces a triangular L0 posterior peaked at v3, which better matches the speaker's peaked belief via KL divergence. "Between 0 6" produces a flat L0 posterior that wastes probability mass on values far from v3.

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

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

Equations

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

def 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

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

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

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

Equations

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

theorem 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.

theorem 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.

def 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.

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

Equations

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

noncomputable def 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).

In nats; multiply by 1 / Real.log 2 to convert to bits.

Equations

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

noncomputable def EgreEtAl2023.U1 {W M I : Type} (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, in nats. 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.

theorem EgreEtAl2023.no_quality_implies_S1_zero {W M I : Type} [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

theorem 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.

theorem 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, α).

theorem 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.

theorem EgreEtAl2023.wir_peaked_at_center : EgreEtAl2023.getScore✝ wir_around3 Value.v3 > EgreEtAl2023.getScore✝ wir_around3 Value.v1

theorem EgreEtAl2023.bir_wir_differ : EgreEtAl2023.getScore✝ l0_around3 Value.v2 ≠ EgreEtAl2023.getScore✝ wir_around3 Value.v2

BIR and WIR differ quantitatively under uniform priors.

def EgreEtAl2023.obs_peaked : Value → ℚ

Equations

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

def EgreEtAl2023.obs_flat : Value → ℚ

Equations

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

theorem EgreEtAl2023.obs_same_support (x : Value) : obs_peaked x > 0 ↔ obs_flat x > 0

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

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

The if pw > 0 ∧ lw > 0 guard is unneeded: mathlib's Real.log 0 = 0 convention makes pw · Real.log lw = 0 whenever either factor is 0.

Equations

• EgreEtAl2023.U_std l0_scores obs = (List.map (fun (w : EgreEtAl2023.Value) => ↑(obs w) * Real.log ↑(l0_scores w)) EgreEtAl2023.allValues).sum

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

C.2: Bergen utility U_bergen(m,o) = Σ_w P(w|o) · log L(w|o), in nats. 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

• EgreEtAl2023.U_bergen l0_scores obs = (List.map (fun (w : EgreEtAl2023.Value) => ↑(obs w) * Real.log ↑(l0_scores w)) EgreEtAl2023.allValues).sum

def EgreEtAl2023.l0_around3_fn : Value → ℚ

Equations

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

theorem 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.

Algebraic content: with obs_peaked = (1/6, 1/6, 1/3, 1/6, 1/6) and obs_flat = (1/5, 1/5, 1/5, 1/5, 1/5) over (v1, v2, v3, v4, v5), and the triangular L0 (1/8, 3/16, 1/4, 3/16, 1/8),

U_peaked - U_flat = (1/15) · (2·log(1/4) - log(1/8) - log(3/16)) = (1/15) · log((1/4)² / ((1/8)·(3/16))) = (1/15) · log(8/3) > 0.

def 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

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

theorem EgreEtAl2023.same_utility_under_uniform_l0 : U_bergen l0_between_fn obs_peaked = U_bergen l0_between_fn obs_flat

Under a uniform L0 over the shared support {v1..v5}, both observations yield the same utility Real.log (1/5). This works because: (a) On the support, Real.log lw = Real.log (1/5) is constant. (b) Off the support, Real.log 0 = 0 (mathlib convention) zeros the term. (c) Both obs_peaked and obs_flat sum to 1 over {v1..v5}.

theorem 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.

theorem EgreEtAl2023.l0_preserves_bir_ranking : EgreEtAl2023.getScore✝ l0_around3 Value.v3 > EgreEtAl2023.getScore✝ l0_around3 Value.v2 ∧ EgreEtAl2023.getScore✝ l0_around3 Value.v2 > EgreEtAl2023.getScore✝ l0_around3 Value.v1 ∧ EgreEtAl2023.getScore✝ l0_around3 Value.v1 > EgreEtAl2023.getScore✝ l0_around3 Value.v0

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

theorem EgreEtAl2023.bir_matches_closed_form (v : Value) : EgreEtAl2023.getScore✝ l0_around3 v = birClosedForm 3 v.toNat

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

theorem EgreEtAl2023.closed_form_matches_phenomena_center : birClosedForm 20 20 = closedForm_center.expectedProb

Closed form matches Phenomena datum for center: P(x=20 | around 20) = 21/441.

theorem EgreEtAl2023.closed_form_matches_phenomena_offset5 : birClosedForm 20 15 = closedForm_offset5.expectedProb

Closed form matches Phenomena datum for offset: P(x=15 | around 20) = 16/441.