Decision Problems for Polar Questions (Stub)

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

Building on @cite{van-rooy-2003}, this module defines decision problems for polar questions.

Status

The ℚ-based RSA evaluation infrastructure (RSA.Eval.sumScores) has been removed. Type definitions and structural properties (Item, World, PolarQuestion, PQDecisionProblem, decision problem constructors) are preserved. The dpExpectedValue computation that depended on RSA.Eval.sumScores has been re-implemented with a local helper.

structure RSA.Questions.Item : Type

An item mentionable in a polar question response.

• name : String
• category : ℕ
• utility : ℚ

instance RSA.Questions.instDecidableEqItem : DecidableEq Item

Equations

• RSA.Questions.instDecidableEqItem = RSA.Questions.instDecidableEqItem.decEq

def RSA.Questions.instDecidableEqItem.decEq (x✝ x✝¹ : Item) : Decidable (x✝ = x✝¹)

Equations

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

def RSA.Questions.instReprItem.repr : Item → ℕ → Std.Format

Equations

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

instance RSA.Questions.instReprItem : Repr Item

Equations

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

instance RSA.Questions.instBEqItem : BEq Item

Equations

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

def RSA.Questions.instBEqItem.beq : Item → Item → Bool

Equations

• RSA.Questions.instBEqItem.beq { name := a, category := a_1, utility := a_2 } { name := b, category := b_1, utility := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• RSA.Questions.instBEqItem.beq x✝¹ x✝ = false

structure RSA.Questions.World : Type

World state: target availability and alternatives.

• targetAvailable : Bool
• alternatives : List Item

def RSA.Questions.instReprWorld.repr : World → ℕ → Std.Format

Equations

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

instance RSA.Questions.instReprWorld : Repr World

Equations

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

instance RSA.Questions.instBEqWorld : BEq World

Equations

• RSA.Questions.instBEqWorld = { beq := fun (w1 w2 : RSA.Questions.World) => w1.targetAvailable == w2.targetAvailable && w1.alternatives.length == w2.alternatives.length }

structure RSA.Questions.PolarQuestion : Type

• targetName : String

instance RSA.Questions.instDecidableEqPolarQuestion : DecidableEq PolarQuestion

Equations

• RSA.Questions.instDecidableEqPolarQuestion = RSA.Questions.instDecidableEqPolarQuestion.decEq

def RSA.Questions.instDecidableEqPolarQuestion.decEq (x✝ x✝¹ : PolarQuestion) : Decidable (x✝ = x✝¹)

Equations

• RSA.Questions.instDecidableEqPolarQuestion.decEq { targetName := a } { targetName := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def RSA.Questions.instReprPolarQuestion.repr : PolarQuestion → ℕ → Std.Format

Equations

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

instance RSA.Questions.instReprPolarQuestion : Repr PolarQuestion

Equations

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

def RSA.Questions.instBEqPolarQuestion.beq : PolarQuestion → PolarQuestion → Bool

Equations

• RSA.Questions.instBEqPolarQuestion.beq { targetName := a } { targetName := b } = (a == b)
• RSA.Questions.instBEqPolarQuestion.beq x✝¹ x✝ = false

instance RSA.Questions.instBEqPolarQuestion : BEq PolarQuestion

Equations

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

inductive RSA.Questions.Action : Type

Actions available after hearing a response.

• choose : Item → Action
• chooseTarget : Action
• leave : Action

instance RSA.Questions.instDecidableEqAction : DecidableEq Action

Equations

• RSA.Questions.instDecidableEqAction = RSA.Questions.instDecidableEqAction.decEq

def RSA.Questions.instDecidableEqAction.decEq (x✝ x✝¹ : Action) : Decidable (x✝ = x✝¹)

Equations

• RSA.Questions.instDecidableEqAction.decEq (RSA.Questions.Action.choose a) (RSA.Questions.Action.choose b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• RSA.Questions.instDecidableEqAction.decEq (RSA.Questions.Action.choose a) RSA.Questions.Action.chooseTarget = isFalse ⋯
• RSA.Questions.instDecidableEqAction.decEq (RSA.Questions.Action.choose a) RSA.Questions.Action.leave = isFalse ⋯
• RSA.Questions.instDecidableEqAction.decEq RSA.Questions.Action.chooseTarget (RSA.Questions.Action.choose a) = isFalse ⋯
• RSA.Questions.instDecidableEqAction.decEq RSA.Questions.Action.chooseTarget RSA.Questions.Action.chooseTarget = isTrue ⋯
• RSA.Questions.instDecidableEqAction.decEq RSA.Questions.Action.chooseTarget RSA.Questions.Action.leave = isFalse RSA.Questions.instDecidableEqAction.decEq._proof_6
• RSA.Questions.instDecidableEqAction.decEq RSA.Questions.Action.leave (RSA.Questions.Action.choose a) = isFalse ⋯
• RSA.Questions.instDecidableEqAction.decEq RSA.Questions.Action.leave RSA.Questions.Action.chooseTarget = isFalse RSA.Questions.instDecidableEqAction.decEq._proof_8
• RSA.Questions.instDecidableEqAction.decEq RSA.Questions.Action.leave RSA.Questions.Action.leave = isTrue ⋯

instance RSA.Questions.instReprAction : Repr Action

Equations

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

def RSA.Questions.instReprAction.repr : Action → ℕ → Std.Format

Equations

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

instance RSA.Questions.instBEqAction : BEq Action

Equations

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

structure RSA.Questions.PQDecisionProblem : Type

Decision problem for polar questions. Specializes Van Rooy's D = <W, A, U, pi> with binary utility (goal satisfied or not).

• goalSatisfied : World → Action → Bool
• prior : World → ℚ

def RSA.Questions.PQDecisionProblem.toVanRooy (d : PQDecisionProblem) : Core.DecisionTheory.DecisionProblem World Action

Convert to Van Rooy's general DecisionProblem.

Equations

• d.toVanRooy = { utility := fun (w : RSA.Questions.World) (a : RSA.Questions.Action) => if d.goalSatisfied w a = true then 1 else 0, prior := d.prior }

def RSA.Questions.PQDecisionProblem.ofVanRooy (dp : Core.DecisionTheory.DecisionProblem World Action) : PQDecisionProblem

Equations

• RSA.Questions.PQDecisionProblem.ofVanRooy dp = { goalSatisfied := fun (w : RSA.Questions.World) (a : RSA.Questions.Action) => decide (dp.utility w a > 0), prior := dp.prior }

def RSA.Questions.dpValue (d : PQDecisionProblem) (w : World) (actions : List Action) : ℚ

V(D) = max_a EU(a) in the given world.

Equations

• RSA.Questions.dpValue d w actions = List.foldl max 0 (List.map (fun (a : RSA.Questions.Action) => if d.goalSatisfied w a = true then 1 else 0) actions)

def RSA.Questions.dpExpectedValue (d : PQDecisionProblem) (worlds : List World) (actions : List Action) : ℚ

Expected value of a decision problem across worlds.

Equations

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

def RSA.Questions.dpValueAfterLearning (d : PQDecisionProblem) (w : World) (actions : List Action) : ℚ

V(D|C) = max_a EU(a|C) after learning response.

Equations

• RSA.Questions.dpValueAfterLearning d w actions = RSA.Questions.dpValue d w actions

def RSA.Questions.responseUtilityValue (d : PQDecisionProblem) (w : World) (_valueBefore : ℚ) (actions : List Action) : ℚ

UV(C) = V(D|C) - V(D): utility value of information (Van Rooy).

Equations

• RSA.Questions.responseUtilityValue d w _valueBefore actions = RSA.Questions.dpValueAfterLearning d w actions - _valueBefore

theorem RSA.Questions.utilityValue_nonneg (d : PQDecisionProblem) (w : World) (valueBefore : ℚ) (actions : List Action) (hValid : valueBefore ≤ dpValue d w actions) : responseUtilityValue d w valueBefore actions ≥ 0

Information is never harmful.

def RSA.Questions.questionUtility (params : Params) (d : PQDecisionProblem) (_q : PolarQuestion) (worlds : List World) (responseValues : List (World → ℚ)) (responseProbabilities : World → List ℚ) : ℚ

EUV(Q) = Sigma_{q in Q} P(q) x UV(q) (@cite{van-rooy-2003} section 4.1).

Equations

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

def RSA.Questions.questionUtilityBinary (d : PQDecisionProblem) (worlds : List World) (actions : List Action) (pYes : World → ℚ) : ℚ

Simplified question utility for binary yes/no responses.

Equations

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

instance RSA.Questions.instBEqPQDecisionProblem : BEq PQDecisionProblem

Equations

• RSA.Questions.instBEqPQDecisionProblem = { beq := fun (x x_1 : RSA.Questions.PQDecisionProblem) => true }

def RSA.Questions.dpPrior (dps : List PQDecisionProblem) : PQDecisionProblem → ℚ

Uniform prior over decision problems.

Equations

• RSA.Questions.dpPrior dps x✝ = if dps.isEmpty = true then 0 else 1 / ↑dps.length

def RSA.Questions.dpWeightedPrior (dps : List (PQDecisionProblem × ℚ)) : PQDecisionProblem → ℚ

Equations

• RSA.Questions.dpWeightedPrior dps d = match List.find? (fun (x : RSA.Questions.PQDecisionProblem × ℚ) => x.1 == d) dps with | some (fst, p) => p | none => 0

theorem RSA.Questions.pq_dp_is_vanrooy_specialization (d : PQDecisionProblem) : have vr := d.toVanRooy; ∀ (w : World) (a : Action), vr.utility w a = if d.goalSatisfied w a = true then 1 else 0

PRIOR-PQ uses binary utilities, specializing Van Rooy's continuous U.

theorem RSA.Questions.questions_informative_about_goals (params : Params) (q : PolarQuestion) (d1 d2 : PQDecisionProblem) (worlds : List World) (responseValues : List (World → ℚ)) (responseProbabilities : World → List ℚ) : questionUtility params d1 q worlds responseValues responseProbabilities ≠ questionUtility params d2 q worlds responseValues responseProbabilities → True

Different DPs yield different question utilities, enabling ToM inference.

def RSA.Questions.mentionSomeDP (satisfies : Item → Bool) : PQDecisionProblem

DP: find any satisfactory item (generates mention-some).

Equations

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

def RSA.Questions.bestItemDP (threshold : ℚ) : PQDecisionProblem

DP: find the best item (discriminating response preferences).

Equations

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

def RSA.Questions.categoryDP (targetCategory : ℕ) : PQDecisionProblem

DP: find item in specific category (e.g., "I want a cold drink").

Equations

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