RSAConfig — Unified RSA Configuration

@cite{degen-2023} @cite{frank-goodman-2012} @cite{bergen-levy-goodman-2016} @cite{kao-etal-2014-hyperbole} @cite{qing-franke-2013}

A streamlined RSA configuration grounded in rational action theory. Each RSA model decomposes into two orthogonal dimensions:

1. What the agent optimizes — the scoring rule (s1Score)
2. What the observer marginalizes over — the latent structure (Latent)

Architecture

All three RSA levels are RationalAction instances:

L0agent(l) : RationalAction U W score(u, w) = meaning(l, u, w)
S1agent(l) : RationalAction W U score(w, u) = s1Score(L0.policy, α, l, w, u)
L1agent : RationalAction U W score(u, w) = prior(w) · Σ_l prior(l|w) · S1(u|w,l)

L0 scores are just the meaning function — any prior the paper wants in L0 is baked into meaning. The empirical worldPrior (object salience, base rates) enters only at L1, keeping L0 fixed under iterated updates.

Latent variables (QUDs, lexicons, thresholds) can enter at two levels:

• L0 (meaning): e.g., lexical uncertainty
• S1 (s1Score): e.g., QUD projection

The s1Score field takes the latent variable l so each paper can specify exactly where its latent variables enter:

Model	meaning uses latent?	s1Score uses latent?
@cite{frank-goodman-2012}	no (Unit)	no (Unit)
@cite{kao-etal-2014-hyperbole} (QUD)	no (ignores q)	yes (cell aggregation)
@cite{bergen-levy-goodman-2016} (lex)	yes (lexicon)	no (standard rpow)

S1 score examples:

• Belief-based (@cite{frank-goodman-2012}): score = rpow(L0(w|u), α). rpow(0,α)=0.
• Action-based (@cite{qing-franke-2013}): score = exp(α · (L0(w|u) - cost(u)))
• QUD-based: score = exp(α · (ln L0(g(s,a)|u) - C(u)))

BToM Grounding (§5)

Every RSAConfig gives rise to a BToM generative model via toBToM. The pragmatic listener (L1) IS a BToM observer: L1_eq_btom_worldMarginal proves that L1's score equals the BToM world marginal. See BToMGrounding.lean for latent classification (Gricean vs channel-theoretic).

noncomputable def RSA.RSAConfig.L0agent_at {U : Type u_1} {W : Type u_2} [Fintype U] [Fintype W] (cfg : RSAConfig U W) (ctx : cfg.Ctx) (l : cfg.Latent) : Core.RationalAction U W

L0 at a specific context (for sequential models).

Scores each world w by meaning(ctx, l, u, w). For one-shot models, use L0agent which fixes ctx = initial.

Equations

• cfg.L0agent_at ctx l = { score := fun (u : U) (w : W) => cfg.meaning ctx l u w, score_nonneg := ⋯ }

noncomputable def RSA.RSAConfig.L0agent {U : Type u_1} {W : Type u_2} [Fintype U] [Fintype W] (cfg : RSAConfig U W) (l : cfg.Latent) : Core.RationalAction U W

L0 as a RationalAction (one per latent value), at initial context.

L0 is the literal listener: given utterance u, score each world w by meaning(initial, l, u, w). The policy gives the normalized posterior L0(w|u, l).

The meaning function IS the score — any prior the paper wants in L0 is baked into meaning, not applied separately. This keeps L0 fixed under iterated prior updates at L1.

Equations

• cfg.L0agent l = { score := fun (u : U) (w : W) => cfg.meaning cfg.initial l u w, score_nonneg := ⋯ }

noncomputable def RSA.RSAConfig.L0 {U : Type u_1} {W : Type u_2} [Fintype U] [Fintype W] (cfg : RSAConfig U W) (l : cfg.Latent) (u : U) (w : W) : ℝ

L0 posterior: P(w|u, l) = meaning(initial,l,u,w) / Σ_w' meaning(initial,l,u,w').

Equations

• cfg.L0 l u w = (cfg.L0agent l).policy u w

noncomputable def RSA.RSAConfig.L0_marginal {U : Type u_1} {W : Type u_2} [Fintype U] [Fintype W] (cfg : RSAConfig U W) (l : cfg.Latent) (u : U) (P : W → Prop) [DecidablePred P] : ℝ

L0 marginal: P(P|u, l) = Σ_{w : P(w)} L0(w|u, l). Sums the L0 posterior over worlds satisfying a decidable predicate.

Equations

• cfg.L0_marginal l u P = ∑ w : W with P w, cfg.L0 l u w

noncomputable def RSA.RSAConfig.S1agent_at {U : Type u_1} {W : Type u_2} [Fintype U] [Fintype W] (cfg : RSAConfig U W) (ctx : cfg.Ctx) (l : cfg.Latent) : Core.RationalAction W U

S1 at a specific context (for sequential models).

Uses L0_at(ctx) as the literal listener, so the speaker's informativity computation reflects the context-dependent meaning.

Equations

• cfg.S1agent_at ctx l = { score := fun (w : W) (u : U) => cfg.s1Score (cfg.L0agent_at ctx l).policy cfg.α l w u, score_nonneg := ⋯ }

noncomputable def RSA.RSAConfig.S1agent {U : Type u_1} {W : Type u_2} [Fintype U] [Fintype W] (cfg : RSAConfig U W) (l : cfg.Latent) : Core.RationalAction W U

S1 as a RationalAction, at initial context.

S1's score is computed by s1Score, which takes L0's normalized posterior, the rationality parameter α, and the latent variable value. The score function is pluggable — different papers provide different scoring rules:

• Belief-based: score = rpow(L0(w|u), α). Correct: rpow(0, α) = 0.
• Action-based: score = exp(α · L0(w|u)).
• QUD-based: score = rpow(qudProject(q, L0(u), w), α).

The latent parameter l enters s1Score so that latent variables like QUDs can affect S1 scoring without being forced into L0's meaning.

Equations

• cfg.S1agent l = { score := fun (w : W) (u : U) => cfg.s1Score (cfg.L0agent l).policy cfg.α l w u, score_nonneg := ⋯ }

noncomputable def RSA.RSAConfig.S1 {U : Type u_1} {W : Type u_2} [Fintype U] [Fintype W] (cfg : RSAConfig U W) (l : cfg.Latent) (w : W) (u : U) : ℝ

S1 policy at initial context: P(u|w, l).

Equations

• cfg.S1 l w u = (cfg.S1agent l).policy w u

noncomputable def RSA.RSAConfig.S1_at {U : Type u_1} {W : Type u_2} [Fintype U] [Fintype W] (cfg : RSAConfig U W) (ctx : cfg.Ctx) (l : cfg.Latent) (w : W) (u : U) : ℝ

S1 policy at a specific context.

Equations

• cfg.S1_at ctx l w u = (cfg.S1agent_at ctx l).policy w u

theorem RSA.RSAConfig.S1_nonneg {U : Type u_1} {W : Type u_2} [Fintype U] [Fintype W] (cfg : RSAConfig U W) (l : cfg.Latent) (w : W) (u : U) : 0 ≤ cfg.S1 l w u

theorem RSA.RSAConfig.S1_sum_eq_one {U : Type u_1} {W : Type u_2} [Fintype U] [Fintype W] (cfg : RSAConfig U W) (l : cfg.Latent) (w : W) (h : (cfg.S1agent l).totalScore w ≠ 0) : ∑ u : U, cfg.S1 l w u = 1

noncomputable def RSA.RSAConfig.L1agent {U : Type u_1} {W : Type u_2} [Fintype U] [Fintype W] (cfg : RSAConfig U W) : Core.RationalAction U W

L1 as a RationalAction.

The pragmatic listener inverts S1 via Bayes' rule, marginalizing over latent variables. Score = prior(w) · Σ_l prior(l|w) · S1(u|w,l).

The empirical worldPrior enters here (not at L0), so L0 stays fixed under iterated prior updates.

In reference games, L1 is choosing a target object. In other settings, L1 is updating beliefs about the world. Either way, the math is the same.

Equations

• cfg.L1agent = { score := fun (u : U) (w : W) => cfg.worldPrior w * ∑ l : cfg.Latent, cfg.latentPrior w l * cfg.S1 l w u, score_nonneg := ⋯ }

noncomputable def RSA.RSAConfig.L1 {U : Type u_1} {W : Type u_2} [Fintype U] [Fintype W] (cfg : RSAConfig U W) (u : U) (w : W) : ℝ

L1 posterior: P(w|u) ∝ prior(w) · Σ_l prior(l) · S1(u|w,l).

Equations

• cfg.L1 u w = cfg.L1agent.policy u w

noncomputable def RSA.RSAConfig.L1_latent {U : Type u_1} {W : Type u_2} [Fintype U] [Fintype W] (cfg : RSAConfig U W) (u : U) (l : cfg.Latent) : ℝ

L1 posterior over latent variables: P(l|u) ∝ Σ_w prior(w) · prior(l|w) · S1(u|w,l).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def RSA.RSAConfig.L1_latent_agent {U : Type u_1} {W : Type u_2} [Fintype U] [Fintype W] (cfg : RSAConfig U W) (u : U) : Core.RationalAction Unit cfg.Latent

L1 latent inference as a RationalAction.

The pragmatic listener's posterior over latent variables, viewed as a Luce choice rule. Score for latent value l is: Σ_w worldPrior(w) · latentPrior(w,l) · S1(l,w,u)

This mirrors L1_latent but packages the computation as a RationalAction, enabling policy_lt_of_score_lt for compositional proofs.

Equations

• cfg.L1_latent_agent u = { score := fun (x : Unit) (l : cfg.Latent) => ∑ w : W, cfg.worldPrior w * cfg.latentPrior w l * cfg.S1 l w u, score_nonneg := ⋯ }

theorem RSA.RSAConfig.L1_latent_eq_policy {U : Type u_1} {W : Type u_2} [Fintype U] [Fintype W] (cfg : RSAConfig U W) (u : U) (l : cfg.Latent) : cfg.L1_latent u l = (cfg.L1_latent_agent u).policy () l

Bridge: L1_latent equals L1_latent_agent.policy.

Both sides unfold to if total = 0 then 0 else score / total with the same score function, so equality is definitional up to unfolding.

theorem RSA.RSAConfig.L1_latent_lt_of_score_lt {U : Type u_1} {W : Type u_2} [Fintype U] [Fintype W] (cfg : RSAConfig U W) (u : U) (l₁ l₂ : cfg.Latent) (h : (cfg.L1_latent_agent u).score () l₁ < (cfg.L1_latent_agent u).score () l₂) : cfg.L1_latent u l₁ < cfg.L1_latent u l₂

Score ordering implies L1_latent ordering. Denominator cancellation for latent comparisons: since L1_latent u l = L1_latent_agent.policy () l, comparing L1_latent reduces to comparing L1_latent_agent scores.

Used by rsa_predict to eliminate the shared normalization constant when comparing L1_latent u l₁ < L1_latent u l₂.

noncomputable def RSA.RSAConfig.L1_marginal {U : Type u_1} {W : Type u_2} [Fintype U] [Fintype W] (cfg : RSAConfig U W) (u : U) (P : W → Prop) [DecidablePred P] : ℝ

L1 marginal: P(P|u) = Σ_{w : P(w)} L1(w|u). Sums the L1 posterior over worlds satisfying a decidable predicate.

Equations

• cfg.L1_marginal u P = ∑ w : W with P w, cfg.L1 u w

theorem RSA.RSAConfig.L1_marginal_lt_of_score_sum_lt {U : Type u_1} {W : Type u_2} [Fintype U] [Fintype W] (cfg : RSAConfig U W) (u : U) (P Q : W → Prop) [DecidablePred P] [DecidablePred Q] (h : (Finset.filter P Finset.univ).sum (cfg.L1agent.score u) < (Finset.filter Q Finset.univ).sum (cfg.L1agent.score u)) : cfg.L1_marginal u P < cfg.L1_marginal u Q

Score-sum ordering implies L1_marginal ordering. Denominator cancellation for marginal comparisons: since all L1(u,w) share the same totalScore(u), comparing marginal sums reduces to comparing score sums.

Used by rsa_predict to eliminate the shared normalization constant when comparing L1_marginal u P < L1_marginal u Q.

noncomputable def RSA.RSAConfig.S2agent {U : Type u_1} {W : Type u_2} [Fintype U] [Fintype W] (cfg : RSAConfig U W) : Core.RationalAction W U

S2 agent: pragmatic speaker conditioning on observed world.

S2 inverts L1 via Bayes' rule over utterances (eq 8, @cite{scontras-pearl-2021}): S2(u|w) ∝ P_{L1}(w|u) = L1(u, w) [the normalized L1 posterior]

Used for endorsement tasks: "would you endorse utterance u given that you observed world w?" This differs from L1 because L1 conditions on the heard utterance (shared denominator across worlds), while S2 conditions on the observed world (different denominator per world).

The score is the normalized L1 posterior P(w|u), not the unnormalized L1 score. This matters: worldPrior enters through L1's normalization denominator, so different worldPriors produce different S2 values.

Equations

• cfg.S2agent = { score := fun (w : W) (u : U) => cfg.L1 u w, score_nonneg := ⋯ }

noncomputable def RSA.RSAConfig.S2 {U : Type u_1} {W : Type u_2} [Fintype U] [Fintype W] (cfg : RSAConfig U W) (w : W) (u : U) : ℝ

S2 policy: P(u|w) = L1(u,w) / Σ_{u'} L1(u',w).

Equations

• cfg.S2 w u = cfg.S2agent.policy w u

theorem RSA.RSAConfig.S2_nonneg {U : Type u_1} {W : Type u_2} [Fintype U] [Fintype W] (cfg : RSAConfig U W) (w : W) (u : U) : 0 ≤ cfg.S2 w u

theorem RSA.RSAConfig.L1_nonneg {U : Type u_1} {W : Type u_2} [Fintype U] [Fintype W] (cfg : RSAConfig U W) (u : U) (w : W) : 0 ≤ cfg.L1 u w

theorem RSA.RSAConfig.L1_latent_nonneg {U : Type u_1} {W : Type u_2} [Fintype U] [Fintype W] (cfg : RSAConfig U W) (u : U) (l : cfg.Latent) : 0 ≤ cfg.L1_latent u l

noncomputable def RSA.RSAConfig.stack {U : Type u_1} {W : Type u_2} [Fintype U] [Fintype W] (cfg : RSAConfig U W) (α₂ : ℝ) (hα₂ : 0 < α₂) (bonus : cfg.Latent → U → ℝ := fun (x : cfg.Latent) (x_1 : U) => 1) (bonus_nonneg : ∀ (l : cfg.Latent) (u : U), 0 ≤ bonus l u := by intros; norm_num) (costFactor : U → ℝ := fun (x : U) => 1) (costFactor_nonneg : ∀ (u : U), 0 ≤ costFactor u := by intros; norm_num) : RSAConfig U W

Build a higher-level RSAConfig from a lower-level one.

The lower-level per-lexicon listener l₁(w|u,L) becomes the new L0 meaning. The new S1 scoring rule applies rpow(l₁(w|u,L), α₂) times an optional bonus (e.g., L₁(L|u)^β for expertise) and costFactor (e.g., exp(-C(u))).

This gives S₂(u|w,L) ∝ l₁(w|u,L)^α₂ · bonus(L,u) · costFactor(u), matching eq 15 of @cite{potts-levy-2015} when bonus = L₁(L|u) and costFactor = exp(-C(u)).

The stacked config's L1 = L₂ (world posterior) and L1_latent = L₂_latent (lexicon posterior), all provable with rsa_predict.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def RSA.RSAConfig.S1_at_nonneg {U : Type u_1} {W : Type u_2} [Fintype U] [Fintype W] (cfg : RSAConfig U W) (ctx : cfg.Ctx) (l : cfg.Latent) (w : W) (u : U) : 0 ≤ cfg.S1_at ctx l w u

S1 probability of producing utterance u in context ctx, for world w and latent value l. This is one step of the sequential chain rule.

Equations

• ⋯ = ⋯

noncomputable def RSA.RSAConfig.trajectoryProbFrom {U : Type u_1} {W : Type u_2} [Fintype U] [Fintype W] (cfg : RSAConfig U W) (ctx : cfg.Ctx) (l : cfg.Latent) (w : W) : List U → ℝ

Trajectory probability starting from an arbitrary context.

Equations

• cfg.trajectoryProbFrom ctx l w [] = 1
• cfg.trajectoryProbFrom ctx l w (u :: us) = cfg.S1_at ctx l w u * cfg.trajectoryProbFrom (cfg.transition ctx u) l w us

noncomputable def RSA.RSAConfig.trajectoryProb {U : Type u_1} {W : Type u_2} [Fintype U] [Fintype W] (cfg : RSAConfig U W) (l : cfg.Latent) (w : W) (traj : List U) : ℝ

Trajectory probability: the probability that S1 produces the sequence traj = [u₁, u₂, ..., uₙ] word-by-word, starting from initial.

S1(traj | w, l) = ∏ⱼ S1_at(ctxⱼ, l, w, uⱼ)

where ctx₀ = initial and ctxⱼ₊₁ = transition(ctxⱼ, uⱼ).

This is the chain rule for incremental production (@cite{cohn-gordon-goodman-potts-2019}, @cite{waldon-degen-2021}).

Equations

• cfg.trajectoryProb l w traj = cfg.trajectoryProbFrom cfg.initial l w traj

theorem RSA.RSAConfig.trajectoryProbFrom_nil {U : Type u_1} {W : Type u_2} [Fintype U] [Fintype W] (cfg : RSAConfig U W) (ctx : cfg.Ctx) (l : cfg.Latent) (w : W) : cfg.trajectoryProbFrom ctx l w [] = 1

theorem RSA.RSAConfig.trajectoryProbFrom_cons {U : Type u_1} {W : Type u_2} [Fintype U] [Fintype W] (cfg : RSAConfig U W) (ctx : cfg.Ctx) (l : cfg.Latent) (w : W) (u : U) (us : List U) : cfg.trajectoryProbFrom ctx l w (u :: us) = cfg.S1_at ctx l w u * cfg.trajectoryProbFrom (cfg.transition ctx u) l w us

theorem RSA.RSAConfig.trajectoryProbFrom_nonneg {U : Type u_1} {W : Type u_2} [Fintype U] [Fintype W] (cfg : RSAConfig U W) (ctx : cfg.Ctx) (l : cfg.Latent) (w : W) (traj : List U) : 0 ≤ cfg.trajectoryProbFrom ctx l w traj

noncomputable def RSA.RSAConfig.L1_action {U : Type u_1} {W : Type u_2} [Fintype U] [Fintype W] (cfg : RSAConfig U W) (αL : ℝ) (u : U) (w : W) : ℝ

Action-oriented listener: applies a second softmax to L1 beliefs.

ρ_a(w | u) = softmax(L1(u, ·), α_L)(w)

Models a listener who soft-maximizes over Bayesian beliefs rather than reporting beliefs directly (@cite{qing-franke-2015}). Provides an additional degree of freedom (α_L) for fitting listener data.

Equations

• cfg.L1_action αL u w = Core.softmax (cfg.L1 u) αL w

theorem RSA.RSAConfig.L1_action_pos {U : Type u_1} {W : Type u_2} [Fintype U] [Fintype W] [Nonempty W] (cfg : RSAConfig U W) (αL : ℝ) (u : U) (w : W) : 0 < cfg.L1_action αL u w

The action-oriented listener always assigns positive probability.

theorem RSA.RSAConfig.L1_action_sum_eq_one {U : Type u_1} {W : Type u_2} [Fintype U] [Fintype W] [Nonempty W] (cfg : RSAConfig U W) (αL : ℝ) (u : U) : ∑ w : W, cfg.L1_action αL u w = 1

The action-oriented listener produces a valid probability distribution.

theorem RSA.RSAConfig.L1_action_amplifies {U : Type u_1} {W : Type u_2} [Fintype U] [Fintype W] [Nonempty W] (cfg : RSAConfig U W) {αL : ℝ} (hα : 0 < αL) (u : U) (w₁ w₂ : W) (h : cfg.L1 u w₁ > cfg.L1 u w₂) : cfg.L1_action αL u w₁ > cfg.L1_action αL u w₂

Higher α_L sharpens the action-oriented listener's distribution: if L1 prefers w₁ over w₂, ρ_a amplifies this preference.

noncomputable def RSA.RSAConfig.toBToM {U : Type u_3} {W : Type u_4} [Fintype U] [Fintype W] (cfg : RSAConfig U W) [DecidableEq W] : Core.BToMModel ℝ U W W cfg.Latent Unit Unit W

Map an RSAConfig to a BToM generative model.

The mapping from RSA to BToM ontology:

• Action = U (utterance)
• Percept = W (speaker perceives the world directly — perfect perception)
• Belief = W (speaker's belief matches the world — perfect knowledge)
• Desire = cfg.Latent (speaker's latent state: goals, interpretations, etc.)
• Shared = Unit (single-utterance models have fixed common ground)
• Medium = Unit (channel properties not separately modeled)
• World = W

The perception/belief chain uses Kronecker deltas [p = w] and [b = p], reflecting the standard RSA assumption that the speaker knows the true world state. RSA's world-conditioned latent prior latentPrior(w, l) maps directly to BToM's world-conditioned desire prior desirePrior(w, d), making the correspondence transparent.

See L1_eq_btom_worldMarginal for the proof that this BToM model's world marginal equals cfg.L1agent.score.

Equations

• One or more equations did not get rendered due to their size.

theorem RSA.RSAConfig.L1_eq_btom_worldMarginal {U : Type u_3} {W : Type u_4} [Fintype U] [Fintype W] [DecidableEq W] (cfg : RSAConfig U W) (u : U) (w : W) : cfg.L1agent.score u w = cfg.toBToM.worldMarginal u w

RSA's pragmatic listener IS BToM world-marginal inference.

L1's score function — worldPrior(w) · Σ_l latentPrior(w,l) · S1(u|w,l) — equals the world marginal of the BToM model constructed by toBToM. This makes RSA's listener a genuine instance of BToM observer inference, not merely an analogy.

Proof sketch: The delta functions in perceptModel and beliefModel collapse the sums over Percept = W and Belief = W to the single term where p = w and b = w. The sums over Shared = Unit and Medium = Unit contribute factor 1. The remaining sum over Desire = Latent matches cfg.L1agent.score by definition of planModel and desirePrior.