Documentation

Studies.CremersWilcoxSpector2023

Exhaustivity and anti-exhaustivity in the Rational Speech Act framework #

A listener who hears A where A and B was available infers that B is false. In the baseline Rational Speech Act model a prior biased towards the world of both A and B reverses the inference: the listener is anti-exhaustive exactly when the log odds of the prior exceed the cost disadvantage of A and not B over A and B, whatever the rationality. Lexical uncertainty over free strengthenings and the wonky-world models stay anti-exhaustive for suitable priors, while grammatical lexical uncertainty, the lexical-intentions speaker and the supervaluationist speaker keep the posterior of both below the prior whenever A and B costs no more than A and not B. The experiment finds no anti-exhaustivity.

We state each model on the substrate's kernel face and prove the paper's conditions on reals for an arbitrary prior, rationality and costs. The lexical-uncertainty models and the Bayesian wonky model are given in the paper both as a joint posterior over worlds and a latent and as the inverse of the speaker averaged over the latent, and the two agree (luJointListener_fst, bayesWonkyJointListener_fst).

TODO #

The non-Bayesian wonky model's limits in the prior and the Bayesian wonky model's wonkiness threshold are not derived.

References #

Worlds, messages and interpretations #

inductive CremersWilcoxSpector2023.World :

In one world only A is true, in the other both A and B are.

wa : World
wab : World

Instances For

@[instance_reducible]

instance CremersWilcoxSpector2023.instDecidableEqWorld :

DecidableEq World

Equations

CremersWilcoxSpector2023.instDecidableEqWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance CremersWilcoxSpector2023.instFintypeWorld :

Fintype World

Equations

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

instance CremersWilcoxSpector2023.instNonemptyWorld :

Nonempty World

@[instance_reducible]

instance CremersWilcoxSpector2023.instMeasurableSpaceWorld :

MeasurableSpace World

Equations

CremersWilcoxSpector2023.instMeasurableSpaceWorld = ⊤

inductive CremersWilcoxSpector2023.Message :

The three messages are A, A and B and A and not B.

a : Message
aAndB : Message
aAndNotB : Message

Instances For

@[instance_reducible]

instance CremersWilcoxSpector2023.instDecidableEqMessage :

DecidableEq Message

Equations

CremersWilcoxSpector2023.instDecidableEqMessage x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance CremersWilcoxSpector2023.instFintypeMessage :

Fintype Message

Equations

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

instance CremersWilcoxSpector2023.instNonemptyMessage :

Nonempty Message

@[instance_reducible]

instance CremersWilcoxSpector2023.instMeasurableSpaceMessage :

MeasurableSpace Message

Equations

CremersWilcoxSpector2023.instMeasurableSpaceMessage = ⊤

def CremersWilcoxSpector2023.truth :

Message → World → Bool

The literal meaning of each message.

Equations

Instances For

def CremersWilcoxSpector2023.alternatives :

Message → List (World → Bool)

A has the scale-mate A and B as its alternative.

Equations

One or more equations did not get rendered due to their size.
CremersWilcoxSpector2023.alternatives x✝ = [CremersWilcoxSpector2023.truth x✝]

Instances For

def CremersWilcoxSpector2023.exh (u : Message) (w : World) :

Bool

The exhaustified meaning, by innocent exclusion of the alternatives.

Equations

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

Instances For

theorem CremersWilcoxSpector2023.exh_a :

exh Message.a = truth Message.aAndNotB

Exhaustification reads A as A and not B.

theorem CremersWilcoxSpector2023.exh_aAndB :

exh Message.aAndB = truth Message.aAndB

A and B has no stronger alternative.

theorem CremersWilcoxSpector2023.exh_aAndNotB :

exh Message.aAndNotB = truth Message.aAndNotB

A and not B has no stronger alternative.

structure CremersWilcoxSpector2023.Meaning :

An interpretation function under which every message is true somewhere and every world is described by some message, so that the literal listener and the speaker are defined.

sat : Message → World → Bool
The truth value of a message at a world.
exists_world (u : Message) : ∃ (w : World), self.sat u w = true
Every message is true somewhere.
exists_message (w : World) : ∃ (u : Message), self.sat u w = true
Every world is described by some message.

Instances For

def CremersWilcoxSpector2023.Meaning.extension (m : Meaning) (u : Message) :

The extension of a message.

Equations

m.extension u = {w : CremersWilcoxSpector2023.World | m.sat u w = true}

Instances For

theorem CremersWilcoxSpector2023.Meaning.mem_extension (m : Meaning) {u : Message} {w : World} :

w ∈ m.extension u ↔ m.sat u w = true

theorem CremersWilcoxSpector2023.Meaning.extension_eq_univ (m : Meaning) {u : Message} (h : ∀ (w : World), m.sat u w = true) :

m.extension u = Set.univ

A message true everywhere has the full extension.

theorem CremersWilcoxSpector2023.Meaning.extension_eq_singleton (m : Meaning) {u : Message} {w : World} (h : ∀ (w' : World), m.sat u w' = true ↔ w' = w) :

m.extension u = {w}

A message true at one world only has that world as its extension.

def CremersWilcoxSpector2023.literal :

The literal interpretation.

Equations

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

Instances For

def CremersWilcoxSpector2023.exhaustified :

The exhaustified interpretation, A read as A and not B.

Equations

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

Instances For

def CremersWilcoxSpector2023.antiExhaustive :

The anti-exhaustive interpretation of the free lexical-uncertainty model, A read as A and B.

Equations

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

Instances For

inductive CremersWilcoxSpector2023.Interpretation :

The two grammatical interpretations, literal and exhaustified.

lit : Interpretation
exh : Interpretation

Instances For

@[instance_reducible]

instance CremersWilcoxSpector2023.instDecidableEqInterpretation :

DecidableEq Interpretation

Equations

CremersWilcoxSpector2023.instDecidableEqInterpretation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance CremersWilcoxSpector2023.instFintypeInterpretation :

Fintype Interpretation

Equations

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

instance CremersWilcoxSpector2023.instNonemptyInterpretation :

Nonempty Interpretation

@[instance_reducible]

instance CremersWilcoxSpector2023.instMeasurableSpaceInterpretation :

MeasurableSpace Interpretation

Equations

CremersWilcoxSpector2023.instMeasurableSpaceInterpretation = ⊤

def CremersWilcoxSpector2023.Interpretation.meaning :

Interpretation → Meaning

The meaning of a grammatical interpretation.

Equations

Instances For

inductive CremersWilcoxSpector2023.FreeInterpretation :

The three interpretations of the free lexical-uncertainty model.

Instances For

@[instance_reducible]

instance CremersWilcoxSpector2023.instDecidableEqFreeInterpretation :

DecidableEq FreeInterpretation

Equations

CremersWilcoxSpector2023.instDecidableEqFreeInterpretation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance CremersWilcoxSpector2023.instFintypeFreeInterpretation :

Fintype FreeInterpretation

Equations

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

instance CremersWilcoxSpector2023.instNonemptyFreeInterpretation :

Nonempty FreeInterpretation

@[instance_reducible]

instance CremersWilcoxSpector2023.instMeasurableSpaceFreeInterpretation :

MeasurableSpace FreeInterpretation

Equations

CremersWilcoxSpector2023.instMeasurableSpaceFreeInterpretation = ⊤

def CremersWilcoxSpector2023.FreeInterpretation.meaning :

FreeInterpretation → Meaning

The meaning of a free interpretation.

Equations

Instances For

inductive CremersWilcoxSpector2023.Background :

The wonky-world listener considers two backgrounds, in which the speaker assumes a uniform prior or the measured one.

wonky : Background
measured : Background

Instances For

@[instance_reducible]

instance CremersWilcoxSpector2023.instDecidableEqBackground :

DecidableEq Background

Equations

CremersWilcoxSpector2023.instDecidableEqBackground x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance CremersWilcoxSpector2023.instFintypeBackground :

Fintype Background

Equations

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

instance CremersWilcoxSpector2023.instNonemptyBackground :

Nonempty Background

@[instance_reducible]

instance CremersWilcoxSpector2023.instMeasurableSpaceBackground :

MeasurableSpace Background

Equations

CremersWilcoxSpector2023.instMeasurableSpaceBackground = ⊤

inductive CremersWilcoxSpector2023.QUD :

The question under discussion asks whether A holds, which the two worlds answer alike, or which world obtains.

coarse : QUD
fine : QUD

Instances For

@[instance_reducible]

instance CremersWilcoxSpector2023.instDecidableEqQUD :

DecidableEq QUD

Equations

CremersWilcoxSpector2023.instDecidableEqQUD x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance CremersWilcoxSpector2023.instFintypeQUD :

Fintype QUD

Equations

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

instance CremersWilcoxSpector2023.instNonemptyQUD :

Nonempty QUD

@[instance_reducible]

instance CremersWilcoxSpector2023.instMeasurableSpaceQUD :

MeasurableSpace QUD

Equations

CremersWilcoxSpector2023.instMeasurableSpaceQUD = ⊤

theorem CremersWilcoxSpector2023.sum_world {β : Type u_1} [AddCommMonoid β] (f : World → β) :

∑ w : World, f w = f World.wa + f World.wab

A sum over the two worlds.

theorem CremersWilcoxSpector2023.sum_message {β : Type u_1} [AddCommMonoid β] (f : Message → β) :

∑ u : Message, f u = f Message.a + f Message.aAndB + f Message.aAndNotB

A sum over the three messages.

theorem CremersWilcoxSpector2023.sum_interpretation {β : Type u_1} [AddCommMonoid β] (f : Interpretation → β) :

∑ i : Interpretation, f i = f Interpretation.lit + f Interpretation.exh

A sum over the two grammatical interpretations.

theorem CremersWilcoxSpector2023.sum_freeInterpretation {β : Type u_1} [AddCommMonoid β] (f : FreeInterpretation → β) :

∑ i : FreeInterpretation, f i = f FreeInterpretation.lit + f FreeInterpretation.exh + f FreeInterpretation.antiExh

A sum over the three free interpretations.

theorem CremersWilcoxSpector2023.sum_background {β : Type u_1} [AddCommMonoid β] (f : Background → β) :

∑ b : Background, f b = f Background.wonky + f Background.measured

A sum over the two backgrounds.

theorem CremersWilcoxSpector2023.sum_qud {β : Type u_1} [AddCommMonoid β] (f : QUD → β) :

∑ q : QUD, f q = f QUD.coarse + f QUD.fine

A sum over the two questions.

Priors and parameters #

structure CremersWilcoxSpector2023.Setting :

A model is fixed by the prior probability of both A and B, the rationality, and the costs of the two conjunctions, A itself costing nothing.

p : ℝ
The prior probability of the world where both A and B hold.
lam : ℝ
The rationality, the paper's λ.
cAndB : ℝ
The cost of A and B.
cAndNotB : ℝ
The cost of A and not B.
p_pos : 0 < self.p
The world of both has positive prior probability.
p_lt_one : self.p < 1
The world of A alone has positive prior probability.
lam_pos : 0 < self.lam
The rationality is positive.

Instances For

def CremersWilcoxSpector2023.Setting.cost (s : Setting) :

Message → ℝ

The cost of a message.

Equations

s.cost CremersWilcoxSpector2023.Message.a = 0
s.cost CremersWilcoxSpector2023.Message.aAndB = s.cAndB
s.cost CremersWilcoxSpector2023.Message.aAndNotB = s.cAndNotB

Instances For

@[reducible, inline]

noncomputable abbrev CremersWilcoxSpector2023.Setting.costFactor (s : Setting) (u : Message) :

ENNReal

The cost factor of a message is the exponential of its cost scaled by the rationality.

Equations

s.costFactor u = ENNReal.ofReal (Real.exp (-(s.lam * s.cost u)))

Instances For

theorem CremersWilcoxSpector2023.Setting.costFactor_ne_zero (s : Setting) (u : Message) :

s.costFactor u ≠ 0

theorem CremersWilcoxSpector2023.Setting.costFactor_ne_top (s : Setting) (u : Message) :

s.costFactor u ≠ ⊤

theorem CremersWilcoxSpector2023.Setting.costFactor_toReal (s : Setting) (u : Message) :

(s.costFactor u).toReal = Real.exp (-(s.lam * s.cost u))

noncomputable def CremersWilcoxSpector2023.Setting.logistic (s : Setting) (x : ℝ) :

ℝ

The paper's f_λ is the logistic function with rate the rationality.

Equations

s.logistic x = (s.lam * x).sigmoid

Instances For

theorem CremersWilcoxSpector2023.Setting.logistic_nonneg (s : Setting) (x : ℝ) :

0 ≤ s.logistic x

theorem CremersWilcoxSpector2023.Setting.logistic_lt_iff (s : Setting) {x y : ℝ} :

s.logistic x < s.logistic y ↔ x < y

theorem CremersWilcoxSpector2023.Setting.logistic_lt (s : Setting) {x y : ℝ} (h : x < y) :

s.logistic x < s.logistic y

noncomputable def CremersWilcoxSpector2023.Setting.priorWeight (s : Setting) :

World → ENNReal

The weight of a world under the measured prior.

Equations

s.priorWeight CremersWilcoxSpector2023.World.wa = ENNReal.ofReal (1 - s.p)
s.priorWeight CremersWilcoxSpector2023.World.wab = ENNReal.ofReal s.p

Instances For

noncomputable def CremersWilcoxSpector2023.Setting.prior (s : Setting) :

MeasureTheory.Measure World

The measured prior over the two worlds.

Equations

s.prior = ∑ w : CremersWilcoxSpector2023.World, s.priorWeight w • MeasureTheory.Measure.dirac w

Instances For

theorem CremersWilcoxSpector2023.Setting.prior_apply_singleton (s : Setting) (w : World) :

s.prior {w} = s.priorWeight w

theorem CremersWilcoxSpector2023.Setting.prior_wa (s : Setting) :

s.prior {World.wa} = ENNReal.ofReal (1 - s.p)

The prior of the world of A alone.

theorem CremersWilcoxSpector2023.Setting.prior_wab (s : Setting) :

s.prior {World.wab} = ENNReal.ofReal s.p

The prior of the world of both.

instance CremersWilcoxSpector2023.Setting.instIsProbabilityMeasureWorldPrior (s : Setting) :

MeasureTheory.IsProbabilityMeasure s.prior

theorem CremersWilcoxSpector2023.Setting.prior_ne_zero (s : Setting) (w : World) :

s.prior {w} ≠ 0

The prior is positive on both worlds.

theorem CremersWilcoxSpector2023.Setting.prior_support (s : Setting) (w : World) :

s.prior {w} ≠ 0 → w = World.wab ∨ w = World.wa

The prior is carried by the two worlds.

theorem CremersWilcoxSpector2023.Setting.prior_real_wa (s : Setting) :

s.prior.real {World.wa} = 1 - s.p

The prior of the world of A alone, as a real.

theorem CremersWilcoxSpector2023.Setting.prior_real_wab (s : Setting) :

s.prior.real {World.wab} = s.p

The prior of the world of both, as a real.

noncomputable def CremersWilcoxSpector2023.wonkyPrior :

MeasureTheory.Measure World

The wonky prior is uniform over the two worlds.

Equations

CremersWilcoxSpector2023.wonkyPrior = ProbabilityTheory.uniformOn Set.univ

Instances For

instance CremersWilcoxSpector2023.instIsProbabilityMeasureWorldWonkyPrior :

MeasureTheory.IsProbabilityMeasure wonkyPrior

theorem CremersWilcoxSpector2023.wonkyPrior_apply_singleton (w : World) :

wonkyPrior {w} = 2⁻¹

The wonky prior gives each world a half.

theorem CremersWilcoxSpector2023.wonkyPrior_ne_zero (w : World) :

wonkyPrior {w} ≠ 0

The wonky prior is positive on both worlds.

theorem CremersWilcoxSpector2023.wonkyPrior_real_singleton (w : World) :

wonkyPrior.real {w} = 2⁻¹

The wonky prior of a world, as a real.

The literal listener and the speaker under an interpretation (eqs. 1 to 3) #

noncomputable def CremersWilcoxSpector2023.L0 (P : MeasureTheory.Measure World) (m : Meaning) :

ProbabilityTheory.Kernel Message World

The literal listener conditions the prior on the message's extension (eq. 1).

Equations

CremersWilcoxSpector2023.L0 P m = RSA.listener P (RSA.truthful m.extension)

Instances For

instance CremersWilcoxSpector2023.instIsFiniteKernelMessageWorldL0 (P : MeasureTheory.Measure World) (m : Meaning) :

ProbabilityTheory.IsFiniteKernel (L0 P m)

theorem CremersWilcoxSpector2023.L0_ne_top (P : MeasureTheory.Measure World) (m : Meaning) (u : Message) (w : World) :

((L0 P m) u) {w} ≠ ⊤

theorem CremersWilcoxSpector2023.L0_eq_zero (P : MeasureTheory.Measure World) (m : Meaning) {u : Message} {w : World} (h : m.sat u w = false) :

((L0 P m) u) {w} = 0

A message false at a world gets no mass there.

theorem CremersWilcoxSpector2023.L0_literal_a (P : MeasureTheory.Measure World) [MeasureTheory.IsProbabilityMeasure P] (w : World) :

((L0 P literal) Message.a) {w} = P {w}

The tautology A leaves the prior unchanged.

noncomputable def CremersWilcoxSpector2023.speaker (P : MeasureTheory.Measure World) (m : Meaning) (s : Setting) :

ProbabilityTheory.Kernel World Message

The speaker is the softmax of the literal listener's log probability less the cost, scaled by the rationality (eqs. 2 and 3).

Equations

CremersWilcoxSpector2023.speaker P m s = RSA.speaker s.lam s.cost (⇑(CremersWilcoxSpector2023.L0 P m)) MeasureTheory.Measure.dirac

Instances For

instance CremersWilcoxSpector2023.instIsFiniteKernelWorldMessageSpeaker (P : MeasureTheory.Measure World) (m : Meaning) (s : Setting) :

ProbabilityTheory.IsFiniteKernel (speaker P m s)

theorem CremersWilcoxSpector2023.weight_ne_top (P : MeasureTheory.Measure World) (m : Meaning) (s : Setting) (u : Message) (w : World) :

((L0 P m) u) {w} ^ s.lam * s.costFactor u ≠ ⊤

The weight of a message is finite.

theorem CremersWilcoxSpector2023.weight_eq_zero (P : MeasureTheory.Measure World) (m : Meaning) (s : Setting) {u : Message} {w : World} (h : m.sat u w = false) :

((L0 P m) u) {w} ^ s.lam * s.costFactor u = 0

A message false at a world has no weight there.

theorem CremersWilcoxSpector2023.speaker_eq_zero (P : MeasureTheory.Measure World) (m : Meaning) (s : Setting) {u : Message} {w : World} (h : m.sat u w = false) :

((speaker P m s) w) {u} = 0

A message false at a world is never used there.

theorem CremersWilcoxSpector2023.L0_ne_zero (P : MeasureTheory.Measure World) (hP : ∀ (w : World), P {w} ≠ 0) (m : Meaning) [MeasureTheory.IsFiniteMeasure P] {u : Message} {w : World} (h : m.sat u w = true) :

((L0 P m) u) {w} ≠ 0

A message true at a world has positive mass there.

theorem CremersWilcoxSpector2023.L0_eq_one (P : MeasureTheory.Measure World) (hP : ∀ (w : World), P {w} ≠ 0) (m : Meaning) [MeasureTheory.IsFiniteMeasure P] {u : Message} {w : World} (h : ∀ (w' : World), m.sat u w' = true ↔ w' = w) :

((L0 P m) u) {w} = 1

A message true at one world only puts all its mass there.

theorem CremersWilcoxSpector2023.L0_apply_univ (P : MeasureTheory.Measure World) (hP : ∀ (w : World), P {w} ≠ 0) (m : Meaning) [MeasureTheory.IsFiniteMeasure P] (u : Message) :

((L0 P m) u) Set.univ = 1

The literal listener is a probability measure.

theorem CremersWilcoxSpector2023.weight_toReal (P : MeasureTheory.Measure World) (hP : ∀ (w : World), P {w} ≠ 0) (m : Meaning) (s : Setting) [MeasureTheory.IsFiniteMeasure P] {u : Message} {w : World} (h : m.sat u w = true) :

(((L0 P m) u) {w} ^ s.lam * s.costFactor u).toReal = Real.exp (s.lam * (Real.log (((L0 P m) u) {w}).toReal - s.cost u))

On reals, the weight of a message true at a world is the exponential of the paper's scaled utility.

theorem CremersWilcoxSpector2023.speaker_ne_zero (P : MeasureTheory.Measure World) (hP : ∀ (w : World), P {w} ≠ 0) (m : Meaning) (s : Setting) [MeasureTheory.IsFiniteMeasure P] {u : Message} {w : World} (h : m.sat u w = true) :

((speaker P m s) w) {u} ≠ 0

A message true at a world is used there.

theorem CremersWilcoxSpector2023.speaker_real_singleton_lt_iff (P : MeasureTheory.Measure World) (hP : ∀ (w : World), P {w} ≠ 0) (m : Meaning) (s : Setting) [MeasureTheory.IsFiniteMeasure P] {u v : Message} {w : World} (hu : m.sat u w = true) (hv : m.sat v w = true) :

((speaker P m s) w).real {u} < ((speaker P m s) w).real {v} ↔ Real.log (((L0 P m) u) {w}).toReal - s.cost u < Real.log (((L0 P m) v) {w}).toReal - s.cost v

Between two messages true at a world, the speaker prefers the one of higher utility.

theorem CremersWilcoxSpector2023.speaker_real_singleton_of_pair (P : MeasureTheory.Measure World) (hP : ∀ (w : World), P {w} ≠ 0) (m : Meaning) (s : Setting) [MeasureTheory.IsFiniteMeasure P] {u v : Message} {w : World} (huv : u ≠ v) (hu : m.sat u w = true) (hv : m.sat v w = true) (hsupp : ∀ (x : Message), m.sat x w = true → x = u ∨ x = v) :

((speaker P m s) w).real {u} = s.logistic (Real.log (((L0 P m) u) {w}).toReal - s.cost u - (Real.log (((L0 P m) v) {w}).toReal - s.cost v))

When exactly two messages are true at a world, the speaker's use of one is the logistic function of the utility difference.

@[reducible, inline]

noncomputable abbrev CremersWilcoxSpector2023.Setting.L0 (s : Setting) (m : Meaning) :

ProbabilityTheory.Kernel Message World

The literal listener with the measured prior.

Equations

s.L0 m = CremersWilcoxSpector2023.L0 s.prior m

Instances For

@[reducible, inline]

noncomputable abbrev CremersWilcoxSpector2023.Setting.speaker (s : Setting) (m : Meaning) :

ProbabilityTheory.Kernel World Message

The speaker with the measured prior in the literal listener.

Equations

s.speaker m = CremersWilcoxSpector2023.speaker s.prior m s

Instances For

Closed forms: the speaker's use of A is a logistic function #

theorem CremersWilcoxSpector2023.speaker_literal_wab_a (P : MeasureTheory.Measure World) [MeasureTheory.IsProbabilityMeasure P] (hP : ∀ (w : World), P {w} ≠ 0) (s : Setting) :

((speaker P literal s) World.wab).real {Message.a} = s.logistic (s.cAndB + Real.log (P.real {World.wab}))

In the world of both, the literal speaker's use of A is the logistic function of the cost of A and B plus the log prior (eq. A.3).

theorem CremersWilcoxSpector2023.speaker_literal_wa_a (P : MeasureTheory.Measure World) [MeasureTheory.IsProbabilityMeasure P] (hP : ∀ (w : World), P {w} ≠ 0) (s : Setting) :

((speaker P literal s) World.wa).real {Message.a} = s.logistic (s.cAndNotB + Real.log (P.real {World.wa}))

In the world of A alone, the use of A is the logistic function of the cost of A and not B plus the log prior (eq. A.2).

theorem CremersWilcoxSpector2023.speaker_exhaustified_wa_a (s : Setting) :

((s.speaker exhaustified) World.wa).real {Message.a} = s.logistic s.cAndNotB

Under the exhaustified interpretation A is as informative as A and not B in the world of A alone, so its use is the logistic function of the latter's cost.

theorem CremersWilcoxSpector2023.speaker_exhaustified_wab_a (s : Setting) :

((s.speaker exhaustified) World.wab).real {Message.a} = 0

Under the exhaustified interpretation A is false in the world of both.

theorem CremersWilcoxSpector2023.speaker_antiExhaustive_wab_a (s : Setting) :

((s.speaker antiExhaustive) World.wab).real {Message.a} = s.logistic s.cAndB

Under the anti-exhaustive interpretation A is as informative as A and B in the world of both.

theorem CremersWilcoxSpector2023.speaker_antiExhaustive_wa_a (s : Setting) :

((s.speaker antiExhaustive) World.wa).real {Message.a} = 0

Under the anti-exhaustive interpretation A is false in the world of A alone.

The baseline model (§3) #

theorem CremersWilcoxSpector2023.baseline_aAndB_lt_a_iff (s : Setting) :

((s.speaker literal) World.wab).real {Message.aAndB} < ((s.speaker literal) World.wab).real {Message.a} ↔ -s.cAndB < Real.log s.p

In the world of both, the speaker prefers A to A and B exactly when the information A and B would add, the negated log prior, does not exceed its cost (6a).

theorem CremersWilcoxSpector2023.baseline_a_lt_aAndNotB_iff (s : Setting) :

((s.speaker literal) World.wa).real {Message.a} < ((s.speaker literal) World.wa).real {Message.aAndNotB} ↔ Real.log (1 - s.p) < -s.cAndNotB

In the world of A alone, the speaker prefers A and not B to A exactly when the negated log prior exceeds its cost (7).

theorem CremersWilcoxSpector2023.comp_speaker_literal_ne_zero (s : Setting) (u : Message) :

(s.prior.bind ⇑(s.speaker literal)) {u} ≠ 0

Every message is used somewhere, so is heard with positive probability.

noncomputable def CremersWilcoxSpector2023.listener (s : Setting) :

ProbabilityTheory.Kernel Message World

The pragmatic listener (eq. 4).

Equations

CremersWilcoxSpector2023.listener s = RSA.listener s.prior ⇑(s.speaker CremersWilcoxSpector2023.literal)

Instances For

theorem CremersWilcoxSpector2023.prior_lt_listener_iff_speaker_lt (s : Setting) :

s.prior.real {World.wab} < ((listener s) Message.a).real {World.wab} ↔ ((s.speaker literal) World.wa).real {Message.a} < ((s.speaker literal) World.wab).real {Message.a}

The listener is anti-exhaustive, the posterior of both A and B exceeding the prior, exactly when the speaker uses A more in the world of both than in the world of A alone (A.4).

theorem CremersWilcoxSpector2023.prior_lt_listener_iff (s : Setting) :

s.prior.real {World.wab} < ((listener s) Message.a).real {World.wab} ↔ s.cAndNotB - s.cAndB < Real.log s.p - Real.log (1 - s.p)

The listener is anti-exhaustive exactly when the log odds of the prior exceed the cost disadvantage of A and not B over A and B, whatever the rationality (6b).

theorem CremersWilcoxSpector2023.prior_lt_listener_iff_of_cost_eq (s : Setting) (hc : s.cAndB = s.cAndNotB) :

s.prior.real {World.wab} < ((listener s) Message.a).real {World.wab} ↔ 1 / 2 < s.p

With equal costs, anti-exhaustivity is a prior biased towards the world of both.

Lexical uncertainty (§4.3) #

The listener holds independent priors over worlds and interpretation functions, infers both from the message and marginalizes on the interpretation, which is to invert the speaker averaged over the interpretations (item 4). The grammatical version (EXH-LU) has the literal and the exhaustified interpretations, and the free version (FREE-LU) adds the anti-exhaustive one.

noncomputable def CremersWilcoxSpector2023.luSpeaker (s : Setting) {I : Type u_1} [Fintype I] [MeasurableSpace I] (meaning : I → Meaning) :

ProbabilityTheory.Kernel World Message

The speaker marginalised over equiprobable interpretation functions (item 4 of the §4.3 model).

Equations

CremersWilcoxSpector2023.luSpeaker s meaning = ∑ i : I, (ProbabilityTheory.uniformOn Set.univ) {i} • s.speaker (meaning i)

Instances For

instance CremersWilcoxSpector2023.instIsFiniteKernelWorldMessageLuSpeaker (s : Setting) {I : Type u_1} [Fintype I] [MeasurableSpace I] (meaning : I → Meaning) :

ProbabilityTheory.IsFiniteKernel (luSpeaker s meaning)

theorem CremersWilcoxSpector2023.luSpeaker_real_singleton (s : Setting) {I : Type u_1} [Fintype I] [MeasurableSpace I] [MeasurableSingletonClass I] (meaning : I → Meaning) (w : World) (u : Message) :

((luSpeaker s meaning) w).real {u} = (↑(Fintype.card I))⁻¹ * ∑ i : I, ((s.speaker (meaning i)) w).real {u}

The averaged speaker on reals.

theorem CremersWilcoxSpector2023.luSpeaker_apply_singleton_ne_zero_iff (s : Setting) {I : Type u_1} [Fintype I] [MeasurableSpace I] [MeasurableSingletonClass I] (meaning : I → Meaning) {w : World} {u : Message} :

((luSpeaker s meaning) w) {u} ≠ 0 ↔ ∃ (i : I), ((s.speaker (meaning i)) w) {u} ≠ 0

A message is used at a world exactly when some interpretation's speaker uses it there.

theorem CremersWilcoxSpector2023.comp_luSpeaker_ne_zero (s : Setting) {I : Type u_1} [Fintype I] [MeasurableSpace I] [MeasurableSingletonClass I] (meaning : I → Meaning) [Nonempty I] (u : Message) :

(s.prior.bind ⇑(luSpeaker s meaning)) {u} ≠ 0

Every message is used somewhere, so is heard with positive probability.

noncomputable def CremersWilcoxSpector2023.luListener (s : Setting) {I : Type u_1} [Fintype I] [MeasurableSpace I] (meaning : I → Meaning) :

ProbabilityTheory.Kernel Message World

The Bayesian inverse of the averaged speaker (item 4 of the §4.3 model).

Equations

CremersWilcoxSpector2023.luListener s meaning = RSA.listener s.prior ⇑(CremersWilcoxSpector2023.luSpeaker s meaning)

Instances For

noncomputable def CremersWilcoxSpector2023.luJointListener (s : Setting) {I : Type u_1} [MeasurableSpace I] (meaning : I → Meaning) :

ProbabilityTheory.Kernel Message (World × I)

The joint posterior over worlds and interpretation functions, under independent priors over the two.

Equations

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

Instances For

theorem CremersWilcoxSpector2023.luJointListener_fst (s : Setting) {I : Type u_1} [Fintype I] [MeasurableSpace I] [MeasurableSingletonClass I] (meaning : I → Meaning) :

(luJointListener s meaning).fst = luListener s meaning

The joint posterior marginalized on interpretation functions is the listener of item 4: the two descriptions of the model in §4.3 agree.

theorem CremersWilcoxSpector2023.luListener_exh_lt_prior (s : Setting) (hc : s.cAndB ≤ s.cAndNotB) :

((luListener s Interpretation.meaning) Message.a).real {World.wab} < s.prior.real {World.wab}

Grammatical lexical uncertainty blocks anti-exhaustivity whenever A and B costs no more than A and not B. The exhaustified interpretation never uses A in the world of both but uses it in the world of A alone more than the literal interpretation uses it in the world of both.

theorem CremersWilcoxSpector2023.prior_lt_luListener_free_iff (s : Setting) :

s.prior.real {World.wab} < ((luListener s FreeInterpretation.meaning) Message.a).real {World.wab} ↔ s.logistic (s.cAndNotB + Real.log (1 - s.p)) + s.logistic s.cAndNotB < s.logistic (s.cAndB + Real.log s.p) + s.logistic s.cAndB

Free lexical uncertainty is anti-exhaustive exactly when the literal and anti-exhaustive uses of A in the world of both outweigh the literal and exhaustified uses in the world of A alone.

theorem CremersWilcoxSpector2023.prior_lt_luListener_free_iff_of_cost_eq (s : Setting) (hc : s.cAndB = s.cAndNotB) :

s.prior.real {World.wab} < ((luListener s FreeInterpretation.meaning) Message.a).real {World.wab} ↔ 1 / 2 < s.p

With equal costs, free lexical uncertainty is anti-exhaustive exactly when the baseline is, namely for a prior biased towards the world of both.

Lexical intentions (§4.4) #

noncomputable def CremersWilcoxSpector2023.liL0 (s : Setting) :

ProbabilityTheory.Kernel (Message × Interpretation) World

The literal listener of a message under a chosen interpretation (item 1 of the §4.4 model).

Equations

CremersWilcoxSpector2023.liL0 s = RSA.listener s.prior (RSA.truthful fun (x : CremersWilcoxSpector2023.Message × CremersWilcoxSpector2023.Interpretation) => x.2.meaning.extension x.1)

Instances For

instance CremersWilcoxSpector2023.instIsFiniteKernelProdMessageInterpretationWorldLiL0 (s : Setting) :

ProbabilityTheory.IsFiniteKernel (liL0 s)

theorem CremersWilcoxSpector2023.liL0_apply (s : Setting) (x : Message × Interpretation) :

(liL0 s) x = (s.L0 x.2.meaning) x.1

noncomputable def CremersWilcoxSpector2023.liSpeaker (s : Setting) :

ProbabilityTheory.Kernel World (Message × Interpretation)

The speaker over messages and interpretations (item 3 of the §4.4 model).

Equations

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

Instances For

instance CremersWilcoxSpector2023.instIsFiniteKernelWorldProdMessageInterpretationLiSpeaker (s : Setting) :

ProbabilityTheory.IsFiniteKernel (liSpeaker s)

noncomputable def CremersWilcoxSpector2023.liMessageSpeaker (s : Setting) :

ProbabilityTheory.Kernel World Message

The speaker's messages, the interpretations marginalised (item 5 of the §4.4 model).

Equations

CremersWilcoxSpector2023.liMessageSpeaker s = (CremersWilcoxSpector2023.liSpeaker s).map Prod.fst

Instances For

instance CremersWilcoxSpector2023.instIsFiniteKernelWorldMessageLiMessageSpeaker (s : Setting) :

ProbabilityTheory.IsFiniteKernel (liMessageSpeaker s)

theorem CremersWilcoxSpector2023.liMessageSpeaker_apply_singleton (s : Setting) (w : World) (u : Message) :

((liMessageSpeaker s) w) {u} = ((liSpeaker s) w) {(u, Interpretation.lit)} + ((liSpeaker s) w) {(u, Interpretation.exh)}

The lexical-intentions speaker's use of a message sums its two interpretations.

theorem CremersWilcoxSpector2023.liMessageSpeaker_real_singleton (s : Setting) (w : World) (u : Message) :

((liMessageSpeaker s) w).real {u} = ((liSpeaker s) w).real {(u, Interpretation.lit)} + ((liSpeaker s) w).real {(u, Interpretation.exh)}

The lexical-intentions speaker's use of a message, on reals.

theorem CremersWilcoxSpector2023.liWeight_ne_top (s : Setting) (w : World) (x : Message × Interpretation) :

((liL0 s) x) {w} ^ s.lam * s.costFactor x.1 ≠ ⊤

The weight of a message under an interpretation is finite.

theorem CremersWilcoxSpector2023.liMessageSpeaker_real_wab_a (s : Setting) :

((liMessageSpeaker s) World.wab).real {Message.a} = Real.exp (s.lam * Real.log s.p) / (Real.exp (s.lam * Real.log s.p) + 2 * Real.exp (-(s.lam * s.cAndB)))

In the world of both, the lexical-intentions speaker uses A, under its literal interpretation only, against the two interpretations of A and B.

theorem CremersWilcoxSpector2023.liMessageSpeaker_real_wa_a (s : Setting) :

((liMessageSpeaker s) World.wa).real {Message.a} = (Real.exp (s.lam * Real.log (1 - s.p)) + 1) / (Real.exp (s.lam * Real.log (1 - s.p)) + 1 + 2 * Real.exp (-(s.lam * s.cAndNotB)))

In the world of A alone, the lexical-intentions speaker uses A under both interpretations, the exhaustified one as informative as A and not B.

theorem CremersWilcoxSpector2023.liSpeaker_ne_zero (s : Setting) {w : World} {u : Message} (hw : literal.sat u w = true) :

((liSpeaker s) w) {(u, Interpretation.lit)} ≠ 0

A message true at a world is used there under its literal interpretation.

theorem CremersWilcoxSpector2023.comp_liMessageSpeaker_ne_zero (s : Setting) (u : Message) :

(s.prior.bind ⇑(liMessageSpeaker s)) {u} ≠ 0

Every message is used somewhere, so is heard with positive probability.

noncomputable def CremersWilcoxSpector2023.liListener (s : Setting) :

ProbabilityTheory.Kernel Message World

The pragmatic listener of the lexical-intentions model (item 6 of the §4.4 model).

Equations

CremersWilcoxSpector2023.liListener s = RSA.listener s.prior ⇑(CremersWilcoxSpector2023.liMessageSpeaker s)

Instances For

theorem CremersWilcoxSpector2023.liListener_lt_prior (s : Setting) (hc : s.cAndB ≤ s.cAndNotB) :

((liListener s) Message.a).real {World.wab} < s.prior.real {World.wab}

The lexical-intentions model blocks anti-exhaustivity whenever A and B costs no more than A and not B, since A is never likelier in the world of both than in the world of A alone.

The supervaluationist model (§4.2) #

def CremersWilcoxSpector2023.QUD.cell :

QUD → World → Set World

The coarse question puts both worlds in one cell, and the fine one distinguishes them.

Equations

CremersWilcoxSpector2023.QUD.coarse.cell x✝ = Set.univ
CremersWilcoxSpector2023.QUD.fine.cell x✝ = {x✝}

Instances For

noncomputable def CremersWilcoxSpector2023.cell (s : Setting) (i : Interpretation) (q : QUD) (u : Message) (w : World) :

ENNReal

The literal listener's mass, under an interpretation, on the cell of a world in a question (item 3 of the §4.2 model, conditioned on the question).

Equations

CremersWilcoxSpector2023.cell s i q u w = ((s.L0 i.meaning) u) (q.cell w)

Instances For

theorem CremersWilcoxSpector2023.cell_coarse (s : Setting) (i : Interpretation) (u : Message) (w : World) :

cell s i QUD.coarse u w = 1

The coarse question has one cell, which carries all the mass.

theorem CremersWilcoxSpector2023.cell_fine (s : Setting) (i : Interpretation) (u : Message) (w : World) :

cell s i QUD.fine u w = ((s.L0 i.meaning) u) {w}

The fine question's cells are the worlds.

noncomputable def CremersWilcoxSpector2023.svWeight (s : Setting) (x : World × QUD) (u : Message) :

ENNReal

The supervaluationist weight is the geometric mean over the two interpretations, taken equiprobable, of the literal listener's mass on the cell, raised to the rationality, times the cost factor. The prior of the question, common to every message, is left out (item 4 of the §4.2 model).

Equations

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

Instances For

theorem CremersWilcoxSpector2023.svWeight_ne_top (s : Setting) (x : World × QUD) (u : Message) :

svWeight s x u ≠ ⊤

theorem CremersWilcoxSpector2023.svWeight_fine_ne_zero (s : Setting) {w : World} {u : Message} (hl : truth u w = true) (he : exh u w = true) :

svWeight s (w, QUD.fine) u ≠ 0

Under the fine question a message true at a world under both interpretations has positive weight there.

noncomputable def CremersWilcoxSpector2023.svSpeaker (s : Setting) :

ProbabilityTheory.Kernel (World × QUD) Message

The supervaluationist speaker, at a world and a question (item 5 of the §4.2 model).

Equations

CremersWilcoxSpector2023.svSpeaker s = ProbabilityTheory.Kernel.ofWeights (CremersWilcoxSpector2023.svWeight s)

Instances For

instance CremersWilcoxSpector2023.instIsFiniteKernelProdWorldQUDMessageSvSpeaker (s : Setting) :

ProbabilityTheory.IsFiniteKernel (svSpeaker s)

theorem CremersWilcoxSpector2023.svSpeaker_coarse (s : Setting) :

(svSpeaker s) (World.wa, QUD.coarse) = (svSpeaker s) (World.wab, QUD.coarse)

Under the coarse question every message is true on the one cell, so the speaker does not depend on the world.

theorem CremersWilcoxSpector2023.svSpeaker_wab_fine_a (s : Setting) :

((svSpeaker s) (World.wab, QUD.fine)) {Message.a} = 0

Under the fine question the exhaustified A is false in the world of both, so the speaker never uses it.

theorem CremersWilcoxSpector2023.svSpeaker_real_wab_fine_a (s : Setting) :

((svSpeaker s) (World.wab, QUD.fine)).real {Message.a} = 0

theorem CremersWilcoxSpector2023.svSpeaker_fine_ne_zero (s : Setting) {w : World} {u : Message} (hl : truth u w = true) (he : exh u w = true) :

((svSpeaker s) (w, QUD.fine)) {u} ≠ 0

Under the fine question a message true at a world under both interpretations is used there.

theorem CremersWilcoxSpector2023.svSpeaker_wab_le_wa (s : Setting) (q : QUD) :

((svSpeaker s) (World.wab, q)) {Message.a} ≤ ((svSpeaker s) (World.wa, q)) {Message.a}

Under either question, A is used no more in the world of both than in the world of A alone (Appendix A.3, the speaker).

noncomputable def CremersWilcoxSpector2023.svJoint (s : Setting) (Q : MeasureTheory.Measure QUD) :

MeasureTheory.Measure (World × QUD)

The joint prior over worlds and questions, independent.

Equations

CremersWilcoxSpector2023.svJoint s Q = s.prior.prod Q

Instances For

theorem CremersWilcoxSpector2023.svJoint_apply_singleton (s : Setting) (Q : MeasureTheory.Measure QUD) (w : World) (q : QUD) :

(svJoint s Q) {(w, q)} = s.prior {w} * Q {q}

theorem CremersWilcoxSpector2023.svJoint_real_singleton (s : Setting) (Q : MeasureTheory.Measure QUD) (w : World) (q : QUD) :

(svJoint s Q).real {(w, q)} = s.prior.real {w} * Q.real {q}

theorem CremersWilcoxSpector2023.exists_truth_and_exh (u : Message) :

∃ (w : World), truth u w = true ∧ exh u w = true

Every message is true somewhere under both grammatical interpretations.

theorem CremersWilcoxSpector2023.comp_svSpeaker_ne_zero (s : Setting) (Q : MeasureTheory.Measure QUD) (hQ : Q {QUD.fine} ≠ 0) (u : Message) :

((svJoint s Q).bind ⇑(svSpeaker s)) {u} ≠ 0

Every message is used somewhere under the fine question, so is heard with positive probability.

instance CremersWilcoxSpector2023.instIsProbabilityMeasureProdWorldQUDSvJoint (s : Setting) (Q : MeasureTheory.Measure QUD) [MeasureTheory.IsProbabilityMeasure Q] :

MeasureTheory.IsProbabilityMeasure (svJoint s Q)

noncomputable def CremersWilcoxSpector2023.svListener (s : Setting) (Q : MeasureTheory.Measure QUD) :

ProbabilityTheory.Kernel Message (World × QUD)

The pragmatic listener, jointly over worlds and questions (item 6 of the §4.2 model).

Equations

CremersWilcoxSpector2023.svListener s Q = RSA.listener (CremersWilcoxSpector2023.svJoint s Q) ⇑(CremersWilcoxSpector2023.svSpeaker s)

Instances For

theorem CremersWilcoxSpector2023.svListener_fst_lt_prior (s : Setting) (Q : MeasureTheory.Measure QUD) (hQ : Q {QUD.fine} ≠ 0) [MeasureTheory.IsProbabilityMeasure Q] :

((svListener s Q) Message.a).fst.real {World.wab} < s.prior.real {World.wab}

The posterior of both A and B falls below its prior, for every prior in the open interval, every prior on the questions that gives the fine one positive probability, and every cost, since the fine question contributes a use of A in the world of A alone and none in the world of both (Appendix A.3, the listener).

The wonky-world models (§4.1) #

noncomputable def CremersWilcoxSpector2023.worldPrior (s : Setting) :

Background → MeasureTheory.Measure World

The speaker's prior is uniform in the wonky background and the measured one otherwise.

Equations

Instances For

instance CremersWilcoxSpector2023.instIsProbabilityMeasureWorldWorldPrior (s : Setting) (b : Background) :

MeasureTheory.IsProbabilityMeasure (worldPrior s b)

theorem CremersWilcoxSpector2023.worldPrior_ne_zero (s : Setting) (b : Background) (w : World) :

(worldPrior s b) {w} ≠ 0

noncomputable def CremersWilcoxSpector2023.bgSpeaker (s : Setting) (b : Background) :

ProbabilityTheory.Kernel World Message

The speaker under a background, with the background's prior in the literal listener (items 1 to 3 of the §4.1 model).

Equations

CremersWilcoxSpector2023.bgSpeaker s b = CremersWilcoxSpector2023.speaker (CremersWilcoxSpector2023.worldPrior s b) CremersWilcoxSpector2023.literal s

Instances For

instance CremersWilcoxSpector2023.instIsFiniteKernelWorldMessageBgSpeaker (s : Setting) (b : Background) :

ProbabilityTheory.IsFiniteKernel (bgSpeaker s b)

theorem CremersWilcoxSpector2023.bgSpeaker_wonky_wab_a (s : Setting) :

((bgSpeaker s Background.wonky) World.wab).real {Message.a} = s.logistic (s.cAndB - Real.log 2)

The wonky speaker uses A in the world of both with the logistic function of the cost of A and B less the log of two.

theorem CremersWilcoxSpector2023.bgSpeaker_wonky_wa_a (s : Setting) :

((bgSpeaker s Background.wonky) World.wa).real {Message.a} = s.logistic (s.cAndNotB - Real.log 2)

The wonky speaker uses A in the world of A alone with the logistic function of the cost of A and not B less the log of two.

theorem CremersWilcoxSpector2023.bgSpeaker_measured_wab_a (s : Setting) :

((bgSpeaker s Background.measured) World.wab).real {Message.a} = s.logistic (s.cAndB + Real.log s.p)

The measured speaker's use of A in the world of both.

theorem CremersWilcoxSpector2023.bgSpeaker_measured_wa_a (s : Setting) :

((bgSpeaker s Background.measured) World.wa).real {Message.a} = s.logistic (s.cAndNotB + Real.log (1 - s.p))

The measured speaker's use of A in the world of A alone.

noncomputable def CremersWilcoxSpector2023.bgWeight (ω : ℝ) :

Background → ENNReal

The wonky background has weight the wonkiness ω, and the measured one 1 - ω.

Equations

CremersWilcoxSpector2023.bgWeight ω CremersWilcoxSpector2023.Background.wonky = ENNReal.ofReal ω
CremersWilcoxSpector2023.bgWeight ω CremersWilcoxSpector2023.Background.measured = ENNReal.ofReal (1 - ω)

Instances For

theorem CremersWilcoxSpector2023.bgWeight_ne_top (ω : ℝ) (b : Background) :

bgWeight ω b ≠ ⊤

theorem CremersWilcoxSpector2023.bgWeight_exists_ne_zero (ω : ℝ) :

∃ (b : Background), bgWeight ω b ≠ 0

Some background has positive weight.

noncomputable def CremersWilcoxSpector2023.bgPrior (ω : ℝ) :

MeasureTheory.Measure Background

The prior on backgrounds puts ω on the wonky background and 1 - ω on the measured one.

Equations

CremersWilcoxSpector2023.bgPrior ω = ∑ b : CremersWilcoxSpector2023.Background, CremersWilcoxSpector2023.bgWeight ω b • MeasureTheory.Measure.dirac b

Instances For

theorem CremersWilcoxSpector2023.bgPrior_apply_singleton (ω : ℝ) (b : Background) :

(bgPrior ω) {b} = bgWeight ω b

instance CremersWilcoxSpector2023.instIsFiniteMeasureBackgroundBgPrior (ω : ℝ) :

MeasureTheory.IsFiniteMeasure (bgPrior ω)

noncomputable def CremersWilcoxSpector2023.bayesWonkySpeaker (s : Setting) (ω : ℝ) :

ProbabilityTheory.Kernel World Message

The speaker marginalised over the listener's uncertainty about the speaker's prior (item 5 of the §4.1 model, the Bayesian version).

Equations

CremersWilcoxSpector2023.bayesWonkySpeaker s ω = ∑ b : CremersWilcoxSpector2023.Background, CremersWilcoxSpector2023.bgWeight ω b • CremersWilcoxSpector2023.bgSpeaker s b

Instances For

instance CremersWilcoxSpector2023.instIsFiniteKernelWorldMessageBayesWonkySpeaker (s : Setting) (ω : ℝ) :

ProbabilityTheory.IsFiniteKernel (bayesWonkySpeaker s ω)

theorem CremersWilcoxSpector2023.bayesWonkySpeaker_real_singleton (s : Setting) (ω : ℝ) (hω₀ : 0 ≤ ω) (hω₁ : ω ≤ 1) (w : World) (u : Message) :

((bayesWonkySpeaker s ω) w).real {u} = ω * ((bgSpeaker s Background.wonky) w).real {u} + (1 - ω) * ((bgSpeaker s Background.measured) w).real {u}

The Bayesian wonky speaker on reals.

theorem CremersWilcoxSpector2023.bayesWonkySpeaker_zero (s : Setting) (w : World) :

(bayesWonkySpeaker s 0) w = (s.speaker literal) w

Without wonkiness the Bayesian wonky speaker is the baseline speaker.

theorem CremersWilcoxSpector2023.comp_bayesWonkySpeaker_ne_zero (s : Setting) (ω : ℝ) (u : Message) :

(s.prior.bind ⇑(bayesWonkySpeaker s ω)) {u} ≠ 0

Every message is used somewhere under a positively weighted background, so is heard with positive probability.

noncomputable def CremersWilcoxSpector2023.bayesWonkyListener (s : Setting) (ω : ℝ) :

ProbabilityTheory.Kernel Message World

The Bayesian wonky listener, with the measured prior (item 5 of the Bayesian §4.1 model).

Equations

CremersWilcoxSpector2023.bayesWonkyListener s ω = RSA.listener s.prior ⇑(CremersWilcoxSpector2023.bayesWonkySpeaker s ω)

Instances For

noncomputable def CremersWilcoxSpector2023.bayesWonkyJointListener (s : Setting) (ω : ℝ) :

ProbabilityTheory.Kernel Message (World × Background)

The joint posterior over worlds and the speaker's background, with the measured prior on worlds independent of the prior on backgrounds (item 4 of the Bayesian §4.1 model).

Equations

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

Instances For

theorem CremersWilcoxSpector2023.bayesWonkyJointListener_fst (s : Setting) (ω : ℝ) :

(bayesWonkyJointListener s ω).fst = bayesWonkyListener s ω

The joint posterior marginalized on backgrounds is the listener of item 5.

theorem CremersWilcoxSpector2023.prior_lt_bayesWonkyListener_iff (s : Setting) (ω : ℝ) (hω₀ : 0 ≤ ω) (hω₁ : ω ≤ 1) :

s.prior.real {World.wab} < ((bayesWonkyListener s ω) Message.a).real {World.wab} ↔ 0 < (1 - ω) * (s.logistic (s.cAndB + Real.log s.p) - s.logistic (s.cAndNotB + Real.log (1 - s.p))) + ω * (s.logistic (s.cAndB - Real.log 2) - s.logistic (s.cAndNotB - Real.log 2))

Anti-exhaustivity exactly when the wonkiness-weighted excess of the use of A in the world of both over its use in the world of A alone is positive (Appendix A.2, the Bayesian model).

noncomputable def CremersWilcoxSpector2023.worldKernel (s : Setting) :

ProbabilityTheory.Kernel Background World

The world given the background.

Equations

CremersWilcoxSpector2023.worldKernel s = ProbabilityTheory.Kernel.ofFunOfCountable (CremersWilcoxSpector2023.worldPrior s)

Instances For

instance CremersWilcoxSpector2023.instIsMarkovKernelBackgroundWorldWorldKernel (s : Setting) :

ProbabilityTheory.IsMarkovKernel (worldKernel s)

noncomputable def CremersWilcoxSpector2023.wonkyJoint (s : Setting) (ω : ℝ) :

MeasureTheory.Measure (Background × World)

The prior of the non-Bayesian model draws the background, then the world under it (item 4 of the §4.1 model).

Equations

CremersWilcoxSpector2023.wonkyJoint s ω = (CremersWilcoxSpector2023.bgPrior ω).compProd (CremersWilcoxSpector2023.worldKernel s)

Instances For

instance CremersWilcoxSpector2023.instIsFiniteMeasureProdBackgroundWorldWonkyJoint (s : Setting) (ω : ℝ) :

MeasureTheory.IsFiniteMeasure (wonkyJoint s ω)

theorem CremersWilcoxSpector2023.wonkyJoint_apply_singleton (s : Setting) (ω : ℝ) (b : Background) (w : World) :

(wonkyJoint s ω) {(b, w)} = bgWeight ω b * (worldPrior s b) {w}

theorem CremersWilcoxSpector2023.wonkyJoint_real_singleton (s : Setting) (ω : ℝ) (b : Background) (w : World) :

(wonkyJoint s ω).real {(b, w)} = (bgWeight ω b).toReal * (worldPrior s b).real {w}

noncomputable def CremersWilcoxSpector2023.wonkySpeaker (s : Setting) :

ProbabilityTheory.Kernel (Background × World) Message

The speaker of the non-Bayesian model, at a background and a world.

Equations

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

Instances For

theorem CremersWilcoxSpector2023.wonkySpeaker_apply (s : Setting) (x : Background × World) :

(wonkySpeaker s) x = (bgSpeaker s x.1) x.2

instance CremersWilcoxSpector2023.instIsFiniteKernelProdBackgroundWorldMessageWonkySpeaker (s : Setting) :

ProbabilityTheory.IsFiniteKernel (wonkySpeaker s)

theorem CremersWilcoxSpector2023.wonkySpeaker_ne_zero (s : Setting) {w : World} {u : Message} (b : Background) (hw : literal.sat u w = true) :

((wonkySpeaker s) (b, w)) {u} ≠ 0

A message true at a world is used there under either background.

theorem CremersWilcoxSpector2023.comp_wonkySpeaker_ne_zero (s : Setting) (ω : ℝ) (u : Message) :

((wonkyJoint s ω).bind ⇑(wonkySpeaker s)) {u} ≠ 0

Every message is used somewhere under a positively weighted background, so is heard with positive probability.

noncomputable def CremersWilcoxSpector2023.wonkyListener (s : Setting) (ω : ℝ) :

ProbabilityTheory.Kernel Message (Background × World)

The non-Bayesian listener, uncertain about the background and the world jointly (item 4 of the §4.1 model).

Equations

CremersWilcoxSpector2023.wonkyListener s ω = RSA.listener (CremersWilcoxSpector2023.wonkyJoint s ω) ⇑(CremersWilcoxSpector2023.wonkySpeaker s)

Instances For

theorem CremersWilcoxSpector2023.prior_lt_wonkyListener_iff (s : Setting) (ω : ℝ) (hω₀ : 0 ≤ ω) (hω₁ : ω ≤ 1) :

s.prior.real {World.wab} < ((wonkyListener s ω) Message.a).snd.real {World.wab} ↔ s.p * (ω * 2⁻¹ * (s.logistic (s.cAndNotB - Real.log 2) + s.logistic (s.cAndB - Real.log 2)) + (1 - ω) * ((1 - s.p) * s.logistic (s.cAndNotB + Real.log (1 - s.p)) + s.p * s.logistic (s.cAndB + Real.log s.p))) < ω * 2⁻¹ * s.logistic (s.cAndB - Real.log 2) + (1 - ω) * (s.p * s.logistic (s.cAndB + Real.log s.p))

The non-Bayesian model is anti-exhaustive with respect to the measured prior exactly when the prior times the marginal use of A falls below the background-weighted use of A in the world of both; the paper resolves this inequality numerically (A.5a).