Small parsimony problem

AbbreviationMin-plus cost semiring#✓fully proved

The cost semiring: MinTropical (WithTop ℕ), with min as addition and + as multiplication.

abbrev Cost : Type := MinTropical (WithTop ℕ)

Used by 16

Used byFitch parsimony score on a quartet · Rooted quartet with unit costs · Labeling agrees with the observed leaf states · Total substitution cost of a labeling · Sankoff's cost is attained · Fitch's algorithm computes the small-parsimony score · Fitch's root set is the set of optimal root states · Tree with unit costs on every edge · Tropical leaf weights of observed states · Sankoff's algorithm · Sankoff's algorithm computes the small-parsimony cost · Sankoff's cost is a lower bound · Sankoff's recursion at a leaf · Sankoff's recursion at an internal vertex · Unit substitution cost · Tropical weight of a labeling equals its edge cost

16 fully proved

Sankoff's algorithm

DefinitionTotal substitution cost of a labeling#✓fully proved

The total substitution cost of a labeling x of the non-root vertices of t with root state s: the sum over all edges of the cost untrop (P a b) from the parent's state a to the child's state b.

def edgeCost : (t : Tree L S Cost) → S → Labeling t → WithTop ℕ
  | leaf _, _, _ => 0
  | node P l Q r, s, z =>
    (untrop (P s z.1.1) + edgeCost l z.1.1 z.1.2) + (untrop (Q s z.2.1) + edgeCost r z.2.1 z.2.2)

Uses 3 · Used by 4

Statement usesLabeling of the non-root nodes of a tree · Rooted binary tree with transition weights · Min-plus cost semiring

Used bySankoff's cost is attained · Sankoff's algorithm computes the small-parsimony cost · Sankoff's cost is a lower bound · Tropical weight of a labeling equals its edge cost

DefinitionLabeling agrees with the observed leaf states#✓fully proved

The labeling x (with root state s) agrees with the observed states σ at every leaf.

def Agrees (σ : L → S) : (t : Tree L S Cost) → S → Labeling t → Prop
  | leaf l, s, _ => s = σ l
  | node _ l _ r, _, z => Agrees σ l z.1.1 z.1.2 ∧ Agrees σ r z.2.1 z.2.2

Uses 3 · Used by 4

Statement usesLabeling of the non-root nodes of a tree · Rooted binary tree with transition weights · Min-plus cost semiring

Used bySankoff's cost is attained · Sankoff's algorithm computes the small-parsimony cost · Sankoff's cost is a lower bound · Tropical weight of a labeling equals its edge cost

DefinitionTropical leaf weights of observed states#✓fully proved

The leaf weights of the observed states σ: the tropical one (cost 0) at the observed state and the tropical zero (cost ⊤) at every other state.

def leafObs (σ : L → S) (l : L) (s : S) : Cost :=
  if s = σ l then 1 else 0

Uses 1 · Used by 7

Statement usesMin-plus cost semiring

Used byFitch's algorithm computes the small-parsimony score · Fitch's root set is the set of optimal root states · Sankoff's algorithm · Sankoff's algorithm computes the small-parsimony cost · Sankoff's recursion at a leaf · Sankoff's recursion at an internal vertex · Tropical weight of a labeling equals its edge cost

TheoremTropical weight of a labeling equals its edge cost#✓fully proved

The weight of a labeling in the tropical semiring is its edge cost if it agrees with the leaf states and ⊤ otherwise.

theorem untrop_weight (σ : L → S) :
    ∀ (t : Tree L S Cost) (s : S) (x : Labeling t),
      untrop (weight (leafObs σ) t s x) = if Agrees σ t s x then edgeCost t s x else ⊤

Uses 7 · Used by 1

Statement usesLabeling of the non-root nodes of a tree · Rooted binary tree with transition weights · Weight of a tree labeling · Labeling agrees with the observed leaf states · Min-plus cost semiring · Total substitution cost of a labeling · Tropical leaf weights of observed states

Used bySankoff's algorithm computes the small-parsimony cost

DefinitionSankoff's algorithm#✓fully proved

The minimum cost of the subtree t given the state s at its root, computed by Felsenstein's pruning recursion over the tropical semiring.

def sankoff (σ : L → S) (t : Tree L S Cost) (s : S) : WithTop ℕ :=
  untrop (prune (leafObs σ) t s)

Uses 4 · Used by 7

Statement usesRooted binary tree with transition weights · Felsenstein's pruning recursion · Min-plus cost semiring · Tropical leaf weights of observed states

Used bySankoff's cost is attained · Fitch's algorithm computes the small-parsimony score · Fitch's root set is the set of optimal root states · Sankoff's algorithm computes the small-parsimony cost · Sankoff's cost is a lower bound · Sankoff's recursion at a leaf · Sankoff's recursion at an internal vertex

TheoremSankoff's algorithm computes the small-parsimony cost#✓fully proved

sankoff σ t s is the minimum total edge cost over all labelings of the non-root vertices that agree with the observed states at the leaves (with root state s).

theorem sankoff_eq_inf (σ : L → S) (t : Tree L S Cost) (s : S) :
    sankoff σ t s = (Finset.univ.filter (Agrees σ t s)).inf (edgeCost t s)

Sources

• Sankoff (1975).

Uses 12 · Used by 2

Statement usesLabeling of the non-root nodes of a tree · Rooted binary tree with transition weights · Labeling agrees with the observed leaf states · Min-plus cost semiring · Total substitution cost of a labeling · Sankoff's algorithm

Proof usesBrute-force likelihood given the root state · Felsenstein's pruning recursion · Felsenstein's pruning algorithm computes the likelihood conditioned on the root state · Weight of a tree labeling · Tropical leaf weights of observed states · Tropical weight of a labeling equals its edge cost

Used bySankoff's cost is attained · Sankoff's cost is a lower bound

TheoremSankoff's cost is a lower bound#✓fully proved

Sankoff's cost is a lower bound for the cost of every labeling that agrees with the leaf states.

theorem sankoff_le_edgeCost (σ : L → S) (t : Tree L S Cost) (s : S) (x : Labeling t)
    (hx : Agrees σ t s x) : sankoff σ t s ≤ edgeCost t s x

Uses 7

Statement usesLabeling of the non-root nodes of a tree · Rooted binary tree with transition weights · Labeling agrees with the observed leaf states · Min-plus cost semiring · Total substitution cost of a labeling · Sankoff's algorithm

Proof usesSankoff's algorithm computes the small-parsimony cost

TheoremSankoff's cost is attained#✓fully proved

Sankoff's cost is attained: if it is finite, some labeling that agrees with the leaf states has exactly this cost. (It is ⊤ exactly when every agreeing labeling uses a forbidden change, or when t is a single leaf whose observed state is not s.)

theorem exists_edgeCost_eq_sankoff (σ : L → S) (t : Tree L S Cost) (s : S)
    (h : sankoff σ t s ≠ ⊤) : ∃ x, Agrees σ t s x ∧ edgeCost t s x = sankoff σ t s

Uses 7

Statement usesLabeling of the non-root nodes of a tree · Rooted binary tree with transition weights · Labeling agrees with the observed leaf states · Min-plus cost semiring · Total substitution cost of a labeling · Sankoff's algorithm

Proof usesSankoff's algorithm computes the small-parsimony cost

TheoremSankoff's recursion at a leaf#✓fully proved

Sankoff's recursion at a leaf: cost 0 at the observed state, ⊤ elsewhere.

theorem sankoff_leaf (σ : L → S) (l : L) (s : S) :
    sankoff σ (leaf l) s = if s = σ l then 0 else ⊤

Uses 5

Statement usesRooted binary tree with transition weights · Min-plus cost semiring · Sankoff's algorithm

Proof usesFelsenstein's pruning recursion · Tropical leaf weights of observed states

TheoremSankoff's recursion at an internal vertex#✓fully proved

Sankoff's recursion at an internal vertex: the cost of state s is the sum, over the two children, of the minimum over the child's state a of the edge cost from s to a plus the child's cost at a.

theorem sankoff_node (σ : L → S) (P Q : S → S → Cost) (l r : Tree L S Cost) (s : S) :
    sankoff σ (node P l Q r) s =
      Finset.univ.inf (fun a => untrop (P s a) + sankoff σ l a) +
        Finset.univ.inf (fun b => untrop (Q s b) + sankoff σ r b)

Uses 5

Statement usesRooted binary tree with transition weights · Min-plus cost semiring · Sankoff's algorithm

Proof usesFelsenstein's pruning recursion · Tropical leaf weights of observed states

Fitch's algorithm

DefinitionUnit substitution cost#✓fully proved

The unit cost: 0 for no change and 1 for a change of state.

def unitCost (a b : S) : Cost :=
  trop (if a = b then 0 else 1)

Uses 1 · Used by 4

Statement usesMin-plus cost semiring

Used byRooted quartet with unit costs · Fitch's algorithm computes the small-parsimony score · Fitch's root set is the set of optimal root states · Tree with unit costs on every edge

DefinitionTree with unit costs on every edge#✓fully proved

Every edge of the tree carries the unit cost.

def IsUnitCost : Tree L S Cost → Prop
  | leaf _ => True
  | node P l Q r => P = unitCost ∧ Q = unitCost ∧ IsUnitCost l ∧ IsUnitCost r

Uses 3 · Used by 2

Statement usesRooted binary tree with transition weights · Min-plus cost semiring · Unit substitution cost

Used byFitch's algorithm computes the small-parsimony score · Fitch's root set is the set of optimal root states

DefinitionFitch's algorithm#✓fully proved

The set of candidate states at the root of the subtree and the number of changes counted so far. The edge weights of the tree are ignored. Each child is evaluated once per node, so the recursion makes one call per vertex.

def fitch {R : Type w} (σ : L → S) : Tree L S R → Finset S × ℕ
  | leaf l => ({σ l}, 0)
  | node _ l _ r =>
    let a := fitch σ l
    let b := fitch σ r
    if (a.1 ∩ b.1).Nonempty then (a.1 ∩ b.1, a.2 + b.2) else (a.1 ∪ b.1, a.2 + b.2 + 1)

Uses 1 · Used by 3

Statement usesRooted binary tree with transition weights

Used byFitch parsimony score on a quartet · Fitch's algorithm computes the small-parsimony score · Fitch's root set is the set of optimal root states

TheoremFitch's algorithm computes the small-parsimony score#✓fully proved

On a binary tree with unit costs, Fitch's count equals the minimum, over root states, of Sankoff's cost.

theorem fitch_score_eq (σ : L → S) (t : Tree L S Cost) (ht : IsUnitCost t) :
    ((fitch σ t).2 : WithTop ℕ) = Finset.univ.inf (sankoff σ t)

Sources

• Fitch (1971); Hartigan (1973).

Uses 8

Statement usesRooted binary tree with transition weights · Min-plus cost semiring · Tree with unit costs on every edge · Fitch's algorithm · Sankoff's algorithm

Proof usesFelsenstein's pruning recursion · Tropical leaf weights of observed states · Unit substitution cost

TheoremFitch's root set is the set of optimal root states#✓fully proved

On a binary tree with unit costs, a root state is in Fitch's set if and only if Sankoff's cost at that state is the minimum.

theorem fitch_set_eq (σ : L → S) (t : Tree L S Cost) (ht : IsUnitCost t) :
    (fitch σ t).1 = Finset.univ.filter (fun s => sankoff σ t s = (fitch σ t).2)

Sources

• Hartigan (1973).

Uses 8

Statement usesRooted binary tree with transition weights · Min-plus cost semiring · Tree with unit costs on every edge · Fitch's algorithm · Sankoff's algorithm

Proof usesFelsenstein's pruning recursion · Tropical leaf weights of observed states · Unit substitution cost

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.