Response Selection Models for Polar Questions (PRIOR-PQ) (Stub)

@cite{hawkins-etal-2025} @cite{van-rooy-2003}

R0 (literal respondent) selects uniformly among true, safe responses. R1 (pragmatic respondent) uses ToM to infer the questioner's decision problem, then soft-maximizes (1-beta) * informativity + beta * actionRelevance - w_c * cost.

Status

The ℚ-based RSA evaluation infrastructure (RSA.Eval, RSA.Eval.sumScores, RSA.Eval.normalize, RSA.Eval.getScore) has been removed. Type definitions and structural properties (Response, R1UtilityComponents) are preserved. RSA computations (R0, R1, softmax, inferredDP) need to be re-implemented using the new RSAConfig framework.

inductive RSA.Questions.Response : Type

Response to a polar question: taciturn, with-mention, or exhaustive.

• taciturn : Bool → Response
• withMention : Bool → Item → Response
• exhaustive : Bool → List Item → Response

def RSA.Questions.instReprResponse.repr : Response → ℕ → Std.Format

Equations

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

instance RSA.Questions.instReprResponse : Repr Response

Equations

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

instance RSA.Questions.instBEqResponse : BEq Response

Equations

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

def RSA.Questions.Response.answer : Response → Bool

Equations

• (RSA.Questions.Response.taciturn a).answer = a
• (RSA.Questions.Response.withMention a a_1).answer = a
• (RSA.Questions.Response.exhaustive a a_1).answer = a

inductive RSA.Questions.ResponseType : Type

• taciturn : ResponseType
• competitor : ResponseType
• sameCategory : ResponseType
• otherCategory : ResponseType
• exhaustive : ResponseType

instance RSA.Questions.instReprResponseType : Repr ResponseType

Equations

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

def RSA.Questions.instReprResponseType.repr : ResponseType → ℕ → Std.Format

Equations

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

instance RSA.Questions.instDecidableEqResponseType : DecidableEq ResponseType

Equations

• RSA.Questions.instDecidableEqResponseType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance RSA.Questions.instBEqResponseType : BEq ResponseType

Equations

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

def RSA.Questions.instBEqResponseType.beq : ResponseType → ResponseType → Bool

Equations

• RSA.Questions.instBEqResponseType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def RSA.Questions.classifyResponse (r : Response) (targetCategory : ℕ) : ResponseType

Equations

• One or more equations did not get rendered due to their size.
• RSA.Questions.classifyResponse (RSA.Questions.Response.taciturn a) targetCategory = RSA.Questions.ResponseType.taciturn
• RSA.Questions.classifyResponse (RSA.Questions.Response.exhaustive a a_1) targetCategory = RSA.Questions.ResponseType.exhaustive

def RSA.Questions.responseTruth (r : Response) (w : World) : Bool

A response is true iff its answer matches the world and mentioned items exist.

Equations

• RSA.Questions.responseTruth (RSA.Questions.Response.taciturn a) w = (a == w.targetAvailable)
• RSA.Questions.responseTruth (RSA.Questions.Response.withMention a a_1) w = (a == w.targetAvailable && w.alternatives.contains a_1)
• RSA.Questions.responseTruth (RSA.Questions.Response.exhaustive a a_1) w = (a == w.targetAvailable && a_1.all fun (i : RSA.Questions.Item) => w.alternatives.contains i)

def RSA.Questions.responseCost (r : Response) : ℚ

Equations

• RSA.Questions.responseCost (RSA.Questions.Response.taciturn a) = 1
• RSA.Questions.responseCost (RSA.Questions.Response.withMention a a_1) = 2
• RSA.Questions.responseCost (RSA.Questions.Response.exhaustive a a_1) = 1 + ↑a_1.length

def RSA.Questions.isSafe (_r : Response) : Bool

Equations

• RSA.Questions.isSafe _r = true

def RSA.Questions.r0Prob (w : World) (responses : List Response) (r : Response) : ℚ

R0: literal respondent. Uniform over true, safe responses.

Equations

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

def RSA.Questions.r0Dist (w : World) (responses : List Response) : List (Response × ℚ)

Equations

• RSA.Questions.r0Dist w responses = List.map (fun (r : RSA.Questions.Response) => (r, RSA.Questions.r0Prob w responses r)) responses

theorem RSA.Questions.r0_grounds_pragmatics (w : World) (responses : List Response) (r : Response) : r0Prob w responses r > 0 → responseTruth r w = true

R0 only assigns probability to true responses.

def RSA.Questions.informativity (r : Response) (w : World) (responses : List Response) : ℚ

Simple informativity: inverse of true-response count.

Equations

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

structure RSA.Questions.R1UtilityComponents : Type

R1 utility decomposition into components.

• informativity : ℚ
• actionRelevance : ℚ
• cost : ℚ
• total : ℚ

def RSA.Questions.instReprR1UtilityComponents.repr : R1UtilityComponents → ℕ → Std.Format

Equations

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

instance RSA.Questions.instReprR1UtilityComponents : Repr R1UtilityComponents

Equations

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

theorem RSA.Questions.higher_utility_preferred (i1 i2 : Item) (h : i1.utility > i2.utility) : i1.utility > i2.utility

theorem RSA.Questions.cost_increases_with_length (items : List Item) : responseCost (Response.exhaustive false items) = 1 + ↑items.length

theorem RSA.Questions.taciturn_minimal_cost : responseCost (Response.taciturn false) = 1

theorem RSA.Questions.taciturn_yes_minimal_cost : responseCost (Response.taciturn true) = 1