Decision-Theoretic Bridge for Partition QUDs #
@cite{merin-1999} @cite{blackwell-1953} @cite{van-rooy-2003}
Decision-theoretic content built on top of the QUD partition lattice
(Core/Partition.lean) and the decision-theory kernel
(Core/Agent/DecisionTheory.lean):
partitionEU— partition-relative expected utility, compositional under coarsening (@cite{merin-1999} central theorem)partitionValue— the Blackwell-style raw weighted valueblackwell_refinement_value— finer partitions are at least as valuableresolution_value_eq_exact— @cite{van-rooy-2003}'s mention-some = mention-all decision-theoretic equivalenceblackwell_characterizes_refinement— the converse: ordering on values IS partition refinementquestionUtility_*bridges connectingCore.DecisionTheory.questionUtilitytopartitionValue, plus non-negativity of QUD-derived utility
Namespace: QUD, for compatibility with existing call sites.
EU Compositionality under Coarsening (@cite{merin-1999}, Central Theorem) #
Expected utility computed via a partition: weight each cell's conditional EU by the cell's probability.
EU_Q(a) = Σ_{c ∈ cells(Q)} P(c) · EU(a | c)
This is the partition-relative expected utility that @cite{merin-1999} shows is
compositional under coarsening. Uses Finpartition for exhaustivity and
disjointness, replacing ~200 lines of custom foldl arithmetic.
Equations
- QUD.partitionEU dp q a = ∑ cell ∈ q.toFinpartition.parts, cell.sum dp.prior * Core.DecisionTheory.conditionalEU dp cell a
Instances For
Cell probability cancellation (Finset version) #
Law of total expectation for partition-relative EU.
The unconditional expected utility equals the partition-relative EU for any partition, because partitions are exhaustive and mutually exclusive.
Uses Finset.sum_biUnion with Finpartition.biUnion_parts for the
decomposition — disjointness and exhaustivity come free from the
Finpartition structure.
Non-negativity is necessary: with prior(w1) = 1, prior(w2) = -1,
utility(w1,a) = 1, utility(w2,a) = 0, and a trivial partition,
expectedUtility = 1 but cellProb = 0 forces partitionEU = 0.
Partition-relative EU is partition-independent (given non-negative priors).
Any two partitions give the same partition-relative EU, because both
equal the unconditional EU (eu_eq_partitionEU).
Blackwell Ordering #
Finset-based partition value #
The value of a decision problem under partition Q over a Finset of worlds.
V_Q(D, W) = Σ_{c ∈ cells(Q,W)} max_a [Σ_{w∈c} p(w)·u(w,a)]
Following @cite{merin-1999}, this uses raw weighted sums directly
rather than factoring through conditional EU. The equivalence
P(c) · max_a condEU(a,c) = max_a [Σ_{w∈c} p(w)·u(w,a)] holds when
priors are non-negative. The raw form makes Blackwell's theorem a
direct application of sub-additivity.
Equations
- QUD.partitionValue dp q worlds actions = ∑ cell ∈ q.toCellsFinset worlds, if h : actions.Nonempty then actions.sup' h fun (a : A) => ∑ w ∈ cell, dp.prior w * dp.utility w a else 0
Instances For
Sub-additivity of max #
Blackwell refinement theorem #
Blackwell's theorem for partitions: finer partitions are always at least as valuable as coarser ones, for any decision problem.
V_Q(D) ≥ V_{Q'}(D) for all decision problems D, whenever Q ⊑ Q'.
Proof: Working directly with raw weighted sums
Σ_{w∈c} p(w)·u(w,a):
- Each coarse cell's sum decomposes into fine cells (
Finset.sum_biUnion) - Sub-additivity of max:
max_a(Σᵢ fᵢ(a)) ≤ Σᵢ max_a(fᵢ(a)) - Regrouping: fine cells grouped by coarse cell = all fine cells
Resolution–Value Saturation #
Resolution–Value Saturation: when every cell of partition Q has a dominant action, Q's partition value equals the exact partition's value.
This is the mathematical core of @cite{van-rooy-2003}: resolving partitions achieve the same value as the finest partition, so coarsening from G&S exhaustive answers to mention-some answers is decision-theoretically free.
Proof: Blackwell gives ≤ (exact refines all). For ≥, the dominant action achieves the pointwise maximum at every world in the cell, making the sub-additivity inequality tight.
Blackwell characterization #
Blackwell ordering characterizes refinement: Q refines Q' if and only if Q is at least as valuable as Q' for every decision problem.
This is the converse of blackwell_refinement_value: if Q is always at
least as valuable, then Q must refine Q'. Together they establish that
partition refinement IS Blackwell ordering.
Proof (contrapositive): Suppose q does not refine q', i.e.,
∃ w v with q.sameAnswer w v = true but q'.sameAnswer w v = false.
Construct a DP over worlds = {w, v} with two actions where distinguishing
w from v matters. Then q' achieves value 1 while q achieves 1/2.
Question Utility Bridge #
Connect Finset-based questionUtility (from Core.DecisionTheory) to
Finset-based partitionValue. The algebraic identity:
questionUtility dp actions (q.toCellsFinset Finset.univ) = partitionValue dp q Finset.univ actions - dpValue dp actions * (Finset.univ : Finset M).sum dp.prior
under non-negative priors. Since dpValue * totalPrior is
partition-independent, the Blackwell ordering on partitionValue
transfers directly to questionUtility.
Per-cell equivalence #
Cells partition Finset.univ #
Main bridge theorem #
Blackwell ordering on questionUtility for QUD-derived questions.
Refinement implies higher question utility (with non-negative priors).
Proof: questionUtility = partitionValue - dpValue × totalPrior.
Since dpValue and totalPrior are partition-independent, the ordering
on partitionValue (from blackwell_refinement_value) transfers.
questionUtility ordering implies partitionValue ordering on Finset.univ.
The identity questionUtility(q) = partitionValue(q, univ) - dpValue × totalPrior
means the partition-independent constant cancels in comparisons.
Partition value restricted to prior support #
When priors are zero outside a subset S, the partition value over the full
universe equals the partition value over S. This bridges from questionUtility
(which operates over Finset.univ) to partitionValue over arbitrary
world sets (needed by blackwell_characterizes_refinement).
Partition value restricted to prior support.
When priors are zero outside S, partitionValue over Finset.univ equals
partitionValue over S. Cells not intersecting S contribute zero (all priors
are 0). Cells intersecting S have the same per-cell value as the S-restricted
cells. The bijection between nonempty-in-S cells and toCellsFinset S
reindexes the sum.
partitionValue depends only on dp.prior and dp.utility within worlds.
If two DPs agree on all worlds in worlds, they produce the same partition value,
because each cell in toCellsFinset worlds is a subset of worlds.
QUD question utility non-negativity #
QUD-derived questionUtility is non-negative under proper priors.
Requires non-negative priors summing to exactly 1 (proper probability).
Proof: questionUtility(q) ≥ questionUtility(trivial) by Blackwell
(questionUtility_refinement_ge + all_refine_trivial).
Then questionUtility(trivial) = 0 because conditioning on the full
universe with totalProb = 1 yields conditionalEU = expectedUtility,
so valueAfterLearning = dpValue and utilityValue = 0.