Optimal leaf ordering of dendrograms

14 fully proved

Optimal Leaf Ordering

InductiveDendrogram as a leaf-labeled binary tree#✓fully proved

A rooted binary tree whose leaves are labeled by α: the shape of a dendrogram (merge heights are irrelevant for leaf ordering).

inductive Dendrogram (α : Type*) where
  /-- A single object. -/
  | leaf : α → Dendrogram α
  /-- The merge of two clusters. -/
  | node : Dendrogram α → Dendrogram α → Dendrogram α

Used by 11

Used byBar-Joseph–Gifford–Jaakkola dynamic program for leaf ordering · Correctness of the optimal leaf ordering recursion · Leaves of a dendrogram · A dendrogram with m internal nodes has \(2^m\) leaf orders · Number of internal nodes of a dendrogram · Optimal leaf-ordering score with fixed end leaves · Optimal leaf-ordering score · Optimal leaf-ordering score via the dynamic program · Optimal leaf-ordering score is finite · Leaf orderings of a dendrogram · Leaf orders are permutations of the leaves

Dendrogram

DefinitionLeaves of a dendrogram#✓fully proved

The leaves of a dendrogram, left to right.

def leaves : Dendrogram α → List α
  | leaf a => [a]
  | node l r => leaves l ++ leaves r

Uses 1 · Used by 4

Statement usesDendrogram as a leaf-labeled binary tree

Used byBar-Joseph–Gifford–Jaakkola dynamic program for leaf ordering · Correctness of the optimal leaf ordering recursion · Optimal leaf-ordering score via the dynamic program · Leaf orders are permutations of the leaves

DefinitionNumber of internal nodes of a dendrogram#✓fully proved

The number of internal (merge) nodes.

def numInternal : Dendrogram α → ℕ
  | leaf _ => 0
  | node l r => numInternal l + numInternal r + 1

Uses 1 · Used by 2

Statement usesDendrogram as a leaf-labeled binary tree

Used byA dendrogram with m internal nodes has \(2^m\) leaf orders · Optimal leaf-ordering score is finite

DefinitionLeaf orderings of a dendrogram#✓fully proved

The leaf orders obtained by choosing, at each internal node, which child is drawn first. Each choice pattern contributes one entry, so the list has 2 ^ numInternal t entries.

def orderings : Dendrogram α → List (List α)
  | leaf a => [[a]]
  | node l r =>
      (orderings l).flatMap (fun u => (orderings r).map (u ++ ·)) ++
        (orderings r).flatMap (fun v => (orderings l).map (v ++ ·))

Uses 1 · Used by 7

Statement usesDendrogram as a leaf-labeled binary tree

Used byCorrectness of the optimal leaf ordering recursion · A dendrogram with m internal nodes has \(2^m\) leaf orders · Optimal leaf-ordering score with fixed end leaves · Optimal leaf-ordering score · Optimal leaf-ordering score via the dynamic program · Optimal leaf-ordering score is finite · Leaf orders are permutations of the leaves

Optimal Leaf Ordering

DefinitionAdjacent-similarity score of a leaf order#✓fully proved

The score of a leaf order: the sum of the similarities of adjacent leaves.

def adjScore (S : α → α → ℝ) : List α → ℝ
  | a :: b :: t => S a b + adjScore S (b :: t)
  | _ => 0

Used by 5

Used byCorrectness of the optimal leaf ordering recursion · Optimal leaf-ordering score with fixed end leaves · Optimal leaf-ordering score · Optimal leaf-ordering score via the dynamic program · Optimal leaf-ordering score is finite

DefinitionOptimal leaf-ordering score#✓fully proved

The best score among the leaf orders of t (never ⊥: optScore_ne_bot).

noncomputable def optScore (S : α → α → ℝ) (t : Dendrogram α) : WithBot ℝ :=
  ((orderings t).map (adjScore S)).maximum

Uses 3 · Used by 2

Statement usesDendrogram as a leaf-labeled binary tree · Leaf orderings of a dendrogram · Adjacent-similarity score of a leaf order

Used byOptimal leaf-ordering score via the dynamic program · Optimal leaf-ordering score is finite

DefinitionOptimal leaf-ordering score with fixed end leaves#✓fully proved

The best score among the leaf orders of t that start with i and end with j (⊥ if there is none).

noncomputable def optEnds [DecidableEq α] (S : α → α → ℝ) (t : Dendrogram α) (i j : α) :
    WithBot ℝ :=
  (((orderings t).filter (fun o => o.head? = some i ∧ o.getLast? = some j)).map
    (adjScore S)).maximum

Uses 3 · Used by 2

Statement usesDendrogram as a leaf-labeled binary tree · Leaf orderings of a dendrogram · Adjacent-similarity score of a leaf order

Used byCorrectness of the optimal leaf ordering recursion · Optimal leaf-ordering score via the dynamic program

DefinitionJoining two subtree orders at an adjacent leaf pair#✓fully proved

One side of the recursion: the left part ranges over orders of a subtree with leaves Ll and best-score table Ml, the right part over a subtree with leaves Lr and table Mr; the two are joined at the adjacent pair (k, l).

noncomputable def joinEnds (S : α → α → ℝ) (Ml Mr : α → α → WithBot ℝ) (Ll Lr : List α)
    (i j : α) : WithBot ℝ :=
  (Ll.flatMap fun k => Lr.map fun l => Ml i k + ((S k l : ℝ) : WithBot ℝ) + Mr l j).foldr
    max ⊥

Used by 2

Used byBar-Joseph–Gifford–Jaakkola dynamic program for leaf ordering · Correctness of the optimal leaf ordering recursion

DefinitionBar-Joseph–Gifford–Jaakkola dynamic program for leaf ordering#✓fully proved

The dynamic program of Bar-Joseph, Gifford and Jaakkola: bestEnds S t i j is computed from the tables of the two children, trying both child orders.

noncomputable def bestEnds [DecidableEq α] (S : α → α → ℝ) : Dendrogram α → α → α → WithBot ℝ
  | leaf a, i, j => if i = a ∧ j = a then 0 else ⊥
  | node l r, i, j =>
      max (joinEnds S (bestEnds S l) (bestEnds S r) (leaves l) (leaves r) i j)
        (joinEnds S (bestEnds S r) (bestEnds S l) (leaves r) (leaves l) i j)

Uses 3 · Used by 2

Statement usesDendrogram as a leaf-labeled binary tree · Leaves of a dendrogram · Joining two subtree orders at an adjacent leaf pair

Used byCorrectness of the optimal leaf ordering recursion · Optimal leaf-ordering score via the dynamic program

TheoremA dendrogram with m internal nodes has \(2^m\) leaf orders#✓fully proved

A dendrogram with m internal nodes has 2 ^ m leaf orders (one per flip pattern).

theorem length_orderings (t : Dendrogram α) : (orderings t).length = 2 ^ numInternal t

Uses 3 · Used by 1

Statement usesDendrogram as a leaf-labeled binary tree · Number of internal nodes of a dendrogram · Leaf orderings of a dendrogram

Used byOptimal leaf-ordering score is finite

TheoremLeaf orders are permutations of the leaves#✓fully proved

Every leaf order of t is a permutation of its leaves.

theorem perm_of_mem_orderings {t : Dendrogram α} {o : List α} (h : o ∈ orderings t) :
    o.Perm (leaves t)

Uses 3 · Used by 2

Statement usesDendrogram as a leaf-labeled binary tree · Leaves of a dendrogram · Leaf orderings of a dendrogram

Used byCorrectness of the optimal leaf ordering recursion · Optimal leaf-ordering score via the dynamic program

TheoremCorrectness of the optimal leaf ordering recursion#✓fully proved

Correctness of the optimal leaf ordering recursion (Bar-Joseph, Gifford and Jaakkola 2001): the dynamic program computes, for every end pair (i, j), the best score of a leaf order of t starting at i and ending at j.

theorem bestEnds_eq_optEnds [DecidableEq α] (S : α → α → ℝ) (t : Dendrogram α) (i j : α) :
    bestEnds S t i j = optEnds S t i j

Uses 8 · Used by 1

Statement usesDendrogram as a leaf-labeled binary tree · Bar-Joseph–Gifford–Jaakkola dynamic program for leaf ordering · Optimal leaf-ordering score with fixed end leaves

Proof usesLeaves of a dendrogram · Leaf orderings of a dendrogram · Adjacent-similarity score of a leaf order · Joining two subtree orders at an adjacent leaf pair · Leaf orders are permutations of the leaves

Used byOptimal leaf-ordering score via the dynamic program

TheoremOptimal leaf-ordering score via the dynamic program#✓fully proved

The optimal leaf-ordering score is the best bestEnds value over end pairs of leaves.

theorem optScore_eq_sup_bestEnds [DecidableEq α] (S : α → α → ℝ) (t : Dendrogram α) :
    optScore S t =
      ((leaves t).flatMap fun i => (leaves t).map fun j => bestEnds S t i j).foldr max ⊥

Uses 9

Statement usesDendrogram as a leaf-labeled binary tree · Leaves of a dendrogram · Bar-Joseph–Gifford–Jaakkola dynamic program for leaf ordering · Optimal leaf-ordering score

Proof usesLeaf orderings of a dendrogram · Adjacent-similarity score of a leaf order · Correctness of the optimal leaf ordering recursion · Optimal leaf-ordering score with fixed end leaves · Leaf orders are permutations of the leaves

TheoremOptimal leaf-ordering score is finite#✓fully proved

Every dendrogram has a leaf order, so the optimal score is a real number.

theorem optScore_ne_bot (S : α → α → ℝ) (t : Dendrogram α) : optScore S t ≠ ⊥

Uses 6

Statement usesDendrogram as a leaf-labeled binary tree · Optimal leaf-ordering score

Proof usesNumber of internal nodes of a dendrogram · Leaf orderings of a dendrogram · Adjacent-similarity score of a leaf order · A dendrogram with m internal nodes has \(2^m\) leaf orders

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.