Partition Refinement Lattice

@cite{groenendijk-stokhof-1984} @cite{merin-1999}

Refinement and coarsening order on partitions (QUD):

• refines (⊑) — Q refines Q' iff Q's equivalence classes are subsets of Q''s. Equivalent to: knowing the Q-answer determines the Q'-answer.
• coarsens — dual of refinement.

Lattice structure

Partitions form a bounded lattice ordered by refinement:

• Meet (* from Core.Question.Partition.QUD): coarsest common refinement.
• Top: exact (finest).
• Bottom: trivial (coarsest).

Antisymmetry holds only up to extensional equivalence of sameAnswer; true propositional antisymmetry would require quotienting.

def QUD.refines {M : Type u_1} (q q' : QUD M) : Prop

Q refines Q' iff Q's equivalence classes are subsets of Q''s.

Intuitively: knowing the Q-answer tells you the Q'-answer. If two elements give the same Q-answer, they must give the same Q'-answer.

Forms a partial order on partitions (up to extensional equivalence).

Equations

• q.refines q' = ∀ (w v : M), q.sameAnswer w v = true → q'.sameAnswer w v = true

def QUD.«term_⊑_» : Lean.TrailingParserDescr

Equations

• QUD.«term_⊑_» = Lean.ParserDescr.trailingNode `QUD.«term_⊑_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊑ ") (Lean.ParserDescr.cat `term 51))

def QUD.coarsens {M : Type u_1} (q q' : QUD M) : Prop

Q coarsens Q' iff Q' refines Q (dual of refinement).

Coarsening merges cells: where Q' distinguishes elements, Q may not. @cite{merin-1999} defines negative attributes in terms of coarsening: negation is the linguistic device that produces coarsenings on the fly.

Equations

• q.coarsens q' = q'.refines q

theorem QUD.refines_refl {M : Type u_1} (q : QUD M) : q.refines q

Refinement is reflexive.

theorem QUD.refines_trans {M : Type u_1} {q1 q2 q3 : QUD M} : q1.refines q2 → q2.refines q3 → q1.refines q3

Refinement is transitive.

theorem QUD.refines_antisymm {M : Type u_1} {q1 q2 : QUD M} : q1.refines q2 → q2.refines q1 → ∀ (w v : M), q1.sameAnswer w v = q2.sameAnswer w v

Refinement is antisymmetric up to extensional equivalence of sameAnswer.

True propositional antisymmetry (q1 = q2) would require quotient types; this is the extensional version.

theorem QUD.all_refine_trivial {M : Type u_1} (q : QUD M) : q.refines trivial

All partitions refine (are coarser than or equal to) the trivial partition.

theorem QUD.compose_refines_left {M : Type u_1} (q1 q2 : QUD M) : (q1 * q2).refines q1

The meet (coarsest common refinement) refines the left factor.

theorem QUD.compose_refines_right {M : Type u_1} (q1 q2 : QUD M) : (q1 * q2).refines q2

The meet (coarsest common refinement) refines the right factor.

theorem QUD.exact_refines_all {M : Type u_1} [BEq M] [LawfulBEq M] (q : QUD M) : exact.refines q

The exact (finest) partition refines all partitions.