def RSA.CombinedUtility.combined (lam utilA utilB : ℚ) (cost : ℚ := 0) : ℚ

Combined utility: weighted interpolation of two utility components.

U_combined = (1-λ)·U_A + λ·U_B - cost

This is the standard form used across multiple RSA papers:

• Sumers: U_A = truthfulness, U_B = relevance
• PRIOR-PQ: U_A = informativity, U_B = action-relevance
• Yoon: U_A = informativity, U_B = social utility

Equations

• RSA.CombinedUtility.combined lam utilA utilB cost = (1 - lam) * utilA + lam * utilB - cost

def RSA.CombinedUtility.combinedWeighted (wA wB utilA utilB : ℚ) (cost : ℚ := 0) : ℚ

Alternative parameterization with explicit weights

Equations

• RSA.CombinedUtility.combinedWeighted wA wB utilA utilB cost = wA * utilA + wB * utilB - cost

theorem RSA.CombinedUtility.combined_at_zero (utilA utilB : ℚ) : combined 0 utilA utilB = utilA

Combined utility equals U_A when λ = 0

theorem RSA.CombinedUtility.combined_at_one (utilA utilB : ℚ) : combined 1 utilA utilB = utilB

Combined utility equals U_B when λ = 1

theorem RSA.CombinedUtility.combined_endpoints (utilA utilB : ℚ) : combined 0 utilA utilB = utilA ∧ combined 1 utilA utilB = utilB

Both endpoints in one theorem

theorem RSA.CombinedUtility.combined_cost_additive (lam utilA utilB cost : ℚ) : combined lam utilA utilB cost = combined lam utilA utilB - cost

Cost is additive

theorem RSA.CombinedUtility.combined_mono_A (lam : ℚ) (hlam : lam < 1) (utilA utilA' utilB : ℚ) (h : utilA < utilA') : combined lam utilA utilB < combined lam utilA' utilB

Combined utility increases with U_A when λ < 1

theorem RSA.CombinedUtility.combined_mono_B (lam : ℚ) (hlam : 0 < lam) (utilA utilB utilB' : ℚ) (h : utilB < utilB') : combined lam utilA utilB < combined lam utilA utilB'

Combined utility increases with U_B when λ > 0

theorem RSA.CombinedUtility.combined_convex (lam : ℚ) (hlam0 : 0 ≤ lam) (hlam1 : lam ≤ 1) (utilA utilB : ℚ) : min utilA utilB ≤ combined lam utilA utilB ∧ combined lam utilA utilB ≤ max utilA utilB

Combined utility is a convex combination when λ ∈ [0,1]

theorem RSA.CombinedUtility.combined_midpoint (utilA utilB : ℚ) : combined (1 / 2) utilA utilB = (utilA + utilB) / 2

Midpoint property

theorem RSA.CombinedUtility.lower_lambda_when_A_dominates (lam1 lam2 : ℚ) (h : lam1 < lam2) (utilA utilB : ℚ) (hAB : utilA > utilB) : combined lam1 utilA utilB > combined lam2 utilA utilB

When U_A > U_B, lower λ gives higher combined utility

theorem RSA.CombinedUtility.higher_lambda_when_B_dominates (lam1 lam2 : ℚ) (h : lam1 < lam2) (utilA utilB : ℚ) (hBA : utilB > utilA) : combined lam1 utilA utilB < combined lam2 utilA utilB

When U_B > U_A, higher λ gives higher combined utility

structure RSA.CombinedUtility.MLEFit : Type

Structure for MLE-fitted λ parameters

• lam : ℚ

  Fitted λ value

• condition : String

  Condition name

• logLikelihood : ℚ

  Log-likelihood (approximate)

def RSA.CombinedUtility.moreRelevanceOriented (fit1 fit2 : MLEFit) : Bool

Compare two conditions by their λ values

Equations

• RSA.CombinedUtility.moreRelevanceOriented fit1 fit2 = decide (fit1.lam > fit2.lam)

def RSA.CombinedUtility.moreTruthOriented (fit1 fit2 : MLEFit) : Bool

Compare two conditions by their λ values

Equations

• RSA.CombinedUtility.moreTruthOriented fit1 fit2 = decide (fit1.lam < fit2.lam)

def RSA.CombinedUtility.combined3 (wA wB wC utilA utilB utilC : ℚ) (cost : ℚ := 0) : ℚ

Combined utility with three components (for richer models).

U = w_A · U_A + w_B · U_B + w_C · U_C - cost

Used when there are three competing objectives.

Equations

• RSA.CombinedUtility.combined3 wA wB wC utilA utilB utilC cost = wA * utilA + wB * utilB + wC * utilC - cost

def RSA.CombinedUtility.normalizeWeights3 (wA wB wC : ℚ) : ℚ × ℚ × ℚ

Normalize weights to sum to 1

Equations

• RSA.CombinedUtility.normalizeWeights3 wA wB wC = if (wA + wB + wC == 0) = true then (0, 0, 0) else (wA / (wA + wB + wC), wB / (wA + wB + wC), wC / (wA + wB + wC))

def RSA.CombinedUtility.goalOrientedUtility (uEpi uGoal β : ℚ) : ℚ

Goal-oriented speaker utility: U_epi + β · U_goal.

This parameterization naturally models argumentative/persuasive speakers:

• @cite{barnett-griffiths-hawkins-2022}: U_goal = ln P_L0(w*|u), β controls persuasive bias
• @cite{cummins-franke-2021}: U_goal = argStr(u, G), β → ∞ for pure argStr speaker

Equivalent to combinedWeighted(1, β, U_epi, U_goal). The parameter β controls the cooperativity spectrum:

• β = 0: fully cooperative (standard RSA)
• 0 < β < ∞: partially argumentative
• β → ∞: purely argumentative

Equations

• RSA.CombinedUtility.goalOrientedUtility uEpi uGoal β = uEpi + β * uGoal

theorem RSA.CombinedUtility.goalOriented_eq_combinedWeighted (uEpi uGoal β : ℚ) : goalOrientedUtility uEpi uGoal β = combinedWeighted 1 β uEpi uGoal

Goal-oriented utility = combinedWeighted(1, β,...)

theorem RSA.CombinedUtility.goalOriented_cooperative (uEpi uGoal : ℚ) : goalOrientedUtility uEpi uGoal 0 = uEpi

At β=0, goal-oriented utility reduces to pure epistemic (cooperative RSA)

theorem RSA.CombinedUtility.goalOriented_mono_beta (uEpi uGoal β₁ β₂ : ℚ) (hβ : β₁ < β₂) (hGoal : 0 < uGoal) : goalOrientedUtility uEpi uGoal β₁ < goalOrientedUtility uEpi uGoal β₂

Higher β increases utility of goal-supporting utterances (U_goal > 0)

theorem RSA.CombinedUtility.goalOriented_antimono_beta_neg (uEpi uGoal β₁ β₂ : ℚ) (hβ : β₁ < β₂) (hGoal : uGoal < 0) : goalOrientedUtility uEpi uGoal β₂ < goalOrientedUtility uEpi uGoal β₁

Negative U_goal DECREASES utility as β increases — the speaker is penalized for utterances that argue AGAINST the goal.

def RSA.CombinedUtility.betaToLam (β : ℚ) : ℚ

Convert additive bias parameter β ∈ [0,∞) to convex weight λ ∈ [0,1).

β/(1+β) maps [0,∞) → [0,1): β=0 ↦ 0, β=1 ↦ 1/2, β→∞ ↦ 1.

This bridges goalOrientedUtility (additive: U + β·V) and combined (convex: (1-λ)·U + λ·V).

Equations

• RSA.CombinedUtility.betaToLam β = β / (1 + β)

def RSA.CombinedUtility.lamToBeta (lam : ℚ) : ℚ

Convert convex weight λ ∈ [0,1) back to additive bias parameter β.

λ/(1-λ) maps [0,1) → [0,∞): λ=0 ↦ 0, λ=1/2 ↦ 1.

Equations

• RSA.CombinedUtility.lamToBeta lam = lam / (1 - lam)

theorem RSA.CombinedUtility.betaToLam_lamToBeta_inv (lam : ℚ) (hlam0 : 0 ≤ lam) (hlam1 : lam < 1) : betaToLam (lamToBeta lam) = lam

Round-trip: betaToLam (lamToBeta λ) = λ for λ ∈ [0,1).

theorem RSA.CombinedUtility.lamToBeta_betaToLam_inv (β : ℚ) (hβ : 0 ≤ β) : lamToBeta (betaToLam β) = β

Round-trip: lamToBeta (betaToLam β) = β for β ≥ 0.

theorem RSA.CombinedUtility.goalOriented_eq_scaled_combined (uEpi uGoal β : ℚ) (hβ : 0 ≤ β) : goalOrientedUtility uEpi uGoal β = (1 + β) * combined (betaToLam β) uEpi uGoal

The key bridge: goalOrientedUtility = (1+β) · combined(β/(1+β),...).

U_epi + β·U_goal = (1+β) · ((1 - β/(1+β))·U_epi + β/(1+β)·U_goal)

Scaling by (1+β) > 0 preserves utterance rankings, so the additive and convex forms are strategically equivalent.

theorem RSA.CombinedUtility.goalOriented_same_ranking (uEpi uGoal uEpi' uGoal' β : ℚ) (hβ : 0 ≤ β) (hord : goalOrientedUtility uEpi uGoal β > goalOrientedUtility uEpi' uGoal' β) : combined (betaToLam β) uEpi uGoal > combined (betaToLam β) uEpi' uGoal'

Utterance ranking equivalence: for β ≥ 0, goalOrientedUtility and combined rank any two utility pairs the same way (scaling by (1+β) > 0 preserves ordering).

If U_epi + β·U_goal > U_epi' + β·U_goal', then combined(β/(1+β), U_epi, U_goal) > combined(β/(1+β), U_epi', U_goal').