RSA reference game — parametric substrate

The classic Rational Speech Act reference game from @cite{frank-goodman-2012} as a substrate, parametric in the meaning matrix and world prior. Every paper using a "speaker normalises inverse-extension- size weights" pattern inherits the architectural theorems below.

The architectural pitch

WebPPL/Python implementations re-derive the size principle and pragmatic narrowing per stimulus. Here both are proved once, parametric in the vocabulary, the meaning matrix, and the world prior. Specific empirical stimuli become one-liner instances.

Main definitions

• RSA.ReferenceGame.IsCovering meaning — the structural assumption: every utterance has a non-empty extension AND every world is named by some utterance. Captured as a typeclass to avoid threading two hypotheses.
• RSA.ReferenceGame.L0 — literal listener (Eq. S3): uniform on extension.
• RSA.ReferenceGame.S1 — pragmatic speaker (Eq. S4 with α=1, no cost): PMF.normalize of L0 weights — the Tenenbaum-Griffiths size principle.
• RSA.ReferenceGame.L1 — pragmatic listener: PMF.posterior against any full-support world prior.

Main statements

• S1_apply_of_appliesTo — the size principle as Eq. S4: S1 w u = (1/|⟦u⟧|) / Σ_{u'} L0 u' w when u applies to w.
• S1_lt_of_partition_gt — the pragmatic-narrowing theorem: when u applies to two worlds, the speaker prefers the world whose alternative-set has SMALLER partition function.
• L1_gt_iff_S1_lt — narrowing transfers from S1 to L1 (uniform prior).
• L1_eq_pure_of_unique_extension — when an utterance applies to a unique world, the listener concentrates entirely there (full mass).

Concrete instantiation

Phenomena/Reference/Studies/FrankGoodman2012.lean instantiates these theorems at the paper's 3-object × 4-feature stimulus. Each of the 4 paper findings is a one-liner corollary.

§1. The covering hypothesis

class RSA.ReferenceGame.IsCovering {Word : Type u_1} {Object : Type u_2} [Fintype Object] (meaning : Word → Object → Bool) : Prop

A meaning matrix is covering if every utterance has a non-empty extension AND every world is named by some utterance. Minimal data needed to set up an RSA reference game on the model class. Captured as a typeclass so consumers state [IsCovering meaning] once and inherit both facts.

• extension_nonempty (u : Word) : (extensionOf meaning u).Nonempty

  Every utterance applies to at least one object.

• covering (w : Object) : ∃ (u : Word), meaning u w = true

  Every object is named by at least one utterance.

§2. Model definitions

@[reducible, inline]

abbrev RSA.ReferenceGame.extension {Word : Type u_1} {Object : Type u_2} [Fintype Object] (meaning : Word → Object → Bool) (u : Word) : Finset Object

Extension of an utterance: the Finset of objects to which it applies.

Equations

• RSA.ReferenceGame.extension meaning u = RSA.extensionOf meaning u

noncomputable def RSA.ReferenceGame.L0 {Word : Type u_1} {Object : Type u_2} [Fintype Object] (meaning : Word → Object → Bool) [hCov : IsCovering meaning] (u : Word) : PMF Object

Literal listener (Eq. S3): uniform on the utterance's extension.

Equations

• RSA.ReferenceGame.L0 meaning u = RSA.L0OfBoolMeaning meaning u ⋯

theorem RSA.ReferenceGame.L0_tsum_ne_zero {Word : Type u_1} {Object : Type u_2} [Fintype Word] [Fintype Object] (meaning : Word → Object → Bool) [hCov : IsCovering meaning] (w : Object) : ∑' (u : Word), (L0 meaning u) w ≠ 0

The L0 sum over utterances at any world is non-zero (covering).

theorem RSA.ReferenceGame.L0_tsum_ne_top {Word : Type u_1} {Object : Type u_2} [Fintype Word] [Fintype Object] (meaning : Word → Object → Bool) [hCov : IsCovering meaning] (w : Object) : ∑' (u : Word), (L0 meaning u) w ≠ ⊤

The L0 sum is finite.

noncomputable def RSA.ReferenceGame.S1 {Word : Type u_1} {Object : Type u_2} [Fintype Word] [Fintype Object] (meaning : Word → Object → Bool) [hCov : IsCovering meaning] (w : Object) : PMF Word

Pragmatic speaker (Eq. S4 with α=1, no cost): PMF.normalize of the literal-listener weights. The normalisation factor cancels the per- utterance constant from the Boltzmann derivation; what remains is the size principle — probability inversely proportional to extension size.

Equations

• RSA.ReferenceGame.S1 meaning w = PMF.normalize (fun (u : Word) => (RSA.ReferenceGame.L0 meaning u) w) ⋯ ⋯

theorem RSA.ReferenceGame.L1_marginal_ne_zero {Word : Type u_1} {Object : Type u_2} [Fintype Word] [Fintype Object] (meaning : Word → Object → Bool) [hCov : IsCovering meaning] {worldPrior : PMF Object} {u : Word} (h_witness : ∃ w ∈ extension meaning u, worldPrior w ≠ 0) : PMF.marginal (S1 meaning) worldPrior u ≠ 0

The marginal Σ_w worldPrior w · S1 w u is non-zero whenever the prior puts positive mass on some world to which u applies — the substrate condition for PMF.posterior.

noncomputable def RSA.ReferenceGame.L1 {Word : Type u_1} {Object : Type u_2} [Fintype Word] [Fintype Object] (meaning : Word → Object → Bool) [hCov : IsCovering meaning] (worldPrior : PMF Object) (u : Word) (h_marg : PMF.marginal (S1 meaning) worldPrior u ≠ 0) : PMF Object

Pragmatic listener: posterior of S1 against any world prior.

Equations

• RSA.ReferenceGame.L1 meaning worldPrior u h_marg = PMF.posterior (RSA.ReferenceGame.S1 meaning) worldPrior u h_marg

§3. The partition function

The "partition function" Σ_u L0 u w is the size-principle weight of all applicable utterances at world w. It is the denominator of the speaker's softmax (Eq. S4) and the load-bearing object for pragmatic narrowing.

The structural theorem partition_eq_filter_sum rewrites it as a sum over the applicable-utterance Finset — the form most consumers want.

noncomputable def RSA.ReferenceGame.partition {Word : Type u_1} {Object : Type u_2} [Fintype Object] (meaning : Word → Object → Bool) [hCov : IsCovering meaning] (w : Object) : ENNReal

The partition function at world w: the size-principle weight summed over all utterances. Equals Σ_{u : meaning u w} (1/|⟦u⟧|) (theorem partition_eq_filter_sum below).

Equations

• RSA.ReferenceGame.partition meaning w = ∑' (u : Word), (RSA.ReferenceGame.L0 meaning u) w

theorem RSA.ReferenceGame.partition_ne_zero {Word : Type u_1} {Object : Type u_2} [Fintype Word] [Fintype Object] (meaning : Word → Object → Bool) [hCov : IsCovering meaning] (w : Object) : partition meaning w ≠ 0

The partition is non-zero (covering).

theorem RSA.ReferenceGame.partition_ne_top {Word : Type u_1} {Object : Type u_2} [Fintype Word] [Fintype Object] (meaning : Word → Object → Bool) [hCov : IsCovering meaning] (w : Object) : partition meaning w ≠ ⊤

The partition is finite.

theorem RSA.ReferenceGame.partition_eq_filter_sum {Word : Type u_1} {Object : Type u_2} [Fintype Word] [Fintype Object] (meaning : Word → Object → Bool) [hCov : IsCovering meaning] (w : Object) [DecidableEq Word] : partition meaning w = ∑ u : Word with meaning u w = true, (↑(extension meaning u).card)⁻¹

Partition as filter sum: the partition function equals the sum of inverse extension cardinalities over applicable utterances. The "non-applicable" terms vanish (their L0 value is 0); what remains is the size-principle weight of each alternative.

This is the form most consumers use to compute concrete partition values.

§4. Apply formulas (Eqs. S3, S4)

@[simp]

theorem RSA.ReferenceGame.L0_apply_of_appliesTo {Word : Type u_1} {Object : Type u_2} [Fintype Word] [Fintype Object] (meaning : Word → Object → Bool) [hCov : IsCovering meaning] {u : Word} {w : Object} (h : meaning u w = true) : (L0 meaning u) w = (↑(extension meaning u).card)⁻¹

@[simp]

theorem RSA.ReferenceGame.L0_apply_of_not_appliesTo {Word : Type u_1} {Object : Type u_2} [Fintype Word] [Fintype Object] (meaning : Word → Object → Bool) [hCov : IsCovering meaning] {u : Word} {w : Object} (h : meaning u w ≠ true) : (L0 meaning u) w = 0

theorem RSA.ReferenceGame.S1_apply_of_appliesTo {Word : Type u_1} {Object : Type u_2} [Fintype Word] [Fintype Object] (meaning : Word → Object → Bool) [hCov : IsCovering meaning] {u : Word} {w : Object} (h : meaning u w = true) : (S1 meaning w) u = (↑(extension meaning u).card)⁻¹ / ∑' (u' : Word), (L0 meaning u') w

Size principle (Eq. S4): for an utterance applying to w, the speaker probability is (1/|⟦u⟧|) divided by the sum of 1/|⟦u'⟧| over all utterances u' applying to w — the partition function.

theorem RSA.ReferenceGame.S1_apply_of_not_appliesTo {Word : Type u_1} {Object : Type u_2} [Fintype Word] [Fintype Object] (meaning : Word → Object → Bool) [hCov : IsCovering meaning] {u : Word} {w : Object} (h : meaning u w ≠ true) : (S1 meaning w) u = 0

The speaker assigns zero probability to utterances that don't apply.

§4. Pragmatic narrowing — the architectural theorem

theorem RSA.ReferenceGame.S1_lt_of_partition_gt {Word : Type u_1} {Object : Type u_2} [Fintype Word] [Fintype Object] (meaning : Word → Object → Bool) [hCov : IsCovering meaning] {u : Word} {w w' : Object} (h_w : meaning u w = true) (h_w' : meaning u w' = true) (h_partition : ∑' (u' : Word), (L0 meaning u') w' < ∑' (u' : Word), (L0 meaning u') w) : (S1 meaning w) u < (S1 meaning w') u

Pragmatic-narrowing theorem (parametric): when u applies to two worlds w and w', the speaker prefers u at w' over w iff the partition function at w exceeds that at w'.

Architectural reading: a larger partition at a world means more competition from informative alternatives, so the speaker is less likely to choose u at that world; the listener therefore narrows toward the world with fewer informative competitors. This is the load-bearing structural theorem of @cite{frank-goodman-2012} — every paper finding is an instance.

Direct via PMF.normalize_lt_of_apply_eq_of_sum_lt: same numerator (L0 u w = L0 u w' = (extension u).card⁻¹), comparing partitions.

theorem RSA.ReferenceGame.S1_lt_of_appliesTo_only {Word : Type u_1} {Object : Type u_2} [Fintype Word] [Fintype Object] (meaning : Word → Object → Bool) [hCov : IsCovering meaning] {u : Word} {w w' : Object} (h_w : meaning u w ≠ true) (h_w' : meaning u w' = true) : (S1 meaning w) u < (S1 meaning w') u

Cross-base companion: when u applies to only one of the two worlds, the speaker prefers the applying world (the other gets zero mass).

§5. L1 narrowing under uniform prior

theorem RSA.ReferenceGame.L1_gt_iff_S1_lt_uniform {Word : Type u_1} {Object : Type u_2} [Fintype Word] [Fintype Object] (meaning : Word → Object → Bool) [hCov : IsCovering meaning] [Nonempty Object] {u : Word} (h_marg : PMF.marginal (S1 meaning) (PMF.uniformOfFintype Object) u ≠ 0) (w w' : Object) : (L1 meaning (PMF.uniformOfFintype Object) u h_marg) w' > (L1 meaning (PMF.uniformOfFintype Object) u h_marg) w ↔ (S1 meaning w) u < (S1 meaning w') u

L1 narrowing follows S1 narrowing (uniform world prior): the posterior at uniform prior reverses the speaker's preference, so L1 favours the world S1 favours.

§6. Unique reference

theorem RSA.ReferenceGame.L1_eq_one_of_unique_extension {Word : Type u_1} {Object : Type u_2} [Fintype Word] [Fintype Object] (meaning : Word → Object → Bool) [hCov : IsCovering meaning] [Nonempty Object] {u : Word} {w_unique : Object} (h_applies : meaning u w_unique = true) (h_unique : ∀ (w' : Object), w' ≠ w_unique → meaning u w' ≠ true) (worldPrior : PMF Object) (h_prior : worldPrior w_unique ≠ 0) (h_marg : PMF.marginal (S1 meaning) worldPrior u ≠ 0) : (L1 meaning worldPrior u h_marg) w_unique = 1

Unique-reference theorem: when utterance u applies to a unique world w_unique (no other world satisfies meaning u), the L1 posterior concentrates entirely on w_unique — full mass 1.

Architectural reading: a uniquely-identifying utterance leaves the listener with no Bayesian uncertainty. Direct via PMF.posterior_eq_one_of_singleton_score_support.