Profile hidden Markov models

InductiveState types of a profile HMM node#✓fully proved

The state types of a profile HMM node: match, insert, delete.

inductive ProfileState
  /-- Match: emit a residue aligned to the node's column. -/
  | M
  /-- Insert: emit a residue between two columns. -/
  | I
  /-- Delete: skip the node's column (silent). -/
  | D
  deriving DecidableEq, Repr

Used by 11

Used byThe Viterbi value is attained · Forward value of a sequence under a profile HMM · Forward computes the total path weight · HMMER Plan 7 restrictions · Nonnegative weights of a profile HMM · Weight of a path through a profile HMM · Every path weighs at most the Viterbi value · Profile hidden Markov model · Profile HMM as an alignment automaton · Nonnegative profile HMM gives a nonnegative alignment automaton · Viterbi value of a sequence under a profile HMM

StructureProfile hidden Markov model#✓fully proved

A profile HMM with L consensus columns over the alphabet α, with weights in R. trans k s t is the weight of a transition from the state of type s at node k (0 ≤ k ≤ L; node 0 is the begin state, read as type M) to a state of type t: to M or D at node k + 1, or to I at node k. stop s is the weight of the transition from the state of type s at node L to the end state.

structure ProfileHMM (L : ℕ) (α R : Type*) where
  /-- The weight of a transition out of node `k` from type `s` to type `t`. -/
  trans : ℕ → ProfileState → ProfileState → R
  /-- The weight of the transition from node `L` to the end state. -/
  stop : ProfileState → R
  /-- The emission weight of a residue from the match state at node `k`. -/
  emitM : ℕ → α → R
  /-- The emission weight of a residue from the insert state at node `k`. -/
  emitI : ℕ → α → R

Uses 1 · Used by 10

Statement usesState types of a profile HMM node

Used byThe Viterbi value is attained · Forward value of a sequence under a profile HMM · Forward computes the total path weight · HMMER Plan 7 restrictions · Nonnegative weights of a profile HMM · Weight of a path through a profile HMM · Every path weighs at most the Viterbi value · Profile HMM as an alignment automaton · Nonnegative profile HMM gives a nonnegative alignment automaton · Viterbi value of a sequence under a profile HMM

DefinitionConsensus columns of a profile HMM#✓fully proved

The consensus columns [1, …, L].

def columns (L : ℕ) : List ℕ := List.range' 1 L

Used by 5

Used byThe Viterbi value is attained · Forward value of a sequence under a profile HMM · Forward computes the total path weight · Every path weighs at most the Viterbi value · Viterbi value of a sequence under a profile HMM

StructureHMMER Plan 7 restrictions#✓fully proved

HMMER's Plan 7 restrictions (Eddy 1998): no delete-to-insert and no insert-to-delete transitions, and no insert states at node 0 (the begin state) or node L.

structure IsPlan7 [Zero R] (h : ProfileHMM L α R) : Prop where
  /-- No `D → I` transitions. -/
  no_DI : ∀ k, h.trans k .D .I = 0
  /-- No `I → D` transitions. -/
  no_ID : ∀ k, h.trans k .I .D = 0
  /-- No insert state at the begin node. -/
  no_I₀ : ∀ s, h.trans 0 s .I = 0
  /-- No insert state at the last node. -/
  no_I_last : ∀ s, h.trans L s .I = 0

Uses 2

Statement usesProfile hidden Markov model · State types of a profile HMM node

16 fully proved

Semiring

DefinitionProfile HMM as an alignment automaton#✓fully proved

The profile HMM as an alignment automaton reading alignments of a sequence to the columns [1, …, L]. The control state is the type of the previous state and the current node (the last column consumed); it starts at (M, 0), the begin state. Reading (some a, some j) visits M j, (some a, none) visits the insert state of the current node, (none, some j) visits D j; the invalid column (none, none) has weight 0.

def toAutomaton : AlignmentAutomaton (ProfileState × ℕ) α ℕ R where
  weight q c := match c with
    | (some a, some j) => h.trans q.2 q.1 .M * h.emitM j a
    | (some a, none) => h.trans q.2 q.1 .I * h.emitI q.2 a
    | (none, some _) => h.trans q.2 q.1 .D
    | (none, none) => 0
  next q c := match c with
    | (some _, some j) => (.M, j)
    | (some _, none) => (.I, q.2)
    | (none, some j) => (.D, j)
    | (none, none) => q
  final q := h.stop q.1

Uses 3 · Used by 7

Statement usesWeighted alignment automaton · Profile hidden Markov model · State types of a profile HMM node

Used byThe Viterbi value is attained · Forward value of a sequence under a profile HMM · Forward computes the total path weight · Weight of a path through a profile HMM · Every path weighs at most the Viterbi value · Nonnegative profile HMM gives a nonnegative alignment automaton · Viterbi value of a sequence under a profile HMM

DefinitionWeight of a path through a profile HMM#✓fully proved

The weight of a path through the model, given as an alignment A of the sequence to the columns: the product of its transition and emission weights from the begin state to the end state.

def pathProb (A : List (Option α × Option ℕ)) : R := h.toAutomaton.alignWeight (.M, 0) A

Uses 4 · Used by 3

Statement usesWeight of an alignment read by an automaton · Profile hidden Markov model · Profile HMM as an alignment automaton · State types of a profile HMM node

Used byThe Viterbi value is attained · Forward computes the total path weight · Every path weighs at most the Viterbi value

DefinitionForward value of a sequence under a profile HMM#✓fully proved

The forward value of a sequence x: the total weight of all paths through the model that emit x (forward_eq_sum), by the recursion on one residue and one column.

def forward (x : List α) : R := h.toAutomaton.sumDP (.M, 0) x (columns L)

Uses 5 · Used by 1

Statement usesTotal alignment weight by first-column recursion · Profile hidden Markov model · Consensus columns of a profile HMM · Profile HMM as an alignment automaton · State types of a profile HMM node

Used byForward computes the total path weight

TheoremForward computes the total path weight#✓fully proved

The sum, over all alignments of x to the columns [1, …, L] (all paths through the model emitting x, each once), of the path weights.

theorem forward_eq_sum (x : List α) :
    h.forward x = ((alignmentsOf x (columns L)).map h.pathProb).sum

Uses 8

Statement usesProfile hidden Markov model · Consensus columns of a profile HMM · Forward value of a sequence under a profile HMM · Weight of a path through a profile HMM · All alignments of sequences over two alphabets

Proof usesThe sum recursion is the sum over alignments · Profile HMM as an alignment automaton · State types of a profile HMM node

Viterbi

DefinitionViterbi value of a sequence under a profile HMM#✓fully proved

The Viterbi value of a sequence x: the value selected by the max recursion (pathProb_le_viterbi, exists_pathProb_eq_viterbi). Under nonnegative weights it is the largest weight of a path through the model emitting x.

def viterbi (x : List α) : R := h.toAutomaton.maxDP (.M, 0) x (columns L)

Uses 5 · Used by 2

Statement usesMax-recursion alignment value from a control state · Profile hidden Markov model · Consensus columns of a profile HMM · Profile HMM as an alignment automaton · State types of a profile HMM node

Used byThe Viterbi value is attained · Every path weighs at most the Viterbi value

StructureNonnegative weights of a profile HMM#✓fully proved

Nonnegative transition and emission weights (the transitions to the end state may have any sign: the Viterbi bound does not need them).

structure Nonneg : Prop where
  /-- Transitions are nonnegative. -/
  trans : ∀ k s t, 0 ≤ h.trans k s t
  /-- Match emissions are nonnegative. -/
  emitM : ∀ k a, 0 ≤ h.emitM k a
  /-- Insert emissions are nonnegative. -/
  emitI : ∀ k a, 0 ≤ h.emitI k a

Uses 2 · Used by 2

Statement usesProfile hidden Markov model · State types of a profile HMM node

Used byEvery path weighs at most the Viterbi value · Nonnegative profile HMM gives a nonnegative alignment automaton

TheoremNonnegative profile HMM gives a nonnegative alignment automaton#✓fully proved

A profile HMM with nonnegative weights is a nonnegative alignment automaton.

theorem toAutomaton_nonneg [IsOrderedRing R] (hn : h.Nonneg) : h.toAutomaton.Nonneg

Uses 6 · Used by 1

Statement usesNonnegative column weights of an alignment automaton · Profile hidden Markov model · Nonnegative weights of a profile HMM · Profile HMM as an alignment automaton · State types of a profile HMM node

Proof usesWeighted alignment automaton

Used byEvery path weighs at most the Viterbi value

TheoremEvery path weighs at most the Viterbi value#✓fully proved

Every path weighs at most the Viterbi value.

theorem pathProb_le_viterbi [IsOrderedRing R] (hn : h.Nonneg) {x : List α}
    {A : List (Option α × Option ℕ)} (hA : A ∈ alignmentsOf x (columns L)) :
    h.pathProb A ≤ h.viterbi x

Uses 10

Statement usesProfile hidden Markov model · Nonnegative weights of a profile HMM · Consensus columns of a profile HMM · Weight of a path through a profile HMM · Viterbi value of a sequence under a profile HMM · All alignments of sequences over two alphabets

Proof usesEvery alignment weighs at most the max recursion · Profile HMM as an alignment automaton · Nonnegative profile HMM gives a nonnegative alignment automaton · State types of a profile HMM node

TheoremThe Viterbi value is attained#✓fully proved

Some path (alignment of x to the profile) has weight equal to the Viterbi value. Under nonnegative weights this attained value is the largest path weight (pathProb_le_viterbi); without that hypothesis attainment alone does not imply maximality.

theorem exists_pathProb_eq_viterbi (x : List α) :
    ∃ A ∈ alignmentsOf x (columns L), h.pathProb A = h.viterbi x

Uses 8

Statement usesProfile hidden Markov model · Consensus columns of a profile HMM · Weight of a path through a profile HMM · Viterbi value of a sequence under a profile HMM · All alignments of sequences over two alphabets

Proof usesThe max recursion is attained · Profile HMM as an alignment automaton · State types of a profile HMM node

Pseudocounts

DefinitionPseudocount emission estimate of a match state#✓fully proved

The emission estimate of a match state from the residues col that a multiple alignment places in its column (gaps omitted), with pseudocounts pc (Durbin et al., chapter 5; Laplace's rule is pc = 1): (count a + pc a) / (|col| + ∑ b, pc b).

def pseudocountEmission (col : List α) (pc : α → K) (a : α) : K :=
  ((col.count a : K) + pc a) / ((col.length : K) + ∑ b, pc b)

Used by 2

Used byPseudocount emission estimates are positive · Pseudocount emission estimates sum to one

TheoremPseudocount emission estimates sum to one#✓fully proved

With positive pseudocounts, the estimated emissions sum to one.

theorem sum_pseudocountEmission [LinearOrder K] [IsStrictOrderedRing K] [Nonempty α]
    (col : List α) {pc : α → K} (hpc : ∀ a, 0 < pc a) :
    ∑ a, pseudocountEmission col pc a = 1

Uses 1

Statement usesPseudocount emission estimate of a match state

TheoremPseudocount emission estimates are positive#✓fully proved

With positive pseudocounts, every residue gets a positive emission estimate, including residues absent from the column.

theorem pseudocountEmission_pos [LinearOrder K] [IsStrictOrderedRing K] (col : List α)
    {pc : α → K} (hpc : ∀ a, 0 < pc a) (a : α) : 0 < pseudocountEmission col pc a

Uses 1

Statement usesPseudocount emission estimate of a match state

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.