Merin (1999): Negative Attributes, Partitions, and Rational Decisions

Merin argues that attribute spaces are partitions for decision-theoretic reasons and characterizes negative attributes epistemically, as proper coarsenings, rather than by their form. The complements of a partition's cells form a partition, and their probabilities a distribution, only when the partition has two cells. The partition of a cell and its complement is the coarsest coarsening that decides the cell, and an attribute is negative when its complement is a cell and its two-cell partition properly coarsens the partition.

Main statements

• compl_isPartition_iff: the complements of the cells form a partition exactly for two cells.
• sum_measureReal_compl, sum_measureReal_compl_eq_one_iff: the complement probabilities sum to one less than the number of cells, and to one exactly for two cells.
• isGreatest_polar_cell: a cell and its complement give the coarsest coarsening deciding it.
• integral_eq_partitionEU, partitionEU_congr: expected utility computed cell by cell does not depend on the partition.

Implementation notes

Coarsening is the refinement order on Setoid. Expected utility integrates a utility against a prior measure independent of the act; the paper's computation for coarsenings uses Jeffrey's form, with probabilities conditional on the act.

TODO

The paper's point that under a coarsening each coarse cell's term is the sum of the terms of the finer cells it contains, and FACT 5, that re-coverings which neither coarsen nor refine admit no such regrouping, are not formalized; nor is the conditional-independence result of [Joh86] that the paper cites.

References

• [Mer99c]
• [Joh86]

FACT 1: complement families

theorem Merin1999b.compl_isPartition_iff {W : Type u_1} [Nonempty W] {F : Set (Set W)} (hF : Setoid.IsPartition F) : Setoid.IsPartition (compl '' F) ↔ F.encard = 2

The complements of the cells of a partition of a nonempty type form a partition exactly when it has two cells (FACT 1 of [Mer99c]).

FACTs 2 and 3: complement probabilities

theorem Merin1999b.sum_measureReal_compl {M : Type u_1} [MeasurableSpace M] (μ : MeasureTheory.Measure M) [MeasureTheory.IsProbabilityMeasure μ] {F : Finset (Set M)} (hF : Setoid.IsPartition ↑F) (hm : ∀ c ∈ F, MeasurableSet c) : ∑ c ∈ F, μ.real cᶜ = ↑F.card - 1

Under a probability measure the probabilities of the complements of the n cells of a finite partition sum to n − 1 (FACT 3 of [Mer99c]).

theorem Merin1999b.sum_measureReal_compl_eq_one_iff {M : Type u_1} [MeasurableSpace M] (μ : MeasureTheory.Measure M) [MeasureTheory.IsProbabilityMeasure μ] {F : Finset (Set M)} (hF : Setoid.IsPartition ↑F) (hm : ∀ c ∈ F, MeasurableSet c) : ∑ c ∈ F, μ.real cᶜ = 1 ↔ F.card = 2

The complement probabilities sum to one exactly when the partition has two cells, so for more than two cells they are not a distribution (FACTs 2 and 3 of [Mer99c]).

Coarsening and negative attributes

def Merin1999b.IsProperCoarsening {M : Type u_1} (q q' : Setoid M) : Prop

Q properly coarsens Q' when it is strictly coarser in the refinement order, which over a finite domain means coarsening with strictly fewer cells ([Mer99c]).

Equations

• Merin1999b.IsProperCoarsening q q' = (q' < q)

theorem Merin1999b.isGreatest_polar_cell {M : Type u_1} (q : Setoid M) (w : M) : IsGreatest {q' : Setoid M | q ≤ q' ∧ q'.Decides (q.cell w)} (Setoid.polar (q.cell w))

For a cell P of a partition, the partition {P, ¬P} is its coarsest coarsening that decides P (FACT 4 of [Mer99c]).

def Merin1999b.IsNegativeAttribute {M : Type u_1} (R : Set M) (q : Setoid M) : Prop

An attribute R is negative with respect to q when the complement of R is a cell of q and the partition {R, ¬R} properly coarsens q ([Mer99c]).

Equations

• Merin1999b.IsNegativeAttribute R q = ((∃ (w : M), q.cell w = Rᶜ) ∧ Merin1999b.IsProperCoarsening (Setoid.polar R) q)

EU compositionality under coarsening

noncomputable def Merin1999b.partitionEU {M : Type u_1} {A : Type u_2} [Fintype M] [DecidableEq M] [MeasurableSpace M] (μ : MeasureTheory.Measure M) (U : M → A → ℝ) (q : Setoid M) [DecidableRel ⇑q] (a : A) : ℝ

The expected utility of an act computed through a partition weights each cell's conditional expected utility by the cell's probability.

Equations

• Merin1999b.partitionEU μ U q a = ∑ cell ∈ (Finpartition.ofSetoid q).parts, μ.real ↑cell * ∫ (m : M), U m a ∂μ[|↑cell]

theorem Merin1999b.integral_eq_partitionEU {M : Type u_1} {A : Type u_2} [Fintype M] [DecidableEq M] [MeasurableSpace M] [DiscreteMeasurableSpace M] [Nonempty M] (μ : MeasureTheory.Measure M) [MeasureTheory.IsProbabilityMeasure μ] (U : M → A → ℝ) (q : Setoid M) [DecidableRel ⇑q] (a : A) : ∫ (m : M), U m a ∂μ = partitionEU μ U q a

Expected utility computed through any partition is the expected utility.

theorem Merin1999b.partitionEU_congr {M : Type u_1} {A : Type u_2} [Fintype M] [DecidableEq M] [MeasurableSpace M] [DiscreteMeasurableSpace M] [Nonempty M] (μ : MeasureTheory.Measure M) [MeasureTheory.IsProbabilityMeasure μ] (U : M → A → ℝ) (q q' : Setoid M) [DecidableRel ⇑q] [DecidableRel ⇑q'] (a : A) : partitionEU μ U q a = partitionEU μ U q' a

Expected utility computed through a partition does not depend on the partition.