Docs / Pragmatics / RSA / LexicalUncertainty

Lexical uncertainty

import Linglib.Pragmatics.RSA.LexicalUncertainty · namespace RSA

Source

In the lexical-uncertainty model of Bergen et al. 2016, speaker and listener share a prior over lexica. The speaker uses one lexicon and addresses its literal listener, and the pragmatic listener, unsure which, inverts the speaker of each lexicon. With the lexicon a coordinate of the state, she is RSA.listener at the product of the prior over states and the prior over lexica. The paper states her belief about the state as the listener of the speaker averaged over lexica, and the two presentations agree. A state is possible after an utterance exactly when it has positive prior and some lexicon of positive prior has its speaker produce the utterance there (the union of the lexica's supports).

Nothing requires the latent to be a lexicon: a threshold, a comparison class, a scope reading or a question under discussion that the speaker knows and the listener does not enters the same way.

Main statements

References

Declarations

Lexical uncertainty. Against a product prior, the first marginal of the listener is the listener of the speaker averaged over the second coordinate by its prior.

theorem listener_prod_fstL42–55
{A : Type u_1} {B : Type u_2} {U : Type u_3} [MeasurableSpace A] [MeasurableSpace B] [MeasurableSpace U] [Fintype A] [Fintype B] [MeasurableSingletonClass A] [MeasurableSingletonClass B] [Countable U] [MeasurableSingletonClass U] (μ : MeasureTheory.Measure A) (ν : MeasureTheory.Measure B) (S : A × B → MeasureTheory.Measure U) :
(listener (μ.prod ν) S).fst = listener μ fun (a : A) => ∑ b : B, ν {b} • S (a, b)
L60–67

Against a product prior, a state is possible after an utterance exactly when it has positive prior and the speaker produces the utterance there at some value of positive prior of the second coordinate.

theorem listener_prod_fst_apply_singleton_ne_zero_iffL69–76
{A : Type u_1} {B : Type u_2} {U : Type u_3} [MeasurableSpace A] [MeasurableSpace B] [MeasurableSpace U] [Fintype A] [Fintype B] [MeasurableSingletonClass A] [MeasurableSingletonClass B] [Countable U] [MeasurableSingletonClass U] (μ : MeasureTheory.Measure A) [MeasureTheory.IsFiniteMeasure μ] (ν : MeasureTheory.Measure B) [MeasureTheory.IsFiniteMeasure ν] (S : A × B → MeasureTheory.Measure U) [∀ (p : A × B), MeasureTheory.IsFiniteMeasure (S p)] (u : U) (a : A) :
((listener (μ.prod ν) S) u).fst {a} ≠ 0 ↔ μ {a} ≠ 0 ∧ ∃ (b : B), ν {b} ≠ 0 ∧ (S (a, b)) {u} ≠ 0