RSA Questions: Shared Infrastructure (Stub)

@cite{groenendijk-stokhof-1984} @cite{hawkins-etal-2025} @cite{van-rooy-2003}

Shared infrastructure for RSA models of question-answer pragmatics.

Status

The ℚ-based RSA evaluation infrastructure (RSA.Eval, RSA.Eval.sumScores, RSA.Eval.normalize, RSA.Eval.getScore) has been removed. This file retains type definitions and structural properties that do not depend on the old API. RSA question-answer computations need to be re-implemented using the new RSAConfig framework.

def RSA.Questions.expectedValue {α : Type} (f : α → ℚ) (dist : List (α × ℚ)) : ℚ

Expected value of a distribution

Equations

• RSA.Questions.expectedValue f dist = List.foldl (fun (acc : ℚ) (x : α × ℚ) => match x with | (a, p) => acc + f a * p) 0 dist

structure RSA.Questions.Params : Type

RSA question-answer model parameters.

• αQ : ℚ

  Questioner rationality

• αR : ℚ

  Respondent rationality

• β : ℚ

  Action-relevance weight: 0 = informativity, 1 = action-relevance

• costWeight : ℚ

  Response cost weight

instance RSA.Questions.instReprParams : Repr Params

Equations

• RSA.Questions.instReprParams = { reprPrec := RSA.Questions.instReprParams.repr }

def RSA.Questions.instReprParams.repr : Params → ℕ → Std.Format

Equations

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

instance RSA.Questions.instBEqParams : BEq Params

Equations

• RSA.Questions.instBEqParams = { beq := RSA.Questions.instBEqParams.beq }

def RSA.Questions.instBEqParams.beq : Params → Params → Bool

Equations

• RSA.Questions.instBEqParams.beq { αQ := a, αR := a_1, β := a_2, costWeight := a_3 } { αQ := b, αR := b_1, β := b_2, costWeight := b_3 } = (a == b && (a_1 == b_1 && (a_2 == b_2 && a_3 == b_3)))
• RSA.Questions.instBEqParams.beq x✝¹ x✝ = false

def RSA.Questions.defaultParams : Params

Default parameters

Equations

• RSA.Questions.defaultParams = { }

def RSA.Questions.pureInformativityParams : Params

Equations

• RSA.Questions.pureInformativityParams = { αQ := RSA.Questions.defaultParams.αQ, αR := RSA.Questions.defaultParams.αR, β := 0, costWeight := RSA.Questions.defaultParams.costWeight }

def RSA.Questions.pureActionRelevanceParams : Params

Equations

• RSA.Questions.pureActionRelevanceParams = { αQ := RSA.Questions.defaultParams.αQ, αR := RSA.Questions.defaultParams.αR, β := 1, costWeight := RSA.Questions.defaultParams.costWeight }

inductive RSA.Questions.GenericResponse (Info : Type) : Type

Generic response type: taciturn, elaborated, or exhaustive.

• taciturn {Info : Type} : Bool → GenericResponse Info
• withInfo {Info : Type} : Bool → Info → GenericResponse Info
• exhaustive {Info : Type} : Bool → List Info → GenericResponse Info

instance RSA.Questions.instReprGenericResponse {Info✝ : Type} [Repr Info✝] : Repr (GenericResponse Info✝)

Equations

• RSA.Questions.instReprGenericResponse = { reprPrec := RSA.Questions.instReprGenericResponse.repr }

def RSA.Questions.instReprGenericResponse.repr {Info✝ : Type} [Repr Info✝] : GenericResponse Info✝ → ℕ → Std.Format

Equations

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

def RSA.Questions.GenericResponse.answer {Info : Type} : GenericResponse Info → Bool

Equations

• (RSA.Questions.GenericResponse.taciturn a).answer = a
• (RSA.Questions.GenericResponse.withInfo a a_1).answer = a
• (RSA.Questions.GenericResponse.exhaustive a a_1).answer = a

def RSA.Questions.GenericResponse.cost {Info : Type} (r : GenericResponse Info) : ℚ

Equations

• (RSA.Questions.GenericResponse.taciturn a).cost = 1
• (RSA.Questions.GenericResponse.withInfo a a_1).cost = 2
• (RSA.Questions.GenericResponse.exhaustive a a_1).cost = 1 + ↑a_1.length

def RSA.Questions.informationValue (valueBefore valueAfter : ℚ) : ℚ

Van Rooy's UV(C) = V(D|C) - V(D).

Equations

• RSA.Questions.informationValue valueBefore valueAfter = valueAfter - valueBefore

def RSA.Questions.basicInformativity (responseSetSize : ℕ) : ℚ

Informativity as inverse of response set size.

Equations

• RSA.Questions.basicInformativity responseSetSize = if (responseSetSize == 0) = true then 0 else 1 / ↑responseSetSize

theorem RSA.Questions.beta_tradeoff (params : Params) : params.β = 0 → 1 - params.β = 1 ∧ params.β = 0

beta = 0 yields pure informativity.

inductive RSA.Questions.RSALevel : Type

RSA iteration level.

Track the depth of pragmatic reasoning:

• L0 = literal listener
• S1 = pragmatic speaker (responds to L0)
• L1 = pragmatic listener (responds to S1)

• L : ℕ → RSALevel
• S : ℕ → RSALevel

def RSA.Questions.instDecidableEqRSALevel.decEq (x✝ x✝¹ : RSALevel) : Decidable (x✝ = x✝¹)

Equations

• RSA.Questions.instDecidableEqRSALevel.decEq (RSA.Questions.RSALevel.L a) (RSA.Questions.RSALevel.L b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• RSA.Questions.instDecidableEqRSALevel.decEq (RSA.Questions.RSALevel.L a) (RSA.Questions.RSALevel.S a_1) = isFalse ⋯
• RSA.Questions.instDecidableEqRSALevel.decEq (RSA.Questions.RSALevel.S a) (RSA.Questions.RSALevel.L a_1) = isFalse ⋯
• RSA.Questions.instDecidableEqRSALevel.decEq (RSA.Questions.RSALevel.S a) (RSA.Questions.RSALevel.S b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

instance RSA.Questions.instDecidableEqRSALevel : DecidableEq RSALevel

Equations

• RSA.Questions.instDecidableEqRSALevel = RSA.Questions.instDecidableEqRSALevel.decEq

instance RSA.Questions.instBEqRSALevel : BEq RSALevel

Equations

• RSA.Questions.instBEqRSALevel = { beq := RSA.Questions.instBEqRSALevel.beq }

def RSA.Questions.instBEqRSALevel.beq : RSALevel → RSALevel → Bool

Equations

• RSA.Questions.instBEqRSALevel.beq (RSA.Questions.RSALevel.L a) (RSA.Questions.RSALevel.L b) = (a == b)
• RSA.Questions.instBEqRSALevel.beq (RSA.Questions.RSALevel.S a) (RSA.Questions.RSALevel.S b) = (a == b)
• RSA.Questions.instBEqRSALevel.beq x✝¹ x✝ = false

instance RSA.Questions.instReprRSALevel : Repr RSALevel

Equations

• RSA.Questions.instReprRSALevel = { reprPrec := RSA.Questions.instReprRSALevel.repr }

def RSA.Questions.instReprRSALevel.repr : RSALevel → ℕ → Std.Format

Equations

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