RSA score chains in ℚ≥0

Combinators for the exact-rational face of RSA models: literal listener, exponentiated speaker with cost, joint pragmatic listener, marginals, and stacked higher-order speakers. A study composes these into its chain and wraps normalization sites with PMF.ofScores; predictions then reduce to ℚ≥0 comparisons closed by decide +kernel via the PMF.ofScores_lt family.

s1 applies PMF.scoresWith mid-tower, so a zero-mass utterance row takes its declared fallback inside the ℚ≥0 values — downstream marginals are total and the PMF bridges need no side conditions.

Scope: this face covers natural-α, rational-parameter models. Models with transcendental ingredients state their chains on the ℝ≥0∞ RSA.Canonical/operator face with kernel-certified rational bounds on named atoms.

Main definitions

• RSA.Score.l0 — literal listener from a Boolean meaning and a prior.
• RSA.Score.s1 — speaker scores l0^α · cost, fallback-completed.
• RSA.Score.l1Joint — joint pragmatic-listener scores over W × Lat.
• RSA.Score.worldMarginal / latentMarginal — marginals of joint scores.
• RSA.Score.s2 — stacked speaker over listener coordinates.

Kernel hygiene

• Declare the full instance set on ℚ≥0-face sections: [Fintype _] [DecidableEq _] [Nonempty _].
• Base tables are pattern matches or Bool tables — never propositional if x = y over a derived DecidableEq; one such ite anywhere in the chain blocks kernel reduction of every order comparison above it.
• Prefer strict-bound sandwiches over equalities with literals.
• Certify every numeric claim externally (exact fractions, mirroring the Lean definitions including fallback semantics) before proving.

def RSA.Score.l0 {U : Type u_1} {W : Type u_2} [Fintype W] (meaning : U → W → Bool) (prior : W → ℚ≥0) (u : U) (w : W) : ℚ≥0

Literal listener: prior conditioned on the meaning's truth, row-wise (÷0 = 0 on utterances true nowhere; speakers complete such rows via their fallback).

Equations

• RSA.Score.l0 meaning prior u w = (if meaning u w = true then prior w else 0) / ∑ w' : W, if meaning u w' = true then prior w' else 0

def RSA.Score.s1 {U : Type u_1} {W : Type u_2} [Fintype U] (l0 : U → W → ℚ≥0) (α : ℕ) (cost : U → ℚ≥0) (fb : PMF.Fallback U) (w : W) : U → ℚ≥0

Speaker scores: (l0 u w)^α · cost u, normalized over utterances and completed by fb on zero-mass rows. α : ℕ keeps the chain in ℚ≥0; cost is the multiplicative cost factor (e.g. a rationalized exp (−C)).

Equations

• RSA.Score.s1 l0 α cost fb w = PMF.scoresWith fb fun (u : U) => l0 u w ^ α * cost u

def RSA.Score.l1Joint {U : Type u_1} {W : Type u_2} {Lat : Type u_3} (prior : W × Lat → ℚ≥0) (s1 : W × Lat → U → ℚ≥0) (u : U) (p : W × Lat) : ℚ≥0

Joint pragmatic-listener scores over world × latent coordinates: prior p · s1 p u. Wrap with PMF.ofScores for the joint listener PMF, or marginalize first.

Equations

• RSA.Score.l1Joint prior s1 u p = prior p * s1 p u

def RSA.Score.worldMarginal {W : Type u_2} {Lat : Type u_3} [Fintype Lat] (f : W × Lat → ℚ≥0) (w : W) : ℚ≥0

World marginal of joint scores.

Equations

• RSA.Score.worldMarginal f w = ∑ l : Lat, f (w, l)

def RSA.Score.latentMarginal {W : Type u_2} {Lat : Type u_3} [Fintype W] (f : W × Lat → ℚ≥0) (l : Lat) : ℚ≥0

Latent marginal of joint scores.

Equations

• RSA.Score.latentMarginal f l = ∑ w : W, f (w, l)

def RSA.Score.s2 {U : Type u_1} {W : Type u_2} {Lat : Type u_3} [Fintype U] (l1World : U → W → ℚ≥0) (l1Lat : U → Lat → ℚ≥0) (α β : ℕ) (cost : U → ℚ≥0) (fb : PMF.Fallback U) (l : Lat) (w : W) : U → ℚ≥0

Stacked speaker: scores over utterances from pragmatic-listener coordinates l1World^α · l1Lat^β · cost, fallback-completed. Higher levels iterate the same shape.

Equations

• RSA.Score.s2 l1World l1Lat α β cost fb l w = PMF.scoresWith fb fun (u : U) => l1World u w ^ α * l1Lat u l ^ β * cost u

Basic lemmas

theorem RSA.Score.l0_le_one {U : Type u_1} {W : Type u_2} [Fintype W] (meaning : U → W → Bool) (prior : W → ℚ≥0) (u : U) (w : W) : l0 meaning prior u w ≤ 1

theorem RSA.Score.l0_eq_zero_of_not_meaning {U : Type u_1} {W : Type u_2} [Fintype W] {meaning : U → W → Bool} {u : U} {w : W} (h : ¬meaning u w = true) (prior : W → ℚ≥0) : l0 meaning prior u w = 0

theorem RSA.Score.s1_sum_eq_one {U : Type u_1} {W : Type u_2} [Fintype U] (l0 : U → W → ℚ≥0) (α : ℕ) (cost : U → ℚ≥0) (fb : PMF.Fallback U) (w : W) : ∑ u : U, s1 l0 α cost fb w u = 1

theorem RSA.Score.worldMarginal_l1Joint_total {U : Type u_1} {W : Type u_2} {Lat : Type u_3} [Fintype W] [Fintype Lat] (prior : W × Lat → ℚ≥0) (s1 : W × Lat → U → ℚ≥0) (u : U) : ∑ w : W, worldMarginal (l1Joint prior s1 u) w = ∑ p : W × Lat, prior p * s1 p u