Skip to content

Pair hidden Markov models

DefinitionFuel-bounded enumeration of two-alphabet alignments#✓fully proved

All alignments of xs : List α with ys : List β, by fuel recursion on the first column (the same recursion as Cslib.Algorithms.Lean.alignmentsAux, for two alphabets). Implementation detail: use alignmentsOf, whose fuel xs.length + ys.length + 1 is enough.

def alignmentsOfAux {α β : Type*} : ℕ → List α → List β → List (List (Option α × Option β))
  | 0, _, _ => []
  | _ + 1, [], [] => [[]]
  | n + 1, [], b :: ys => (alignmentsOfAux n [] ys).map fun A => (none, some b) :: A
  | n + 1, a :: xs, [] => (alignmentsOfAux n xs []).map fun A => (some a, none) :: A
  | n + 1, a :: xs, b :: ys =>
      (alignmentsOfAux n xs ys).map (fun A => (some a, some b) :: A) ++
        (alignmentsOfAux n xs (b :: ys)).map (fun A => (some a, none) :: A) ++
        (alignmentsOfAux n (a :: xs) ys).map (fun A => (none, some b) :: A)
Used by 10
Used byEvery alignment weighs at most the max recursion · All alignments of sequences over two alphabets · Alignments of two nonempty sequences by first column · Alignments of a nonempty sequence with the empty one · Two-alphabet alignments agree with single-alphabet alignments · Alignments of the empty sequence with a nonempty one · The max recursion is attained · Membership in alignmentsOf is validity · Each alignment is listed once · The sum recursion is the sum over alignments

DefinitionAll alignments of sequences over two alphabets#✓fully proved

All alignments of a sequence over α with a sequence over β: lists of columns Option α × Option β with no (none, none) column whose rows filter to xs and ys (mem_alignmentsOf), each listed once (nodup_alignmentsOf). For β = α this is Cslib.Algorithms.Lean.alignments (alignmentsOf_eq_alignments).

def alignmentsOf {α β : Type*} (xs : List α) (ys : List β) : List (List (Option α × Option β)) :=
  alignmentsOfAux (xs.length + ys.length + 1) xs ys
Uses 1 · Used by 18
Statement usesFuel-bounded enumeration of two-alphabet alignments
Used byEvery alignment weighs at most the Viterbi value · Every alignment weighs at most the max recursion · Alignments of two nonempty sequences by first column · Alignments of a nonempty sequence with the empty one · Two-alphabet alignments agree with single-alphabet alignments · Alignments of the empty sequence with a nonempty one · The Viterbi value is attained · The max recursion is attained · The pair-HMM recursion computes the total weight · Membership in alignmentsOf is validity · Each alignment is listed once · Sum recursion on two nonempty sequences · Sum recursion with an empty second sequence · The sum recursion is the sum over alignments · Sum recursion with an empty first sequence · The Viterbi value is attained · Forward computes the total path weight · Every path weighs at most the Viterbi value

TheoremAlignments of two nonempty sequences by first column#✓fully proved

The alignments of two nonempty sequences, by their first column.

theorem alignmentsOf_cons_cons {α β : Type*} (a : α) (b : β) (xs : List α) (ys : List β) :
    alignmentsOf (a :: xs) (b :: ys) =
      (alignmentsOf xs ys).map (fun A => (some a, some b) :: A) ++
        (alignmentsOf xs (b :: ys)).map (fun A => (some a, none) :: A) ++
        (alignmentsOf (a :: xs) ys).map (fun A => (none, some b) :: A)
Uses 2 · Used by 2
Statement usesAll alignments of sequences over two alphabets
Proof usesFuel-bounded enumeration of two-alphabet alignments
Used byMembership in alignmentsOf is validity · Sum recursion on two nonempty sequences

TheoremAlignments of the empty sequence with a nonempty one#✓fully proved

The alignments of the empty sequence with a nonempty one.

theorem alignmentsOf_nil_cons {α β : Type*} (b : β) (ys : List β) :
    alignmentsOf ([] : List α) (b :: ys) =
      (alignmentsOf [] ys).map (fun A => (none, some b) :: A)
Uses 2 · Used by 2
Statement usesAll alignments of sequences over two alphabets
Proof usesFuel-bounded enumeration of two-alphabet alignments
Used byMembership in alignmentsOf is validity · Sum recursion with an empty first sequence

TheoremAlignments of a nonempty sequence with the empty one#✓fully proved

The alignments of a nonempty sequence with the empty one.

theorem alignmentsOf_cons_nil {α β : Type*} (a : α) (xs : List α) :
    alignmentsOf (a :: xs) ([] : List β) =
      (alignmentsOf xs []).map (fun A => (some a, none) :: A)
Uses 2 · Used by 2
Statement usesAll alignments of sequences over two alphabets
Proof usesFuel-bounded enumeration of two-alphabet alignments
Used byMembership in alignmentsOf is validity · Sum recursion with an empty second sequence

TheoremMembership in alignmentsOf is validity#✓fully proved

No (none, none) column, and the rows filter to the two sequences.

theorem mem_alignmentsOf {α β : Type*} (xs : List α) (ys : List β)
    (A : List (Option α × Option β)) :
    A ∈ alignmentsOf xs ys ↔
      (∀ c ∈ A, c ≠ (none, none)) ∧ A.filterMap Prod.fst = xs ∧ A.filterMap Prod.snd = ys
Uses 5
Statement usesAll alignments of sequences over two alphabets
Proof usesFuel-bounded enumeration of two-alphabet alignments · Alignments of two nonempty sequences by first column · Alignments of a nonempty sequence with the empty one · Alignments of the empty sequence with a nonempty one

TheoremEach alignment is listed once#✓fully proved

Each alignment is listed once.

theorem nodup_alignmentsOf {α β : Type*} (xs : List α) (ys : List β) :
    (alignmentsOf xs ys).Nodup
Uses 2
Statement usesAll alignments of sequences over two alphabets
Proof usesFuel-bounded enumeration of two-alphabet alignments

TheoremTwo-alphabet alignments agree with single-alphabet alignments#✓fully proved

On one alphabet, alignmentsOf is Cslib.Algorithms.Lean.alignments.

theorem alignmentsOf_eq_alignments {α : Type*} (xs ys : List α) :
    alignmentsOf xs ys = alignments xs ys
Uses 5 · Used by 3
Statement usesThe list of all alignments · All alignments of sequences over two alphabets
Proof usesAlignment · Fuel-bounded enumeration of alignments · Fuel-bounded enumeration of two-alphabet alignments
Used byEvery alignment weighs at most the Viterbi value · The Viterbi value is attained · The pair-HMM recursion computes the total weight

StructureWeighted alignment automaton#✓fully proved

A weighted automaton reading an alignment of a sequence over α with a sequence over β column by column with a control state in Q: the weight of reading a column in a control state, the next control state, and the final weight of a control state. Weights are in R.

structure AlignmentAutomaton (Q α β R : Type*) where
  /-- The weight of reading a column in a control state. -/
  weight : Q → Option α × Option β → R
  /-- The control state after reading a column. -/
  next : Q → Option α × Option β → Q
  /-- The weight of ending in a control state. -/
  final : Q → R
Used by 22
Used byWeight of an alignment read by an automaton · Every alignment weighs at most the max recursion · The max recursion is attained · Log-odds of one alignment · Log-odds Viterbi is linear-gap Needleman–Wunsch · Max-recursion alignment value from a control state · Max recursion on two nonempty sequences · Max recursion with an empty second sequence · Max recursion with an empty first sequence · Max recursion on two empty sequences is the final weight · Fuel-bounded max recursion over alignments · Nonnegative column weights of an alignment automaton · Total alignment weight by first-column recursion · Sum recursion on two nonempty sequences · Sum recursion with an empty second sequence · The sum recursion is the sum over alignments · Sum recursion with an empty first sequence · Sum recursion on two empty sequences is the final weight · Fuel-bounded sum recursion over alignments · Pair HMM as an alignment automaton · Profile HMM as an alignment automaton · Nonnegative profile HMM gives a nonnegative alignment automaton

DefinitionWeight of an alignment read by an automaton#✓fully proved

The weight of an alignment read from control state q: the product of the column weights along the alignment, then the final weight.

def alignWeight : Q → List (Option α × Option β) → R
  | q, [] => M.final q
  | q, c :: A => M.weight q c * alignWeight (M.next q c) A
Uses 1 · Used by 12
Statement usesWeighted alignment automaton
Used byJoint weight of sequences and an alignment's state path · Every alignment weighs at most the max recursion · The Viterbi value is attained · The max recursion is attained · The pair-HMM recursion computes the total weight · Log-odds of one alignment · Log-odds Viterbi is linear-gap Needleman–Wunsch · Sum recursion on two nonempty sequences · Sum recursion with an empty second sequence · The sum recursion is the sum over alignments · Sum recursion with an empty first sequence · Weight of a path through a profile HMM

DefinitionFuel-bounded sum recursion over alignments#✓fully proved

The sum recursion with fuel (the fuel bounds the recursion depth). Implementation detail: use sumDP, whose fuel xs.length + ys.length + 1 is enough.

def sumDPAux : ℕ → Q → List α → List β → R
  | 0, _, _, _ => 0
  | _ + 1, q, [], [] => M.final q
  | n + 1, q, [], b :: ys =>
      M.weight q (none, some b) * sumDPAux n (M.next q (none, some b)) [] ys
  | n + 1, q, a :: xs, [] =>
      M.weight q (some a, none) * sumDPAux n (M.next q (some a, none)) xs []
  | n + 1, q, a :: xs, b :: ys =>
      M.weight q (some a, some b) * sumDPAux n (M.next q (some a, some b)) xs ys +
        M.weight q (some a, none) * sumDPAux n (M.next q (some a, none)) xs (b :: ys) +
        M.weight q (none, some b) * sumDPAux n (M.next q (none, some b)) (a :: xs) ys
Uses 1 · Used by 2
Statement usesWeighted alignment automaton
Used byTotal alignment weight by first-column recursion · The sum recursion is the sum over alignments

DefinitionTotal alignment weight by first-column recursion#✓fully proved

The total weight of all alignments of xs and ys read from control state q, by the first-column recursion (sumDP_eq_sum).

def sumDP (q : Q) (xs : List α) (ys : List β) : R :=
  sumDPAux M (xs.length + ys.length + 1) q xs ys
Uses 2 · Used by 8
Statement usesWeighted alignment automaton · Fuel-bounded sum recursion over alignments
Used byTotal weight of a sequence pair under a pair HMM · The pair-HMM recursion computes the total weight · Sum recursion on two nonempty sequences · Sum recursion with an empty second sequence · The sum recursion is the sum over alignments · Sum recursion with an empty first sequence · Sum recursion on two empty sequences is the final weight · Forward value of a sequence under a profile HMM

TheoremThe sum recursion is the sum over alignments#✓fully proved

The sum recursion is the sum over alignments.

theorem sumDP_eq_sum (q : Q) (xs : List α) (ys : List β) :
    sumDP M q xs ys = ((alignmentsOf xs ys).map (alignWeight M q)).sum
Uses 6 · Used by 5
Statement usesWeighted alignment automaton · Weight of an alignment read by an automaton · Total alignment weight by first-column recursion · All alignments of sequences over two alphabets
Proof usesFuel-bounded sum recursion over alignments · Fuel-bounded enumeration of two-alphabet alignments
Used byThe pair-HMM recursion computes the total weight · Sum recursion on two nonempty sequences · Sum recursion with an empty second sequence · Sum recursion with an empty first sequence · Forward computes the total path weight

TheoremSum recursion on two nonempty sequences#✓fully proved

The sum recursion on two nonempty sequences.

theorem sumDP_cons_cons (q : Q) (a : α) (b : β) (xs : List α) (ys : List β) :
    sumDP M q (a :: xs) (b :: ys) =
      M.weight q (some a, some b) * sumDP M (M.next q (some a, some b)) xs ys +
        M.weight q (some a, none) * sumDP M (M.next q (some a, none)) xs (b :: ys) +
        M.weight q (none, some b) * sumDP M (M.next q (none, some b)) (a :: xs) ys
Uses 6
Statement usesWeighted alignment automaton · Total alignment weight by first-column recursion
Proof usesWeight of an alignment read by an automaton · The sum recursion is the sum over alignments · All alignments of sequences over two alphabets · Alignments of two nonempty sequences by first column

TheoremSum recursion with an empty first sequence#✓fully proved

The sum recursion when the first sequence is empty.

theorem sumDP_nil_cons (q : Q) (b : β) (ys : List β) :
    sumDP M q ([] : List α) (b :: ys) =
      M.weight q (none, some b) * sumDP M (M.next q (none, some b)) [] ys
Uses 6
Statement usesWeighted alignment automaton · Total alignment weight by first-column recursion
Proof usesWeight of an alignment read by an automaton · The sum recursion is the sum over alignments · All alignments of sequences over two alphabets · Alignments of the empty sequence with a nonempty one

TheoremSum recursion with an empty second sequence#✓fully proved

The sum recursion when the second sequence is empty.

theorem sumDP_cons_nil (q : Q) (a : α) (xs : List α) :
    sumDP M q (a :: xs) ([] : List β) =
      M.weight q (some a, none) * sumDP M (M.next q (some a, none)) xs []
Uses 6
Statement usesWeighted alignment automaton · Total alignment weight by first-column recursion
Proof usesWeight of an alignment read by an automaton · The sum recursion is the sum over alignments · All alignments of sequences over two alphabets · Alignments of a nonempty sequence with the empty one

TheoremSum recursion on two empty sequences is the final weight#✓fully proved

The sum recursion on two empty sequences is the final weight.

theorem sumDP_nil_nil (q : Q) : sumDP M q ([] : List α) ([] : List β) = M.final q
Uses 2
Statement usesWeighted alignment automaton · Total alignment weight by first-column recursion

DefinitionFuel-bounded max recursion over alignments#✓fully proved

The max recursion with fuel. Implementation detail: use maxDP.

def maxDPAux : ℕ → Q → List α → List β → R
  | 0, _, _, _ => 0
  | _ + 1, q, [], [] => M.final q
  | n + 1, q, [], b :: ys =>
      M.weight q (none, some b) * maxDPAux n (M.next q (none, some b)) [] ys
  | n + 1, q, a :: xs, [] =>
      M.weight q (some a, none) * maxDPAux n (M.next q (some a, none)) xs []
  | n + 1, q, a :: xs, b :: ys =>
      max (max (M.weight q (some a, some b) * maxDPAux n (M.next q (some a, some b)) xs ys)
        (M.weight q (some a, none) * maxDPAux n (M.next q (some a, none)) xs (b :: ys)))
        (M.weight q (none, some b) * maxDPAux n (M.next q (none, some b)) (a :: xs) ys)
Uses 1 · Used by 6
Statement usesWeighted alignment automaton
Used byEvery alignment weighs at most the max recursion · The max recursion is attained · Max-recursion alignment value from a control state · Max recursion on two nonempty sequences · Max recursion with an empty second sequence · Max recursion with an empty first sequence

DefinitionMax-recursion alignment value from a control state#✓fully proved

The max-recursion value of an alignment of xs and ys read from control state q, by the first-column recursion (alignWeight_le_maxDP, exists_alignWeight_eq_maxDP). It is the largest alignment weight only when the weights are nonnegative; in general it is the value of the recursively chosen alignment.

def maxDP (q : Q) (xs : List α) (ys : List β) : R :=
  maxDPAux M (xs.length + ys.length + 1) q xs ys
Uses 2 · Used by 9
Statement usesWeighted alignment automaton · Fuel-bounded max recursion over alignments
Used byEvery alignment weighs at most the max recursion · The Viterbi value is attained · The max recursion is attained · Max recursion on two nonempty sequences · Max recursion with an empty second sequence · Max recursion with an empty first sequence · Max recursion on two empty sequences is the final weight · Viterbi value of a pair HMM · Viterbi value of a sequence under a profile HMM

DefinitionNonnegative column weights of an alignment automaton#✓fully proved

Nonnegative column weights. The final weights may have any sign: the max recursion bounds every alignment weight without that (alignWeight_le_maxDP).

def Nonneg : Prop := ∀ q c, 0 ≤ M.weight q c
Uses 1 · Used by 3
Statement usesWeighted alignment automaton
Used byEvery alignment weighs at most the max recursion · Nonnegative pair HMM gives a nonnegative alignment automaton · Nonnegative profile HMM gives a nonnegative alignment automaton

TheoremEvery alignment weighs at most the max recursion#✓fully proved

Every alignment weighs at most the max recursion (nonnegative weights).

theorem alignWeight_le_maxDP [IsOrderedRing R] {M : AlignmentAutomaton Q α β R}
    (hM : M.Nonneg) (q : Q) {xs : List α} {ys : List β} {A : List (Option α × Option β)}
    (hA : A ∈ alignmentsOf xs ys) :
    alignWeight M q A ≤ maxDP M q xs ys
Uses 7 · Used by 2
Statement usesWeighted alignment automaton · Nonnegative column weights of an alignment automaton · Weight of an alignment read by an automaton · Max-recursion alignment value from a control state · All alignments of sequences over two alphabets
Proof usesFuel-bounded max recursion over alignments · Fuel-bounded enumeration of two-alphabet alignments
Used byEvery alignment weighs at most the Viterbi value · Every path weighs at most the Viterbi value

TheoremThe max recursion is attained#✓fully proved

The max recursion is attained by an alignment.

theorem exists_alignWeight_eq_maxDP (q : Q) (xs : List α) (ys : List β) :
    ∃ A ∈ alignmentsOf xs ys, alignWeight M q A = maxDP M q xs ys
Uses 6 · Used by 2
Statement usesWeighted alignment automaton · Weight of an alignment read by an automaton · Max-recursion alignment value from a control state · All alignments of sequences over two alphabets
Proof usesFuel-bounded max recursion over alignments · Fuel-bounded enumeration of two-alphabet alignments
Used byThe Viterbi value is attained · The Viterbi value is attained

TheoremMax recursion on two nonempty sequences#✓fully proved

The max recursion on two nonempty sequences.

theorem maxDP_cons_cons (q : Q) (a : α) (b : β) (xs : List α) (ys : List β) :
    maxDP M q (a :: xs) (b :: ys) =
      max (max (M.weight q (some a, some b) * maxDP M (M.next q (some a, some b)) xs ys)
        (M.weight q (some a, none) * maxDP M (M.next q (some a, none)) xs (b :: ys)))
        (M.weight q (none, some b) * maxDP M (M.next q (none, some b)) (a :: xs) ys)
Uses 3
Statement usesWeighted alignment automaton · Max-recursion alignment value from a control state
Proof usesFuel-bounded max recursion over alignments

TheoremMax recursion with an empty first sequence#✓fully proved

The max recursion when the first sequence is empty.

theorem maxDP_nil_cons (q : Q) (b : β) (ys : List β) :
    maxDP M q ([] : List α) (b :: ys) =
      M.weight q (none, some b) * maxDP M (M.next q (none, some b)) [] ys
Uses 3
Statement usesWeighted alignment automaton · Max-recursion alignment value from a control state
Proof usesFuel-bounded max recursion over alignments

TheoremMax recursion with an empty second sequence#✓fully proved

The max recursion when the second sequence is empty.

theorem maxDP_cons_nil (q : Q) (a : α) (xs : List α) :
    maxDP M q (a :: xs) ([] : List β) =
      M.weight q (some a, none) * maxDP M (M.next q (some a, none)) xs []
Uses 3
Statement usesWeighted alignment automaton · Max-recursion alignment value from a control state
Proof usesFuel-bounded max recursion over alignments

TheoremMax recursion on two empty sequences is the final weight#✓fully proved

The max recursion on two empty sequences is the final weight.

theorem maxDP_nil_nil (q : Q) : maxDP M q ([] : List α) ([] : List β) = M.final q
Uses 2
Statement usesWeighted alignment automaton · Max-recursion alignment value from a control state
44 fully proved

Pair HMMs

InductiveEmitting states of a pair HMM#✓fully proved

The emitting states of a pair HMM: M emits an aligned pair, X a letter of the first sequence only, Y a letter of the second sequence only.

inductive PairState
  /-- Emit an aligned pair `(a, b)`. -/
  | M
  /-- Emit a letter of the first sequence against a gap. -/
  | X
  /-- Emit a letter of the second sequence against a gap. -/
  | Y
  deriving DecidableEq, Repr
Used by 15
Used byJoint weight of sequences and an alignment's state path · Every alignment weighs at most the Viterbi value · Pair HMM state emitting an alignment column · The Viterbi value is attained · Memoryless pair HMM · Total weight of a sequence pair under a pair HMM · The pair-HMM recursion computes the total weight · Hypotheses of the linear-gap log-odds correspondence · Log-odds of one alignment · Log-odds Viterbi is linear-gap Needleman–Wunsch · Nonnegative weights of a pair HMM · Pair hidden Markov model · Pair HMM as an alignment automaton · Nonnegative pair HMM gives a nonnegative alignment automaton · Viterbi value of a pair HMM

DefinitionPair HMM state emitting an alignment column#✓fully proved

The state that emits an alignment column: M for (some a, some b), X for (some a, none), Y for (none, some b) (and M, unused, for the invalid (none, none)).

def colState {α : Type*} : Option α × Option α → PairState
  | (some _, none) => .X
  | (none, some _) => .Y
  | _ => .M
Uses 1 · Used by 4
Statement usesEmitting states of a pair HMM
Used byLog-odds of one alignment · Log-odds Viterbi is linear-gap Needleman–Wunsch · Pair HMM as an alignment automaton · Nonnegative pair HMM gives a nonnegative alignment automaton

StructurePair hidden Markov model#✓fully proved

A pair HMM over the alphabet α with weights in R (Durbin et al., chapter 4): the transition weights from the silent begin state (start) and between emitting states (trans), to the silent end state (stop from an emitting state, startStop for the empty alignment), and the emission weights of the three emitting states.

Cslib.Bioinformatics.HMM.PairHMM · 15 lines 
structure PairHMM (α R : Type*) where
  /-- The weight of the transition from the begin state to an emitting state. -/
  start : PairState → R
  /-- The weight of the transition from the begin state directly to the end state. -/
  startStop : R
  /-- The weight of a transition between emitting states (from the first to the second). -/
  trans : PairState → PairState → R
  /-- The weight of the transition from an emitting state to the end state. -/
  stop : PairState → R
  /-- The emission weight of an aligned pair from `M`. -/
  emitM : α → α → R
  /-- The emission weight of a letter of the first sequence from `X`. -/
  emitX : α → R
  /-- The emission weight of a letter of the second sequence from `Y`. -/
  emitY : α → R
Uses 1 · Used by 14
Statement usesEmitting states of a pair HMM
Used byJoint weight of sequences and an alignment's state path · Every alignment weighs at most the Viterbi value · Emission weight of an alignment column · The Viterbi value is attained · Memoryless pair HMM · Total weight of a sequence pair under a pair HMM · The pair-HMM recursion computes the total weight · Hypotheses of the linear-gap log-odds correspondence · Log-odds of one alignment · Log-odds Viterbi is linear-gap Needleman–Wunsch · Nonnegative weights of a pair HMM · Pair HMM as an alignment automaton · Nonnegative pair HMM gives a nonnegative alignment automaton · Viterbi value of a pair HMM

DefinitionEmission weight of an alignment column#✓fully proved

The emission weight of an alignment column (0 for the invalid (none, none)).

def emitCol : Option α × Option α → R
  | (some a, some b) => h.emitM a b
  | (some a, none) => h.emitX a
  | (none, some b) => h.emitY b
  | (none, none) => 0
Uses 1 · Used by 4
Statement usesPair hidden Markov model
Used byLog-odds of one alignment · Log-odds Viterbi is linear-gap Needleman–Wunsch · Pair HMM as an alignment automaton · Nonnegative pair HMM gives a nonnegative alignment automaton

DefinitionPair HMM as an alignment automaton#✓fully proved

The pair HMM as an alignment automaton: the control state is the previous HMM state (none for the begin state).

def toAutomaton : AlignmentAutomaton (Option PairState) α α R where
  weight q c := (match q with
    | none => h.start (colState c)
    | some s => h.trans s (colState c)) * h.emitCol c
  next _ c := some (colState c)
  final q := match q with
    | none => h.startStop
    | some s => h.stop s
Uses 5 · Used by 9
Statement usesWeighted alignment automaton · Pair hidden Markov model · Emission weight of an alignment column · Emitting states of a pair HMM · Pair HMM state emitting an alignment column
Used byJoint weight of sequences and an alignment's state path · Every alignment weighs at most the Viterbi value · The Viterbi value is attained · Total weight of a sequence pair under a pair HMM · The pair-HMM recursion computes the total weight · Log-odds of one alignment · Log-odds Viterbi is linear-gap Needleman–Wunsch · Nonnegative pair HMM gives a nonnegative alignment automaton · Viterbi value of a pair HMM

DefinitionJoint weight of sequences and an alignment's state path#✓fully proved

The joint weight of the sequences and the state path of an alignment A (the path visits colState c for each column c): the product of the transition and emission weights along the path, from the begin state to the end state.

def alignProb (A : Alignment α) : R := h.toAutomaton.alignWeight none A
Uses 5 · Used by 5
Statement usesAlignment · Weight of an alignment read by an automaton · Pair hidden Markov model · Pair HMM as an alignment automaton · Emitting states of a pair HMM
Used byEvery alignment weighs at most the Viterbi value · The Viterbi value is attained · The pair-HMM recursion computes the total weight · Log-odds of one alignment · Log-odds Viterbi is linear-gap Needleman–Wunsch

DefinitionTotal weight of a sequence pair under a pair HMM#✓fully proved

The total weight P(xs, ys) of a pair HMM: the total weight of all state paths that emit xs and ys (likelihood_eq_sum), by the first-column recursion.

def likelihood (xs ys : List α) : R := h.toAutomaton.sumDP none xs ys
Uses 4 · Used by 1
Statement usesTotal alignment weight by first-column recursion · Pair hidden Markov model · Pair HMM as an alignment automaton · Emitting states of a pair HMM
Used byThe pair-HMM recursion computes the total weight

TheoremThe pair-HMM recursion computes the total weight#✓fully proved

The sum over all alignments of xs and ys of the joint weight of the sequences and the alignment.

theorem likelihood_eq_sum (xs ys : List α) :
    h.likelihood xs ys = ((alignments xs ys).map h.alignProb).sum
Uses 12
Statement usesAlignment · The list of all alignments · Pair hidden Markov model · Joint weight of sequences and an alignment's state path · Total weight of a sequence pair under a pair HMM
Proof usesWeight of an alignment read by an automaton · Total alignment weight by first-column recursion · The sum recursion is the sum over alignments · Pair HMM as an alignment automaton · Emitting states of a pair HMM · All alignments of sequences over two alphabets · Two-alphabet alignments agree with single-alphabet alignments

DefinitionViterbi value of a pair HMM#✓fully proved

The Viterbi value of a pair HMM: the max-recursion value for xs, ys. It is the largest joint weight over alignments when the HMM weights are nonnegative (see alignProb_le_viterbi).

def viterbi (xs ys : List α) : R := h.toAutomaton.maxDP none xs ys
Uses 4 · Used by 3
Statement usesMax-recursion alignment value from a control state · Pair hidden Markov model · Pair HMM as an alignment automaton · Emitting states of a pair HMM
Used byEvery alignment weighs at most the Viterbi value · The Viterbi value is attained · Log-odds Viterbi is linear-gap Needleman–Wunsch

StructureNonnegative weights of a pair HMM#✓fully proved

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

structure Nonneg : Prop where
  /-- Begin-state transitions are nonnegative. -/
  start : ∀ s, 0 ≤ h.start s
  /-- Transitions between emitting states are nonnegative. -/
  trans : ∀ s t, 0 ≤ h.trans s t
  /-- Match emissions are nonnegative. -/
  emitM : ∀ a b, 0 ≤ h.emitM a b
  /-- `X` emissions are nonnegative. -/
  emitX : ∀ a, 0 ≤ h.emitX a
  /-- `Y` emissions are nonnegative. -/
  emitY : ∀ b, 0 ≤ h.emitY b
Uses 2 · Used by 3
Statement usesPair hidden Markov model · Emitting states of a pair HMM
Used byEvery alignment weighs at most the Viterbi value · Log-odds Viterbi is linear-gap Needleman–Wunsch · Nonnegative pair HMM gives a nonnegative alignment automaton

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

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

theorem toAutomaton_nonneg [IsOrderedRing R] (hn : h.Nonneg) : h.toAutomaton.Nonneg
Uses 7 · Used by 1
Statement usesNonnegative column weights of an alignment automaton · Pair hidden Markov model · Nonnegative weights of a pair HMM · Pair HMM as an alignment automaton · Emitting states of a pair HMM
Proof usesEmission weight of an alignment column · Pair HMM state emitting an alignment column
Used byEvery alignment weighs at most the Viterbi value

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

Every alignment weighs at most the Viterbi value.

theorem alignProb_le_viterbi [IsOrderedRing R] (hn : h.Nonneg) {xs ys : List α} {A : Alignment α}
    (hA : IsAlignment A xs ys) : h.alignProb A ≤ h.viterbi xs ys
Uses 14 · Used by 1
Statement usesAlignment · Valid alignment of two sequences · Pair hidden Markov model · Nonnegative weights of a pair HMM · Joint weight of sequences and an alignment's state path · Viterbi value of a pair HMM
Proof usesThe list of all alignments · The enumerated alignments are exactly the valid ones · Every alignment weighs at most the max recursion · Pair HMM as an alignment automaton · Nonnegative pair HMM gives a nonnegative alignment automaton · Emitting states of a pair HMM · All alignments of sequences over two alphabets · Two-alphabet alignments agree with single-alphabet alignments
Used byLog-odds Viterbi is linear-gap Needleman–Wunsch

TheoremThe Viterbi value is attained#✓fully proved

The Viterbi value is attained by an alignment: the Viterbi alignment.

theorem exists_alignProb_eq_viterbi (xs ys : List α) :
    ∃ A, IsAlignment A xs ys ∧ h.alignProb A = h.viterbi xs ys
Uses 14 · Used by 1
Statement usesAlignment · Valid alignment of two sequences · Pair hidden Markov model · Joint weight of sequences and an alignment's state path · Viterbi value of a pair HMM
Proof usesThe list of all alignments · The enumerated alignments are exactly the valid ones · Weight of an alignment read by an automaton · The max recursion is attained · Max-recursion alignment value from a control state · Pair HMM as an alignment automaton · Emitting states of a pair HMM · All alignments of sequences over two alphabets · Two-alphabet alignments agree with single-alphabet alignments
Used byLog-odds Viterbi is linear-gap Needleman–Wunsch

Log-odds scores and Needleman–Wunsch

StructureMemoryless pair HMM#✓fully proved

The pair HMM's transition weights do not depend on the current state: every transition into an emitting state s (from the begin state or from any emitting state) has weight π s, and every transition into the end state has weight τ.

structure IsMemoryless (h : PairHMM α ℝ) (π : PairState → ℝ) (τ : ℝ) : Prop where
  /-- Begin-state transitions. -/
  start : ∀ s, h.start s = π s
  /-- Transitions between emitting states. -/
  trans : ∀ s t, h.trans s t = π t
  /-- Transitions to the end state from an emitting state. -/
  stop : ∀ s, h.stop s = τ
  /-- The begin-to-end transition. -/
  startStop : h.startStop = τ
Uses 2 · Used by 3
Statement usesPair hidden Markov model · Emitting states of a pair HMM
Used byHypotheses of the linear-gap log-odds correspondence · Log-odds of one alignment · Log-odds Viterbi is linear-gap Needleman–Wunsch

DefinitionIndependence-model weight of a sequence pair#✓fully proved

The independence-model weight for xs and ys (Durbin et al., chapter 4): η² (1 - η)^(|xs| + |ys|) ∏ q xs ∏ q ys. This is a probability when q is a normalized nonnegative distribution and 0 < η < 1, as required by LinearGapLogOdds.

noncomputable def background (q : α → ℝ) (η : ℝ) (xs ys : List α) : ℝ :=
  η ^ 2 * (1 - η) ^ (xs.length + ys.length) * (xs.map q).prod * (ys.map q).prod
Used by 2
Used byLog-odds of one alignment · Log-odds Viterbi is linear-gap Needleman–Wunsch

StructureHypotheses of the linear-gap log-odds correspondence#✓fully proved

The hypotheses of the log-odds correspondence: a memoryless pair HMM with normalized positive transition and emission probabilities, normalized positive background frequencies and 0 < η < 1, whose per-column log-odds scores against the independence model are the integer scores σ a b (aligned pair) and gap (gap column).

Cslib.Bioinformatics.HMM.PairHMM.LinearGapLogOdds · 37 lines 
structure LinearGapLogOdds (h : PairHMM α ℝ) (π : PairState → ℝ) (τ : ℝ) (q : α → ℝ) (η : ℝ)
    (σ : α → α → ℤ) (gap : ℤ) : Prop where
  /-- The transition weights do not depend on the current state. -/
  memoryless : h.IsMemoryless π τ
  /-- The begin row and every emitting-state transition row sum to one. -/
  transition_sum : π .M + π .X + π .Y + τ = 1
  /-- The background frequencies sum to one over the finite alphabet. -/
  q_sum : ∑ a, q a = 1
  /-- The match emission probabilities sum to one. -/
  emitM_sum : ∑ a, ∑ b, h.emitM a b = 1
  /-- The `X` emission probabilities sum to one. -/
  emitX_sum : ∑ a, h.emitX a = 1
  /-- The `Y` emission probabilities sum to one. -/
  emitY_sum : ∑ b, h.emitY b = 1
  /-- Positive transition weights. -/
  π_pos : ∀ s, 0 < π s
  /-- A positive end transition. -/
  τ_pos : 0 < τ
  /-- Positive background frequencies. -/
  q_pos : ∀ a, 0 < q a
  /-- The background stopping probability is in `(0, 1)`. -/
  η_pos : 0 < η
  /-- The background stopping probability is in `(0, 1)`. -/
  η_lt_one : η < 1
  /-- Positive match emissions. -/
  emitM_pos : ∀ a b, 0 < h.emitM a b
  /-- Positive `X` emissions. -/
  emitX_pos : ∀ a, 0 < h.emitX a
  /-- Positive `Y` emissions. -/
  emitY_pos : ∀ b, 0 < h.emitY b
  /-- The log-odds score of an aligned pair is `σ a b`. -/
  logOdds_M : ∀ a b,
    Real.log (π .M * h.emitM a b / ((1 - η) ^ 2 * q a * q b)) = σ a b
  /-- The log-odds score of a letter of the first sequence against a gap is `gap`. -/
  logOdds_X : ∀ a, Real.log (π .X * h.emitX a / ((1 - η) * q a)) = gap
  /-- The log-odds score of a letter of the second sequence against a gap is `gap`. -/
  logOdds_Y : ∀ b, Real.log (π .Y * h.emitY b / ((1 - η) * q b)) = gap
Uses 3 · Used by 2
Statement usesPair hidden Markov model · Memoryless pair HMM · Emitting states of a pair HMM
Used byLog-odds of one alignment · Log-odds Viterbi is linear-gap Needleman–Wunsch

TheoremLog-odds of one alignment#✓fully proved

For a memoryless pair HMM, the log-odds of an alignment against the independence model is its linear-gap alignment score plus log (τ / η²).

theorem log_alignProb_div_background {h : PairHMM α ℝ} {π : PairState → ℝ} {τ : ℝ}
    {q : α → ℝ} {η : ℝ} {σ : α → α → ℤ} {gap : ℤ} (H : LinearGapLogOdds h π τ q η σ gap)
    {xs ys : List α} {A : Alignment α} (hA : IsAlignment A xs ys) :
    Real.log (h.alignProb A / background q η xs ys) =
      alignmentScore σ gap A + Real.log (τ / η ^ 2)
Uses 15 · Used by 1
Statement usesAlignment · Valid alignment of two sequences · Score of an alignment · Pair hidden Markov model · Hypotheses of the linear-gap log-odds correspondence · Joint weight of sequences and an alignment's state path · Independence-model weight of a sequence pair · Emitting states of a pair HMM
Proof usesScore of an alignment column · Weighted alignment automaton · Weight of an alignment read by an automaton · Memoryless pair HMM · Emission weight of an alignment column · Pair HMM as an alignment automaton · Pair HMM state emitting an alignment column
Used byLog-odds Viterbi is linear-gap Needleman–Wunsch

TheoremLog-odds Viterbi is linear-gap Needleman–Wunsch#✓fully proved

For a memoryless pair HMM whose per-column log-odds scores are σ a b and gap, the log-odds Viterbi score against the independence model is the Needleman–Wunsch score with substitution scores σ and linear gap score gap, plus the length term log (τ / η²).

theorem log_viterbi_div_background {h : PairHMM α ℝ} {π : PairState → ℝ} {τ : ℝ}
    {q : α → ℝ} {η : ℝ} {σ : α → α → ℤ} {gap : ℤ} (H : LinearGapLogOdds h π τ q η σ gap)
    (xs ys : List α) :
    Real.log (h.viterbi xs ys / background q η xs ys) =
      nwScore σ gap xs ys + Real.log (τ / η ^ 2)
Uses 23
Statement usesNeedleman–Wunsch score · Pair hidden Markov model · Hypotheses of the linear-gap log-odds correspondence · Independence-model weight of a sequence pair · Viterbi value of a pair HMM · Emitting states of a pair HMM
Proof usesAlignment · Valid alignment of two sequences · Score of an alignment · Needleman–Wunsch is optimal · Score of an alignment column · Needleman–Wunsch is attained · Weighted alignment automaton · Weight of an alignment read by an automaton · Memoryless pair HMM · Nonnegative weights of a pair HMM · Joint weight of sequences and an alignment's state path · Every alignment weighs at most the Viterbi value · Emission weight of an alignment column · The Viterbi value is attained · Log-odds of one alignment · Pair HMM as an alignment automaton · Pair HMM state emitting an alignment column

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.