Docs / Pragmatics / RSA / Recursion

The recursion

import Linglib.Pragmatics.RSA.Recursion · namespace RSA

Source

A speaker at recursion level n addresses the listener at level n - 1, and the listener at level n addresses the speaker at level n, grounding out in a listener at level 0. A level is therefore an iterate of one map, RSA.recurse, which replaces a listener by the listener of the speaker who addresses her. Along the iterates utterances read alike stay alike, whatever their costs. When the speaker knows the state, a listener keeps exactly the states the listener she started from allows, so that no finite level excludes a state where an utterance is true: the recursion sharpens preferences among those states without making any of them impossible.

References

Declarations

One level of recursion replaces a listener by the listener of the speaker who addresses her. The speaker observes the state through κ, believes b o at an observation o, and has rationality α and cost C; the listener holds the prior μ.

recurseL34–39
noncomputable def RSA.recurse {W : Type u_1} {U : Type u_2} {O : Type u_3} [MeasurableSpace W] [Fintype W] [MeasurableSpace U] [Fintype U] [MeasurableSingletonClass U] [MeasurableSpace O] [Countable O] [MeasurableSingletonClass O] (μ : MeasureTheory.Measure W) (κ : ProbabilityTheory.Kernel W O) (b : O → MeasureTheory.Measure W) (α : ℝ) (C : U → ℝ) (L : ProbabilityTheory.Kernel U W) :
ProbabilityTheory.Kernel U W

Used by instIsFiniteKernelRecurse, instIsZeroOrProbabilityMeasureCoeKernelMeasureRecurse, instIsFiniteKernelIterateKernelRecurse, instIsZeroOrProbabilityMeasureCoeKernelMeasureIterateRecurse, recurse_apply_eq_of_apply_eq, iterate_recurse_apply_eq_of_apply_eq, recurse_id_dirac, recurse_apply_singleton_eq_zero, iterate_recurse_id_dirac_apply_singleton_eq_zero, iterate_recurse_id_dirac_apply_singleton_ne_zero, iterate_recurse_id_dirac_apply_singleton_ne_zero_iff, iterate_recurse_listener_truthful_apply_singleton_ne_zero_iff

Used in Pragmatics/RSA/AlternatingMaximization, BergenLevyGoodman2016, ZaslavskyHuLevy2021

L44–46
L48–50
L52–58
L60–67
L69–78

Bergen et al. 2016's Lemma 2: utterances a listener interprets alike are interpreted alike at every level of the recursion.

theorem iterate_recurse_apply_eq_of_apply_eqL80–88
{W : Type u_1} {U : Type u_2} {O : Type u_3} [MeasurableSpace W] [Fintype W] [MeasurableSpace U] [Fintype U] [MeasurableSingletonClass U] [MeasurableSpace O] [Countable O] [MeasurableSingletonClass O] {μ : MeasureTheory.Measure W} {κ : ProbabilityTheory.Kernel W O} {b : O → MeasureTheory.Measure W} {α : ℝ} {C : U → ℝ} {L : ProbabilityTheory.Kernel U W} {u u' : U} (h : L u = L u') (n : ℕ) :
((recurse μ κ b α C)^[n] L) u' = ((recurse μ κ b α C)^[n] L) u

Built from

L90–95
L101–112
L114–120
L124–131

When the speaker knows the state, a listener at any level takes a state to be possible exactly when the listener she started from does.

theorem iterate_recurse_id_dirac_apply_singleton_ne_zero_iffL133–139
{W : Type u_1} {U : Type u_2} [MeasurableSpace W] [Fintype W] [MeasurableSpace U] [Fintype U] [MeasurableSingletonClass U] {μ : MeasureTheory.Measure W} {α : ℝ} {C : U → ℝ} {L : ProbabilityTheory.Kernel U W} {u : U} {w : W} [MeasurableSingletonClass W] [MeasureTheory.IsFiniteMeasure μ] [ProbabilityTheory.IsFiniteKernel L] (hα : 0 < α) (hL : ∀ (u : U) (w : W), (L u) {w} ≠ 0 → μ {w} ≠ 0) (n : ℕ) :
(((recurse μ ProbabilityTheory.Kernel.id MeasureTheory.Measure.dirac α C)^[n] L) u) {w} ≠ 0 ↔ (L u) {w} ≠ 0

Built from

When the speaker knows the state and the recursion starts from the literal listener, no level excludes a state of positive prior where the utterance is true, or admits any other.

theorem iterate_recurse_listener_truthful_apply_singleton_ne_zero_iffL141–149
{W : Type u_1} {U : Type u_2} [MeasurableSpace W] [Fintype W] [MeasurableSpace U] [Fintype U] [MeasurableSingletonClass U] {μ : MeasureTheory.Measure W} {α : ℝ} {C : U → ℝ} {u : U} {w : W} [MeasurableSingletonClass W] [MeasureTheory.IsFiniteMeasure μ] {sem : U → Set W} (hα : 0 < α) (n : ℕ) :
(((recurse μ ProbabilityTheory.Kernel.id MeasureTheory.Measure.dirac α C)^[n] (listener μ (truthful sem))) u) {w} ≠ 0 ↔ w ∈ sem u ∧ μ {w} ≠ 0

Built from