Felsenstein's pruning algorithm

InductiveRooted binary tree with transition weights#✓fully proved

A rooted binary tree with leaf labels L; an internal node node P l Q r carries the transition weights P and Q (from the node's state to the child's state) on the edges to its left child l and right child r.

inductive Tree (L : Type u) (S : Type v) (R : Type w) where
  /-- A leaf with label `l`. -/
  | leaf : L → Tree L S R
  /-- An internal node with transition weights `P` to the left child and `Q` to the right one. -/
  | node : (S → S → R) → Tree L S R → (S → S → R) → Tree L S R → Tree L S R

Used by 62

Used byBrute-force likelihood given the root state · Brute-force likelihood at a leaf · Brute-force likelihood factors over subtrees · Number of labelings of a tree · Labeling of the non-root nodes of a tree · Site likelihood of a phylogenetic tree · The site likelihood by pruning · Site likelihood from tabulated partial likelihoods · Number of internal nodes of a tree · Number of leaves of a tree · Felsenstein's pruning recursion · Felsenstein's pruning algorithm computes the likelihood conditioned on the root state · Tabulated Felsenstein pruning algorithm · Tabulated pruning computes the pruning recursion · Independent sites · Weight of a tree labeling · Likelihood of Pupko's joint reconstruction · Root state of Pupko's reconstruction · Max-product pruning recursion · The max-product recursion computes the maximal labeling weight · Nonnegativity of max-product pruning · Nonnegative transition weights on a tree · Pupko's joint reconstruction · Pupko et al. (2000): joint maximum likelihood · Pupko's traceback · maxPrune bounds the weight of every labeling · Nonnegativity of labeling weights · The traced labeling attains maxPrune · Likelihood of an alignment of independent columns · The PhyloCSF score · The published PhyloCSF score in decibans · Deciban score as a rescaled natural-log score · The score is the log-likelihood ratio of the alignment · Score threshold test for calling an alignment coding · Likelihood of one alignment column · Site likelihood by Felsenstein's pruning algorithm · PhyloCSF's score threshold test is most powerful for unnormalized weights · Likelihood is invariant under swapping root subtrees · The root can be pushed to the end of its edge · Pulley principle, rerooting · Pulley principle, sliding · Nonnegativity of site pattern probabilities · Partial likelihoods are invariant under swapping subtrees · Four-taxon quartet tree model · Rooted quartet with unit costs · True split against third split frequency difference · Wrong split against third split frequency difference · Felsenstein (1978), the exact comparison · Site pattern probabilities sum to one · Labeling agrees with the observed leaf states · Total substitution cost of a labeling · Sankoff's cost is attained · Fitch's algorithm · 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 · 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 · Tropical weight of a labeling equals its edge cost

DefinitionNumber of internal nodes of a tree#✓fully proved

The number of internal nodes.

def numInternal : Tree L S R → ℕ
  | leaf _ => 0
  | node _ l _ r => numInternal l + numInternal r + 1

Uses 1 · Used by 1

Statement usesRooted binary tree with transition weights

Used byNumber of labelings of a tree

DefinitionNumber of leaves of a tree#✓fully proved

The number of leaves.

def numLeaves : Tree L S R → ℕ
  | leaf _ => 1
  | node _ l _ r => numLeaves l + numLeaves r

Uses 1

Statement usesRooted binary tree with transition weights

DefinitionLabeling of the non-root nodes of a tree#✓fully proved

A labeling of the non-root nodes of a tree by states: at every internal node, the states of its two children and labelings of the two subtrees.

def Labeling : Tree L S R → Type v
  | leaf _ => PUnit
  | node _ l _ r => (S × Labeling l) × (S × Labeling r)

Uses 1 · Used by 20

Statement usesRooted binary tree with transition weights

Used byBrute-force likelihood given the root state · Brute-force likelihood at a leaf · Brute-force likelihood factors over subtrees · Number of labelings of a tree · Independent sites · Weight of a tree labeling · Likelihood of Pupko's joint reconstruction · The max-product recursion computes the maximal labeling weight · Pupko's joint reconstruction · Pupko et al. (2000): joint maximum likelihood · Pupko's traceback · maxPrune bounds the weight of every labeling · Nonnegativity of labeling weights · The traced labeling attains maxPrune · Labeling agrees with the observed leaf states · Total substitution cost of a labeling · Sankoff'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

TheoremNumber of labelings of a tree#✓fully proved

There are |S| ^ (2 · #internal nodes) labelings (one state for each non-root node), so the brute-force sum bruteLik has exponentially many terms.

theorem card_labeling [Fintype S] :
    ∀ t : Tree L S R, Fintype.card (Labeling t) = Fintype.card S ^ (2 * t.numInternal)

Uses 3

Statement usesLabeling of the non-root nodes of a tree · Rooted binary tree with transition weights · Number of internal nodes of a tree

DefinitionWeight of a tree labeling#✓fully proved

The weight of a labeling given root state s: the product over all edges of the transition weight from the parent's state to the child's state, times the leaf weight obs l at the state of every leaf l.

def weight : (t : Tree L S R) → S → Labeling t → R
  | leaf l, s, _ => obs l s
  | node P l Q r, s, z =>
    (P s z.1.1 * weight l z.1.1 z.1.2) * (Q s z.2.1 * weight r z.2.1 z.2.2)

Uses 2 · Used by 11

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

Used byBrute-force likelihood given the root state · Brute-force likelihood factors over subtrees · Independent sites · Likelihood of Pupko's joint reconstruction · The max-product recursion computes the maximal labeling weight · Pupko et al. (2000): joint maximum likelihood · maxPrune bounds the weight of every labeling · Nonnegativity of labeling weights · The traced labeling attains maxPrune · Sankoff's algorithm computes the small-parsimony cost · Tropical weight of a labeling equals its edge cost

DefinitionBrute-force likelihood given the root state#✓fully proved

The likelihood of the leaf data conditioned on root state s, by brute force: the sum of the weights of all labelings of the non-root nodes.

def bruteLik (t : Tree L S R) (s : S) : R :=
  ∑ x : Labeling t, weight obs t s x

Uses 3 · Used by 7

Statement usesLabeling of the non-root nodes of a tree · Rooted binary tree with transition weights · Weight of a tree labeling

Used byBrute-force likelihood at a leaf · Brute-force likelihood factors over subtrees · Site likelihood of a phylogenetic tree · The site likelihood by pruning · Felsenstein's pruning algorithm computes the likelihood conditioned on the root state · Independent sites · Sankoff's algorithm computes the small-parsimony cost

DefinitionSite likelihood of a phylogenetic tree#✓fully proved

The site likelihood with root distribution π: ∑ s, π s * bruteLik obs t s.

def likelihood (t : Tree L S R) (π : S → R) : R :=
  ∑ s, π s * bruteLik obs t s

Uses 2 · Used by 14

Statement usesRooted binary tree with transition weights · Brute-force likelihood given the root state

Used byThe site likelihood by pruning · Site likelihood from tabulated partial likelihoods · Independent sites · Likelihood of one alignment column · Likelihood is invariant under swapping root subtrees · The root can be pushed to the end of its edge · Pulley principle, rerooting · Pulley principle, sliding · Probability of a site pattern on a quartet · Nonnegativity of site pattern probabilities · True split against third split frequency difference · Wrong split against third split frequency difference · Felsenstein (1978), the exact comparison · Site pattern probabilities sum to one

DefinitionFelsenstein's pruning recursion#✓fully proved

Felsenstein's pruning recursion: the partial likelihood of the subtree t given state s at its root.

def prune : Tree L S R → S → R
  | leaf l, s => obs l s
  | node P l Q r, s => (∑ a, P s a * prune l a) * (∑ b, Q s b * prune r b)

Uses 1 · Used by 21

Statement usesRooted binary tree with transition weights

Used byThe site likelihood by pruning · Site likelihood from tabulated partial likelihoods · Felsenstein's pruning algorithm computes the likelihood conditioned on the root state · Tabulated pruning computes the pruning recursion · Site likelihood by Felsenstein's pruning algorithm · Likelihood is invariant under swapping root subtrees · The root can be pushed to the end of its edge · Pulley principle, rerooting · Pulley principle, sliding · Nonnegativity of site pattern probabilities · Partial likelihoods are invariant under swapping subtrees · True split against third split frequency difference · Wrong split against third split frequency difference · Felsenstein (1978), the exact comparison · Site pattern probabilities sum to one · Fitch'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

TheoremBrute-force likelihood at a leaf#✓fully proved

At a leaf, the brute-force likelihood is the leaf weight.

theorem bruteLik_leaf (l : L) (s : S) : bruteLik obs (leaf l) s = obs l s

Uses 3 · Used by 1

Statement usesRooted binary tree with transition weights · Brute-force likelihood given the root state

Proof usesLabeling of the non-root nodes of a tree

Used byFelsenstein's pruning algorithm computes the likelihood conditioned on the root state

TheoremBrute-force likelihood factors over subtrees#✓fully proved

The brute-force likelihood factors over the two subtrees of the root (the distributive law behind pruning).

theorem bruteLik_node (P Q : S → S → R) (l r : Tree L S R) (s : S) :
    bruteLik obs (node P l Q r) s =
      (∑ a, P s a * bruteLik obs l a) * (∑ b, Q s b * bruteLik obs r b)

Uses 4 · Used by 1

Statement usesRooted binary tree with transition weights · Brute-force likelihood given the root state

Proof usesLabeling of the non-root nodes of a tree · Weight of a tree labeling

Used byFelsenstein's pruning algorithm computes the likelihood conditioned on the root state

TheoremFelsenstein's pruning algorithm computes the likelihood conditioned on the root state#✓fully proved

Felsenstein's pruning algorithm computes the likelihood conditioned on the root state.

theorem prune_eq_bruteLik : ∀ (t : Tree L S R) (s : S), prune obs t s = bruteLik obs t s

Uses 5 · Used by 2

Statement usesRooted binary tree with transition weights · Brute-force likelihood given the root state · Felsenstein's pruning recursion

Proof usesBrute-force likelihood at a leaf · Brute-force likelihood factors over subtrees

Used byThe site likelihood by pruning · Sankoff's algorithm computes the small-parsimony cost

TheoremThe site likelihood by pruning#✓fully proved

likelihood obs t π = ∑ s, π s * prune obs t s.

theorem likelihood_eq_sum_prune (t : Tree L S R) (π : S → R) :
    likelihood obs t π = ∑ s, π s * prune obs t s

Uses 5 · Used by 9

Statement usesRooted binary tree with transition weights · Site likelihood of a phylogenetic tree · Felsenstein's pruning recursion

Proof usesBrute-force likelihood given the root state · Felsenstein's pruning algorithm computes the likelihood conditioned on the root state

Used bySite likelihood from tabulated partial likelihoods · Site likelihood by Felsenstein's pruning algorithm · Likelihood is invariant under swapping root subtrees · The root can be pushed to the end of its edge · Nonnegativity of site pattern probabilities · True split against third split frequency difference · Wrong split against third split frequency difference · Felsenstein (1978), the exact comparison · Site pattern probabilities sum to one

17 fully proved

The tabulated algorithm

DefinitionTabulated Felsenstein pruning algorithm#✓fully proved

Felsenstein's pruning algorithm, tabulated on the states Fin n: the vector of partial likelihoods of each subtree is computed once, with O(n²) operations per internal node.

def pruneTab : Tree L (Fin n) R → Vector R n
  | leaf l => Vector.ofFn (obs l)
  | node P l Q r =>
    let u := pruneTab l
    let v := pruneTab r
    Vector.ofFn fun s => (∑ a, P s a * u[a]) * (∑ b, Q s b * v[b])

Uses 1 · Used by 2

Statement usesRooted binary tree with transition weights

Used bySite likelihood from tabulated partial likelihoods · Tabulated pruning computes the pruning recursion

TheoremTabulated pruning computes the pruning recursion#✓fully proved

The tabulated algorithm computes the pruning recursion.

theorem pruneTab_get : ∀ (t : Tree L (Fin n) R) (s : Fin n),
    (pruneTab obs t)[s] = prune obs t s

Uses 3 · Used by 1

Statement usesRooted binary tree with transition weights · Felsenstein's pruning recursion · Tabulated Felsenstein pruning algorithm

Used bySite likelihood from tabulated partial likelihoods

TheoremSite likelihood from tabulated partial likelihoods#✓fully proved

The site likelihood from the tabulated partial likelihoods at the root.

theorem likelihood_eq_sum_pruneTab (t : Tree L (Fin n) R) (π : Fin n → R) :
    likelihood obs t π = ∑ s, π s * (pruneTab obs t)[s]

Uses 6

Statement usesRooted binary tree with transition weights · Site likelihood of a phylogenetic tree · Tabulated Felsenstein pruning algorithm

Proof usesThe site likelihood by pruning · Felsenstein's pruning recursion · Tabulated pruning computes the pruning recursion

Independent sites

TheoremIndependent sites#✓fully proved

For an alignment whose sites k : ι evolve independently along the same tree with leaf data obs k, the joint likelihood (the sum over all choices of a root state and a labeling at every site of the product of the per-site weights) is the product of the per-site likelihoods.

theorem sum_prod_siteWeight_eq_prod_likelihood (obs : ι → L → S → R) (t : Tree L S R)
    (π : S → R) :
    ∑ σ : ι → S × Labeling t, ∏ k, π (σ k).1 * weight (obs k) t (σ k).1 (σ k).2 =
      ∏ k, likelihood (obs k) t π

Uses 5

Statement usesLabeling of the non-root nodes of a tree · Rooted binary tree with transition weights · Site likelihood of a phylogenetic tree · Weight of a tree labeling

Proof usesBrute-force likelihood given the root state

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.