Rational speech acts at a uniform prior

import Linglib.Pragmatics.RSA.Uniform · namespace RSA

Franke and Bergen's model has finitely many states, Boolean meanings, a uniform prior and no cost. Its literal listener is then uniform on the extension of the utterance, and its speaker weighs each true utterance by the inverse size of its extension to the power of her rationality. Her masses are ratios of inverse-power sums over informativity profiles, the multisets of extension sizes of the utterances true at a state, so a comparison between two states is a comparison of multisets of naturals. It holds at every rationality when one multiset dominates the other, and at a natural rationality it is an inequality of naturals.

Main definitions

RSA.profile sem A w: the extension sizes of the utterances in A true at w.

Main results

RSA.listener_uniformOn_truthful_apply: the literal listener is uniform on the extension.
RSA.speaker_uniformOn_dirac_real_singleton_lt_of_card_lt: of two true utterances the speaker prefers the one with the smaller extension.
RSA.speaker_uniformOn_dirac_real_finset_lt_of_strictDominates: the speaker is likelier to choose within a set of utterances at one state than at another, at every rationality, when the products of their profiles are ordered by dominance.
RSA.listener_speaker_uniformOn_real_singleton_lt_of_strictDominates: the pragmatic listener's preference between two states under the same condition.

Implementation notes

There are no new kernels. The literal listener is RSA.listener at the uniform prior and the truthful channel, and the speaker is RSA.speaker at no cost; this file abbreviates them L₀ and S₁[α].
Meanings are Finset-valued, so that extension sizes, and with them the hypotheses of the comparison lemmas, are decidable.
The comparison lemmas are stated for the speaker's mass on a set of utterances. The pragmatic listener is the case of a singleton, and the listener who hears only the form of the speaker's choice the case of the fibre of the form.

References

Franke & Bergen 2020, Theory-Driven Statistical Modeling for Semantics and Pragmatics: A Case Study on Grammatically Generated Implicature Readings formalized

Informativity profiles

The informativity profile of a state over a set A of utterances is the multiset of extension sizes of the utterances in A true at the state.

def profile L62–65

{W : Type u_1} {U : Type u_2} [DecidableEq W] (sem : U → Finset W) (A : Finset U) (w : W) :

Multiset ℕ

profile sem A w = Multiset.map (fun (u : U) => (sem u).card) {x ∈ A | w ∈ sem x}.val

Used in Anderson2021, FrankGoodman2012

The literal listener

The literal listener at a uniform prior (eq. 5) is uniform on the extension of the utterance.

theorem listener_uniformOn_truthful_apply L157–160

{W : Type u_1} {U : Type u_2} [Fintype W] [MeasurableSpace W] [DiscreteMeasurableSpace W] [Fintype U] [MeasurableSpace U] [DiscreteMeasurableSpace U] (sem : U → Finset W) (u : U) :

(listener (ProbabilityTheory.uniformOn Set.univ) (truthful fun (u : U) => ↑(sem u))) u = ProbabilityTheory.uniformOn ↑(sem u)

L166–168

L170–173

The speaker

The speaker of eq. 7 knows the state and addresses the literal listener at no cost.

Of two true utterances, the speaker produces the one with the smaller extension more often at every positive rationality, the qualitative claim of eq. 7.

theorem speaker_uniformOn_dirac_real_singleton_lt_of_card_lt L224–235

{W : Type u_1} {U : Type u_2} [Fintype W] [MeasurableSpace W] [DiscreteMeasurableSpace W] [Fintype U] [MeasurableSpace U] [DiscreteMeasurableSpace U] (sem : U → Finset W) {α : ℝ} [DecidableEq W] (hα : 0 < α) {w : W} {u u' : U} (h : w ∈ sem u) (h' : w ∈ sem u') (hcard : (sem u').card < (sem u).card) :

((speaker α 0 (⇑(listener (ProbabilityTheory.uniformOn Set.univ) (truthful fun (u : U) => ↑(sem u)))) MeasureTheory.Measure.dirac) w).real {u} < ((speaker α 0 (⇑(listener (ProbabilityTheory.uniformOn Set.univ) (truthful fun (u : U) => ↑(sem u)))) MeasureTheory.Measure.dirac) w).real {u'}

A speaker who entertains several states

A speaker with a probability belief, facing the literal listener at no cost, weighs an utterance by the support S of her belief alone. She says only the utterances true throughout S, each with weight the inverse size of its extension to the power α.

L359–362

L364–374

L376–380

Comparing two states

How likely the speaker is to choose within a set A of utterances at one state against another is a comparison of profile sums. It holds at every positive rationality when the products of the profile of A at one state with the profile of the remaining utterances at the other are ordered by dominance, and at a natural rationality it is an inequality of naturals. The pragmatic listener at a uniform prior ranks two states as the speaker produces what she heard.

L396–410

The speaker is likelier to choose within A at w₂ than at w₁, at every positive rationality, when the products of profiles are ordered by strict dominance.

theorem speaker_uniformOn_dirac_real_finset_lt_of_strictDominates L412–430

{W : Type u_1} {U : Type u_2} [Fintype W] [MeasurableSpace W] [DiscreteMeasurableSpace W] [Fintype U] [MeasurableSpace U] [DiscreteMeasurableSpace U] (sem : U → Finset W) [DecidableEq W] [DecidableEq U] {α : ℝ} {A : Finset U} {w₁ w₂ : W} (hα : 0 < α) (h : ((profile sem A w₂).prodMul (profile sem Aᶜ w₁)).StrictDominates ((profile sem A w₁).prodMul (profile sem Aᶜ w₂))) :

((speaker α 0 (⇑(listener (ProbabilityTheory.uniformOn Set.univ) (truthful fun (u : U) => ↑(sem u)))) MeasureTheory.Measure.dirac) w₁).real ↑A < ((speaker α 0 (⇑(listener (ProbabilityTheory.uniformOn Set.univ) (truthful fun (u : U) => ↑(sem u)))) MeasureTheory.Measure.dirac) w₂).real ↑A

Built from

L432–452

Hearing an utterance, the pragmatic listener at a uniform prior prefers w₂ to w₁ at every positive rationality when the products of profiles are ordered by strict dominance.

theorem listener_speaker_uniformOn_real_singleton_lt_of_strictDominates L454–462

{W : Type u_1} {U : Type u_2} [Fintype W] [MeasurableSpace W] [DiscreteMeasurableSpace W] [Fintype U] [MeasurableSpace U] [DiscreteMeasurableSpace U] (sem : U → Finset W) [DecidableEq W] [DecidableEq U] {α : ℝ} {w₁ w₂ : W} (hα : 0 < α) {u : U} (h : ((profile sem {u} w₂).prodMul (profile sem {u}ᶜ w₁)).StrictDominates ((profile sem {u} w₁).prodMul (profile sem {u}ᶜ w₂))) :

((listener (ProbabilityTheory.uniformOn Set.univ) ⇑(speaker α 0 (⇑(listener (ProbabilityTheory.uniformOn Set.univ) (truthful fun (u : U) => ↑(sem u)))) MeasureTheory.Measure.dirac)) u).real {w₁} < ((listener (ProbabilityTheory.uniformOn Set.univ) ⇑(speaker α 0 (⇑(listener (ProbabilityTheory.uniformOn Set.univ) (truthful fun (u : U) => ↑(sem u)))) MeasureTheory.Measure.dirac)) u).real {w₂}

Built from

The listener who hears the form

When the listener hears only the form obs u of the speaker's choice (eqs. 18b and 21b), her belief about the state compares how likely the speaker is to choose within the fibre of the form, and her belief about the choice compares how likely the states together are to produce it.

L478–506

L510–520

L522–536

Latent families

A latent the speaker also knows, a lexicon or a parse, indexes the meaning, and the listener at a uniform prior over pairs of a state and a latent inverts the speaker of each latent.

L554–579