Gotoh affine-gap alignment

InductiveGap states#✓fully proved

A gap state is one of three values: \(\mathrm{none}\), \(\mathrm{gapX}\) and \(\mathrm{gapY}\). The affine-gap score and the Gotoh recursion carry one as the kind of the previous column: \(\mathrm{gapX}\) after a column pairing an element of the first sequence with a gap, \(\mathrm{gapY}\) after a column pairing a gap with an element of the second sequence, and \(\mathrm{none}\) otherwise, including before the first column.

inductive GapState | none | gapX | gapY deriving DecidableEq, Repr
Used by 24
Used byAffine-gap alignment score · Affine-gap score from a gap state · Linear gaps as affine gaps, from any gap state · Linear gaps are affine gaps with equal costs · Gotoh is optimal · Gotoh is attained · The first row · Gap cost · Cost of a gap run · Adding a column to a gap run · Fuel-bounded Gotoh recursion · Gotoh continuation value after a gap in the second sequence · First-column recurrence for the continuation after a gap in the second sequence · Continuation after a gap in the second sequence, empty first sequence · Continuation after a gap in the second sequence, empty second sequence · Gotoh continuation value after a gap in the first sequence · First-column recurrence for the continuation after a gap in the first sequence · Continuation after a gap in the first sequence, empty first sequence · Continuation after a gap in the first sequence, empty second sequence · Gotoh value with no open gap run · First-column recurrence for the continuation after a match · Gotoh value against an empty first sequence · Gotoh value against an empty second sequence · One row of the table

DefinitionGap cost#✓fully proved

Given an integer gap-open cost \(o\), an integer gap-extend cost \(e\) and gap states \(p\) (of the previous column) and \(c\) (of the current gap column), the cost of the current column is \(e\) if \(p = c\) (the column continues a run) and \(o\) otherwise (it opens a run).

def gapCost (gapOpen gapExtend : ℤ) (prev cur : GapState) : ℤ :=
  if prev = cur then gapExtend else gapOpen
Uses 1 · Used by 17
Statement usesGap states
Used byAffine-gap score from a gap state · Linear gaps as affine gaps, from any gap state · Gotoh is optimal · Gotoh is attained · The first row · Adding a column to a gap run · Fuel-bounded Gotoh recursion · First-column recurrence for the continuation after a gap in the second sequence · Continuation after a gap in the second sequence, empty first sequence · Continuation after a gap in the second sequence, empty second sequence · First-column recurrence for the continuation after a gap in the first sequence · Continuation after a gap in the first sequence, empty first sequence · Continuation after a gap in the first sequence, empty second sequence · First-column recurrence for the continuation after a match · Gotoh value against an empty first sequence · Gotoh value against an empty second sequence · One row of the table

DefinitionAffine-gap score from a gap state#✓fully proved

Fix an integer substitution score \(\sigma\), an integer gap-open cost \(o\) and an integer gap-extend cost \(e\). The affine-gap score of an alignment started from a gap state \(p\) is the sum of its column scores, computed left to right while carrying a gap state that starts at \(p\) and is updated after each column. The empty alignment scores \(0\). A column pairing an element \(a\) of the first sequence with an element \(b\) of the second scores \(\sigma(a, b)\) and sets the state to \(\mathrm{none}\). A column pairing an element of the first sequence with a gap has kind \(\mathrm{gapX}\), and a column pairing a gap with an element of the second sequence has kind \(\mathrm{gapY}\); such a column scores \(e\) if the carried state equals its kind and \(o\) otherwise, and sets the state to its kind. A column of two gaps scores \(0\) and sets the state to \(\mathrm{none}\).

The column of two gaps cannot occur in a valid alignment; it is scored as a no-op.

def affineScoreAux : Alignment α → GapState → ℤ
  | [], _ => 0
  | (some a, some b) :: A, _ => σ a b + affineScoreAux A .none
  | (some _, none) :: A, prev =>
      gapCost gapOpen gapExtend prev .gapX + affineScoreAux A .gapX
  | (none, some _) :: A, prev =>
      gapCost gapOpen gapExtend prev .gapY + affineScoreAux A .gapY
  | (none, none) :: A, _ => affineScoreAux A .none
Uses 3 · Used by 4
Statement usesAlignment · Gap states · Gap cost
Used byAffine-gap alignment score · Linear gaps as affine gaps, from any gap state · Gotoh is optimal · Gotoh is attained

DefinitionAffine-gap alignment score#✓fully proved

Given an integer substitution score \(\sigma\), an integer gap-open cost \(o\) and an integer gap-extend cost \(e\), the affine-gap score of an alignment is its affine-gap score from a gap state, started from the state \(\mathrm{none}\) (no open gap run).

def affineScore (A : Alignment α) : ℤ := affineScoreAux σ gapOpen gapExtend A .none
Uses 3 · Used by 6
Statement usesAlignment · Gap states · Affine-gap score from a gap state
Used byLinear gaps are affine gaps with equal costs · Gotoh is optimal · The table is an upper bound · Gotoh is attained · The table is attained · Gotoh with equal gap scores is Needleman–Wunsch

DefinitionFuel-bounded Gotoh recursion#✓fully proved

Fix an integer-valued scoring function \(\sigma\) on pairs of letters and integer gap-open and gap-extend penalties \(g_o\) and \(g_e\). A gap state records what the previous alignment column was: a match (\(\mathrm{none}\)), a gap in the second sequence (\(\mathrm{gapX}\)) or a gap in the first sequence (\(\mathrm{gapY}\)). For gap states \(p\), \(q\) let \(c(p, q)\) be the gap cost, \(g_e\) if \(p = q\) and \(g_o\) otherwise. Write \(\varepsilon\) for the empty sequence and \(a \cdot u\) for the sequence with first letter \(a\) followed by \(u\). For fuel \(n \in \mathbb{N}\), sequences \(u\), \(v\) and a gap state \(p\), the integer \(G_n(u, v, p)\) is defined by recursion on \(n\): \(G_0(u, v, p) = 0\), \(G_{n+1}(\varepsilon, \varepsilon, p) = 0\), \(G_{n+1}(\varepsilon, b \cdot v, p) = c(p, \mathrm{gapY}) + G_n(\varepsilon, v, \mathrm{gapY})\), \(G_{n+1}(a \cdot u, \varepsilon, p) = c(p, \mathrm{gapX}) + G_n(u, \varepsilon, \mathrm{gapX})\), and \(G_{n+1}(a \cdot u, b \cdot v, p)\) is the maximum of \(\sigma(a, b) + G_n(u, v, \mathrm{none})\), \(c(p, \mathrm{gapX}) + G_n(u, b \cdot v, \mathrm{gapX})\) and \(c(p, \mathrm{gapY}) + G_n(a \cdot u, v, \mathrm{gapY})\).

With fuel at least the sum of the two lengths this is the Gotoh dynamic program; with less fuel the base case \(G_0 = 0\) cuts the recursion short.

def gotohAux : ℕ → List α → List α → GapState → ℤ
  | 0, _, _, _ => 0
  | _ + 1, [], [], _ => 0
  | n + 1, [], b :: ys, prev => gapCost gapOpen gapExtend prev .gapY + gotohAux n [] ys .gapY
  | n + 1, a :: xs, [], prev => gapCost gapOpen gapExtend prev .gapX + gotohAux n xs [] .gapX
  | n + 1, a :: xs, b :: ys, prev =>
      max (σ a b + gotohAux n xs ys .none)
        (max (gapCost gapOpen gapExtend prev .gapX + gotohAux n xs (b :: ys) .gapX)
          (gapCost gapOpen gapExtend prev .gapY + gotohAux n (a :: xs) ys .gapY))
Uses 2 · Used by 14
Statement usesGap states · Gap cost
Used byGotoh is optimal · Gotoh is attained · Gotoh continuation value after a gap in the second sequence · First-column recurrence for the continuation after a gap in the second sequence · Continuation after a gap in the second sequence, empty first sequence · Continuation after a gap in the second sequence, empty second sequence · Gotoh continuation value after a gap in the first sequence · First-column recurrence for the continuation after a gap in the first sequence · Continuation after a gap in the first sequence, empty first sequence · Continuation after a gap in the first sequence, empty second sequence · Gotoh value with no open gap run · First-column recurrence for the continuation after a match · Gotoh value against an empty first sequence · Gotoh value against an empty second sequence

DefinitionGotoh value with no open gap run#✓fully proved

Given a substitution score \(\sigma\), a gap-open score \(g_o\) and a gap-extend score \(g_e\), this is the value of the Gotoh dynamic program on sequences \(x\) and \(y\) when no gap run is open (the previous column was a match, or there is no previous column): the best affine-gap score of an alignment of \(x\) and \(y\), where a match column pairing \(a\) with \(b\) scores \(\sigma(a, b)\) and a gap column scores \(g_e\) if it continues a run of gaps in the same sequence and \(g_o\) otherwise.

It is a continuation value, not an endpoint-restricted matrix: the first column may be a match or either gap.

def gotohContNone (xs ys : List α) : ℤ :=
  gotohAux σ gapOpen gapExtend (xs.length + ys.length) xs ys .none
Uses 2 · Used by 10
Statement usesGap states · Fuel-bounded Gotoh recursion
Used byGotoh is optimal · Specification of a Gotoh table cell · The first row · First-column recurrence for the continuation after a gap in the second sequence · First-column recurrence for the continuation after a gap in the first sequence · First-column recurrence for the continuation after a match · Gotoh value against an empty first sequence · Gotoh value against an empty second sequence · Gotoh score · One row of the table

DefinitionGotoh continuation value after a gap in the second sequence#✓fully proved

Fix an integer-valued scoring function \(\sigma\) on pairs of letters and integer gap-open and gap-extend penalties \(g_o\) and \(g_e\). For sequences \(u\) and \(v\), the value \(X(u, v)\) is the fuel-bounded Gotoh recursion on \(u\) and \(v\), run with fuel equal to the sum of their lengths and started in the gap state where the previous column was a gap in \(v\).

It is the best affine-gap score of an alignment of \(u\) with \(v\) scored from that state. It is a continuation value, not an endpoint-restricted matrix: the next column may be a match or either gap, and the previous state only makes a next gap in \(v\) cost \(g_e\) instead of \(g_o\).

def gotohContGapX (xs ys : List α) : ℤ :=
  gotohAux σ gapOpen gapExtend (xs.length + ys.length) xs ys .gapX
Uses 2 · Used by 9
Statement usesGap states · Fuel-bounded Gotoh recursion
Used byGotoh is optimal · Specification of a Gotoh table cell · The first row · First-column recurrence for the continuation after a gap in the second sequence · Continuation after a gap in the second sequence, empty first sequence · Continuation after a gap in the second sequence, empty second sequence · First-column recurrence for the continuation after a gap in the first sequence · First-column recurrence for the continuation after a match · One row of the table

DefinitionGotoh continuation value after a gap in the first sequence#✓fully proved

Fix an integer-valued scoring function \(\sigma\) on pairs of letters and integer gap-open and gap-extend penalties \(g_o\) and \(g_e\). For sequences \(u\) and \(v\), the value \(Y(u, v)\) is the fuel-bounded Gotoh recursion on \(u\) and \(v\), run with fuel equal to the sum of their lengths and started in the gap state where the previous column was a gap in \(u\).

It is the best affine-gap score of an alignment of \(u\) with \(v\) scored from that state. It is a continuation value, not an endpoint-restricted matrix: the next column may be a match or either gap, and the previous state only makes a next gap in \(u\) cost \(g_e\) instead of \(g_o\).

def gotohContGapY (xs ys : List α) : ℤ :=
  gotohAux σ gapOpen gapExtend (xs.length + ys.length) xs ys .gapY
Uses 2 · Used by 9
Statement usesGap states · Fuel-bounded Gotoh recursion
Used byGotoh is optimal · Specification of a Gotoh table cell · The first row · First-column recurrence for the continuation after a gap in the second sequence · First-column recurrence for the continuation after a gap in the first sequence · Continuation after a gap in the first sequence, empty first sequence · Continuation after a gap in the first sequence, empty second sequence · First-column recurrence for the continuation after a match · One row of the table

DefinitionGotoh score#✓fully proved

For a substitution score \(\sigma\) and gap-open and gap-extend scores \(g_o\) and \(g_e\), the Gotoh score of sequences \(x\) and \(y\) is the Gotoh value of \(x\) against \(y\) with no open gap run, since no gap run is open before the first column.

It is the optimal affine-gap alignment score of \(x\) and \(y\).

def gotohScore (xs ys : List α) : ℤ := gotohContNone σ gapOpen gapExtend xs ys
Uses 1 · Used by 7
Statement usesGotoh value with no open gap run
Used byGotoh is optimal · The table is an upper bound · Gotoh is attained · The table is attained · Gotoh with equal gap scores is Needleman–Wunsch · The table computes the optimal affine-gap score · Gotoh table with equal gap costs gives the Needleman–Wunsch score

DefinitionCost of a gap run#✓fully proved

Given an integer gap-open cost \(o\), an integer gap-extend cost \(e\), gap states \(p\) (of the column before the run) and \(c\) (of the run's columns) and a length \(k \in \mathbb{N}\), the cost of a run of \(k\) gap columns is \(k e\) if \(p = c\) (the run continues an open run); otherwise it is \(0\) for \(k = 0\) and \(o + (k - 1) e\) for \(k \ge 1\).

def gapRunCost (gapOpen gapExtend : ℤ) (prev cur : GapState) (k : ℕ) : ℤ :=
  if prev = cur then (k : ℤ) * gapExtend
  else if k = 0 then 0 else gapOpen + ((k - 1 : ℕ) : ℤ) * gapExtend
Uses 1 · Used by 9
Statement usesGap states
Used byThe first row · Adding a column to a gap run · Continuation after a gap in the second sequence, empty first sequence · Continuation after a gap in the second sequence, empty second sequence · Continuation after a gap in the first sequence, empty first sequence · Continuation after a gap in the first sequence, empty second sequence · Gotoh value against an empty first sequence · Gotoh value against an empty second sequence · One row of the table

TheoremAdding a column to a gap run#✓fully proved

For an integer gap-open cost \(o\), an integer gap-extend cost \(e\), gap states \(p\) and \(c\) and \(k \in \mathbb{N}\), the gap cost of a column in state \(c\) after state \(p\), plus the cost of a run of \(k\) columns in state \(c\) that follows state \(c\), equals the cost of a run of \(k + 1\) columns in state \(c\) that follows state \(p\).

theorem gapRunCost_succ (gapOpen gapExtend : ℤ) (prev cur : GapState) (k : ℕ) :
    gapCost gapOpen gapExtend prev cur + gapRunCost gapOpen gapExtend cur cur k
      = gapRunCost gapOpen gapExtend prev cur (k + 1)
Uses 3 · Used by 8
Statement usesGap states · Gap cost · Cost of a gap run
Used byThe first row · Continuation after a gap in the second sequence, empty first sequence · Continuation after a gap in the second sequence, empty second sequence · Continuation after a gap in the first sequence, empty first sequence · Continuation after a gap in the first sequence, empty second sequence · Gotoh value against an empty first sequence · Gotoh value against an empty second sequence · One row of the table

TheoremRemoving a leading match column from a valid alignment#✓fully proved

Let \(a\) and \(b\) be elements, let \(xs\) and \(ys\) be sequences, and let \(A\) be an alignment. If the alignment whose first column is the match column \((a, b)\), followed by the columns of \(A\), is a valid alignment of the sequence \(a\) followed by \(xs\) and the sequence \(b\) followed by \(ys\), then \(A\) is a valid alignment of \(xs\) and \(ys\).

theorem isAlignment_of_cons_match {a b : α} {A : Alignment α} {xs ys : List α}
    (h : IsAlignment ((some a, some b) :: A) (a :: xs) (b :: ys)) : IsAlignment A xs ys
Uses 2 · Used by 1
Statement usesAlignment · Valid alignment of two sequences
Used byGotoh is optimal

TheoremRemoving a leading column with a gap in the second sequence#✓fully proved

Let \(A\) be an alignment, \(a\) an element and \(x\), \(y\) sequences. If prepending to \(A\) the column that pairs \(a\) with a gap gives a valid alignment of \(a x\) (the sequence \(x\) with \(a\) prepended) and \(y\), then \(A\) is a valid alignment of \(x\) and \(y\).

theorem isAlignment_of_cons_gapX {a : α} {A : Alignment α} {xs ys : List α}
    (h : IsAlignment ((some a, none) :: A) (a :: xs) ys) : IsAlignment A xs ys
Uses 2 · Used by 1
Statement usesAlignment · Valid alignment of two sequences
Used byGotoh is optimal

TheoremRemoving a leading column with a gap in the first sequence#✓fully proved

Let \(A\) be an alignment, \(b\) an element and \(x\), \(y\) sequences. If prepending to \(A\) the column that pairs a gap with \(b\) gives a valid alignment of \(x\) and \(b y\) (the sequence \(y\) with \(b\) prepended), then \(A\) is a valid alignment of \(x\) and \(y\).

theorem isAlignment_of_cons_gapY {b : α} {A : Alignment α} {xs ys : List α}
    (h : IsAlignment ((none, some b) :: A) xs (b :: ys)) : IsAlignment A xs ys
Uses 2 · Used by 1
Statement usesAlignment · Valid alignment of two sequences
Used byGotoh is optimal

TheoremPrepending a match column#✓fully proved

If \(A\) is a valid alignment of sequences \(x\) and \(y\), then for all elements \(a\) and \(b\), the alignment obtained by prepending to \(A\) the column that pairs \(a\) with \(b\) is a valid alignment of \(a x\) and \(b y\) (the sequences \(x\) and \(y\) with \(a\) and \(b\) prepended).

theorem isAlignment_cons_match {a b : α} {A : Alignment α} {xs ys : List α}
    (h : IsAlignment A xs ys) : IsAlignment ((some a, some b) :: A) (a :: xs) (b :: ys)
Uses 2 · Used by 1
Statement usesAlignment · Valid alignment of two sequences
Used byGotoh is attained

TheoremPrepending a column with a gap in the second sequence#✓fully proved

If \(A\) is a valid alignment of sequences \(x\) and \(y\), then for every element \(a\), the alignment obtained by prepending to \(A\) the column that pairs \(a\) with a gap is a valid alignment of \(a x\) (the sequence \(x\) with \(a\) prepended) and \(y\).

theorem isAlignment_cons_gapX {a : α} {A : Alignment α} {xs ys : List α}
    (h : IsAlignment A xs ys) : IsAlignment ((some a, none) :: A) (a :: xs) ys
Uses 2 · Used by 1
Statement usesAlignment · Valid alignment of two sequences
Used byGotoh is attained

TheoremPrepending a column with a gap in the first sequence#✓fully proved

If \(A\) is a valid alignment of sequences \(x\) and \(y\), then for every element \(b\), the alignment obtained by prepending to \(A\) the column that pairs a gap with \(b\) is a valid alignment of \(x\) and \(b y\) (the sequence \(y\) with \(b\) prepended).

theorem isAlignment_cons_gapY {b : α} {A : Alignment α} {xs ys : List α}
    (h : IsAlignment A xs ys) : IsAlignment ((none, some b) :: A) xs (b :: ys)
Uses 2 · Used by 1
Statement usesAlignment · Valid alignment of two sequences
Used byGotoh is attained

TheoremGotoh is optimal#✓fully proved

Let \(\sigma\) be an integer substitution score, \(o\) an integer gap-open cost and \(e\) an integer gap-extend cost. For all sequences \(x\) and \(y\) and every valid alignment \(A\) of \(x\) and \(y\), the affine-gap score of \(A\) is at most the Gotoh score of \(x\) and \(y\), both taken with \(\sigma\), \(o\) and \(e\).

theorem affineScore_le_gotohScore (A : Alignment α) (xs ys : List α)
    (hA : IsAlignment A xs ys) :
    affineScore σ gapOpen gapExtend A ≤ gotohScore σ gapOpen gapExtend xs ys
Uses 14 · Used by 2
Statement usesAlignment · Valid alignment of two sequences · Affine-gap alignment score · Gotoh score
Proof usesGap states · Affine-gap score from a gap state · Gap cost · Fuel-bounded Gotoh recursion · Gotoh continuation value after a gap in the second sequence · Gotoh continuation value after a gap in the first sequence · Gotoh value with no open gap run · Removing a leading column with a gap in the second sequence · Removing a leading column with a gap in the first sequence · Removing a leading match column from a valid alignment
Used byThe table is an upper bound · Gotoh with equal gap scores is Needleman–Wunsch

TheoremGotoh is attained#✓fully proved

Let \(\sigma\) be an integer substitution score, \(o\) an integer gap-open cost and \(e\) an integer gap-extend cost. For all sequences \(x\) and \(y\) there is a valid alignment \(A\) of \(x\) and \(y\) whose affine-gap score equals the Gotoh score of \(x\) and \(y\), both taken with \(\sigma\), \(o\) and \(e\).

theorem exists_affineScore_eq_gotohScore (xs ys : List α) :
    ∃ A, IsAlignment A xs ys ∧
      affineScore σ gapOpen gapExtend A = gotohScore σ gapOpen gapExtend xs ys
Uses 11 · Used by 2
Statement usesAlignment · Valid alignment of two sequences · Affine-gap alignment score · Gotoh score
Proof usesGap states · Affine-gap score from a gap state · Gap cost · Fuel-bounded Gotoh recursion · Prepending a column with a gap in the second sequence · Prepending a column with a gap in the first sequence · Prepending a match column
Used byThe table is attained · Gotoh with equal gap scores is Needleman–Wunsch

TheoremFirst-column recurrence for the continuation after a match#✓fully proved

Fix an integer-valued scoring function \(\sigma\) on pairs of letters and integer gap-open and gap-extend penalties \(g_o\) and \(g_e\). For sequences \(u\), \(v\) let \(N(u, v)\), \(X(u, v)\) and \(Y(u, v)\) be the Gotoh continuation values when the previous column was a match, a gap in \(v\) and a gap in \(u\) respectively, and write \(a \cdot u\) for the sequence with first letter \(a\) followed by \(u\). For all letters \(a\), \(b\) and sequences \(u\), \(v\), the value \(N(a \cdot u, b \cdot v)\) is the maximum of \(N(u, v) + \sigma(a, b)\), \(X(u, b \cdot v) + g_o\) and \(Y(a \cdot u, v) + g_o\).

theorem gotohContNone_eq (a b : α) (xs ys : List α) :
    gotohContNone σ gapOpen gapExtend (a :: xs) (b :: ys) =
      max (gotohContNone σ gapOpen gapExtend xs ys + σ a b)
        (max (gotohContGapX σ gapOpen gapExtend xs (b :: ys) + gapOpen)
          (gotohContGapY σ gapOpen gapExtend (a :: xs) ys + gapOpen))
Uses 6 · Used by 1
Statement usesGotoh continuation value after a gap in the second sequence · Gotoh continuation value after a gap in the first sequence · Gotoh value with no open gap run
Proof usesGap states · Gap cost · Fuel-bounded Gotoh recursion
Used byOne row of the table

TheoremFirst-column recurrence for the continuation after a gap in the second sequence#✓fully proved

Fix an integer-valued scoring function \(\sigma\) on pairs of letters and integer gap-open and gap-extend penalties \(g_o\) and \(g_e\). For sequences \(u\), \(v\) let \(N(u, v)\), \(X(u, v)\) and \(Y(u, v)\) be the Gotoh continuation values when the previous column was a match, a gap in \(v\) and a gap in \(u\) respectively, and write \(a \cdot u\) for the sequence with first letter \(a\) followed by \(u\). For all letters \(a\), \(b\) and sequences \(u\), \(v\), the value \(X(a \cdot u, b \cdot v)\) is the maximum of \(N(u, v) + \sigma(a, b)\), \(X(u, b \cdot v) + g_e\) and \(Y(a \cdot u, v) + g_o\).

theorem gotohContGapX_eq (a b : α) (xs ys : List α) :
    gotohContGapX σ gapOpen gapExtend (a :: xs) (b :: ys) =
      max (gotohContNone σ gapOpen gapExtend xs ys + σ a b)
        (max (gotohContGapX σ gapOpen gapExtend xs (b :: ys) + gapExtend)
          (gotohContGapY σ gapOpen gapExtend (a :: xs) ys + gapOpen))
Uses 6 · Used by 1
Statement usesGotoh continuation value after a gap in the second sequence · Gotoh continuation value after a gap in the first sequence · Gotoh value with no open gap run
Proof usesGap states · Gap cost · Fuel-bounded Gotoh recursion
Used byOne row of the table

TheoremFirst-column recurrence for the continuation after a gap in the first sequence#✓fully proved

Fix an integer-valued scoring function \(\sigma\) on pairs of letters and integer gap-open and gap-extend penalties \(g_o\) and \(g_e\). For sequences \(u\), \(v\) let \(N(u, v)\), \(X(u, v)\) and \(Y(u, v)\) be the Gotoh continuation values when the previous column was a match, a gap in \(v\) and a gap in \(u\) respectively, and write \(a \cdot u\) for the sequence with first letter \(a\) followed by \(u\). For all letters \(a\), \(b\) and sequences \(u\), \(v\), the value \(Y(a \cdot u, b \cdot v)\) is the maximum of \(N(u, v) + \sigma(a, b)\), \(X(u, b \cdot v) + g_o\) and \(Y(a \cdot u, v) + g_e\).

theorem gotohContGapY_eq (a b : α) (xs ys : List α) :
    gotohContGapY σ gapOpen gapExtend (a :: xs) (b :: ys) =
      max (gotohContNone σ gapOpen gapExtend xs ys + σ a b)
        (max (gotohContGapX σ gapOpen gapExtend xs (b :: ys) + gapOpen)
          (gotohContGapY σ gapOpen gapExtend (a :: xs) ys + gapExtend))
Uses 6 · Used by 1
Statement usesGotoh continuation value after a gap in the second sequence · Gotoh continuation value after a gap in the first sequence · Gotoh value with no open gap run
Proof usesGap states · Gap cost · Fuel-bounded Gotoh recursion
Used byOne row of the table

TheoremGotoh value against an empty first sequence#✓fully proved

Let \(g_o\) and \(g_e\) be the gap-open and gap-extend scores. For every sequence \(y\) of length \(n\), the Gotoh value with no open gap run of the empty sequence against \(y\) equals the score of a freshly opened run of \(n\) gaps in the first sequence: \(0\) if \(n = 0\), and \(g_o + (n - 1) g_e\) if \(n \ge 1\).

theorem gotohContNone_nil_left (ys : List α) :
    gotohContNone σ gapOpen gapExtend [] ys =
      gapRunCost gapOpen gapExtend .none .gapY ys.length
Uses 6 · Used by 1
Statement usesGap states · Cost of a gap run · Gotoh value with no open gap run
Proof usesGap cost · Adding a column to a gap run · Fuel-bounded Gotoh recursion
Used byThe first row

TheoremGotoh value against an empty second sequence#✓fully proved

Let \(g_o\) and \(g_e\) be the gap-open and gap-extend scores. For every sequence \(x\) of length \(n\), the Gotoh value with no open gap run of \(x\) against the empty sequence equals the score of a freshly opened run of \(n\) gaps in the second sequence: \(0\) if \(n = 0\), and \(g_o + (n - 1) g_e\) if \(n \ge 1\).

theorem gotohContNone_nil_right (xs : List α) :
    gotohContNone σ gapOpen gapExtend xs [] =
      gapRunCost gapOpen gapExtend .none .gapX xs.length
Uses 6 · Used by 1
Statement usesGap states · Cost of a gap run · Gotoh value with no open gap run
Proof usesGap cost · Adding a column to a gap run · Fuel-bounded Gotoh recursion
Used byOne row of the table

TheoremContinuation after a gap in the second sequence, empty first sequence#✓fully proved

Fix a scoring function \(\sigma\) on pairs of letters and integer gap-open and gap-extend penalties \(g_o\) and \(g_e\), and let \(X(u, v)\) be the Gotoh continuation value of sequences \(u\), \(v\) when the previous column was a gap in \(v\). For every sequence \(v\) of length \(k\), the value \(X(\varepsilon, v)\), where \(\varepsilon\) is the empty sequence, is the cost of one freshly opened gap run of length \(k\): it is \(0\) if \(k = 0\) and \(g_o + (k - 1) g_e\) if \(k \ge 1\).

theorem gotohContGapX_nil_left (ys : List α) :
    gotohContGapX σ gapOpen gapExtend [] ys =
      gapRunCost gapOpen gapExtend .gapX .gapY ys.length
Uses 6 · Used by 1
Statement usesGap states · Cost of a gap run · Gotoh continuation value after a gap in the second sequence
Proof usesGap cost · Adding a column to a gap run · Fuel-bounded Gotoh recursion
Used byThe first row

TheoremContinuation after a gap in the second sequence, empty second sequence#✓fully proved

Fix a scoring function \(\sigma\) on pairs of letters and integer gap-open and gap-extend penalties \(g_o\) and \(g_e\), and let \(X(u, v)\) be the Gotoh continuation value of sequences \(u\), \(v\) when the previous column was a gap in \(v\). For every sequence \(u\) of length \(k\), the value \(X(u, \varepsilon)\), where \(\varepsilon\) is the empty sequence, equals \(k \, g_e\): the open gap run is extended by \(k\) columns.

theorem gotohContGapX_nil_right (xs : List α) :
    gotohContGapX σ gapOpen gapExtend xs [] =
      gapRunCost gapOpen gapExtend .gapX .gapX xs.length
Uses 6 · Used by 1
Statement usesGap states · Cost of a gap run · Gotoh continuation value after a gap in the second sequence
Proof usesGap cost · Adding a column to a gap run · Fuel-bounded Gotoh recursion
Used byOne row of the table

TheoremContinuation after a gap in the first sequence, empty first sequence#✓fully proved

Fix a scoring function \(\sigma\) on pairs of letters and integer gap-open and gap-extend penalties \(g_o\) and \(g_e\), and let \(Y(u, v)\) be the Gotoh continuation value of sequences \(u\), \(v\) when the previous column was a gap in \(u\). For every sequence \(v\) of length \(k\), the value \(Y(\varepsilon, v)\), where \(\varepsilon\) is the empty sequence, equals \(k \, g_e\): the open gap run is extended by \(k\) columns.

theorem gotohContGapY_nil_left (ys : List α) :
    gotohContGapY σ gapOpen gapExtend [] ys =
      gapRunCost gapOpen gapExtend .gapY .gapY ys.length
Uses 6 · Used by 1
Statement usesGap states · Cost of a gap run · Gotoh continuation value after a gap in the first sequence
Proof usesGap cost · Adding a column to a gap run · Fuel-bounded Gotoh recursion
Used byThe first row

TheoremContinuation after a gap in the first sequence, empty second sequence#✓fully proved

Fix a scoring function \(\sigma\) on pairs of letters and integer gap-open and gap-extend penalties \(g_o\) and \(g_e\), and let \(Y(u, v)\) be the Gotoh continuation value of sequences \(u\), \(v\) when the previous column was a gap in \(u\). For every sequence \(u\) of length \(k\), the value \(Y(u, \varepsilon)\), where \(\varepsilon\) is the empty sequence, is the cost of one freshly opened gap run of length \(k\): it is \(0\) if \(k = 0\) and \(g_o + (k - 1) g_e\) if \(k \ge 1\).

theorem gotohContGapY_nil_right (xs : List α) :
    gotohContGapY σ gapOpen gapExtend xs [] =
      gapRunCost gapOpen gapExtend .gapY .gapX xs.length
Uses 6 · Used by 1
Statement usesGap states · Cost of a gap run · Gotoh continuation value after a gap in the first sequence
Proof usesGap cost · Adding a column to a gap run · Fuel-bounded Gotoh recursion
Used byOne row of the table

TheoremLinear gaps as affine gaps, from any gap state#✓fully proved

Let \(\sigma\) be an integer substitution score and \(g\) an integer. If the gap-open cost and the gap-extend cost both equal \(g\), then for every alignment \(A\) and every gap state \(p\), the affine-gap score of \(A\) started from state \(p\), with substitution score \(\sigma\), equals the alignment score of \(A\) with substitution score \(\sigma\) and gap penalty \(g\).

theorem affineScoreAux_eq_alignmentScore (gap : ℤ) (hopen : gapOpen = gap)
    (hext : gapExtend = gap) : ∀ (A : Alignment α) (prev : GapState),
    affineScoreAux σ gapOpen gapExtend A prev = alignmentScore σ gap A
Uses 6 · Used by 1
Statement usesAlignment · Gap states · Affine-gap score from a gap state · Score of an alignment
Proof usesScore of an alignment column · Gap cost
Used byLinear gaps are affine gaps with equal costs

TheoremLinear gaps are affine gaps with equal costs#✓fully proved

Let \(\sigma\) be an integer substitution score and \(g\) an integer. If the gap-open cost and the gap-extend cost both equal \(g\), then for every alignment \(A\), the affine-gap score of \(A\) with substitution score \(\sigma\) equals the alignment score of \(A\) with substitution score \(\sigma\) and gap penalty \(g\).

theorem affineScore_eq_alignmentScore (gap : ℤ) (hopen : gapOpen = gap)
    (hext : gapExtend = gap) (A : Alignment α) :
    affineScore σ gapOpen gapExtend A = alignmentScore σ gap A
Uses 5 · Used by 1
Statement usesAlignment · Affine-gap alignment score · Score of an alignment
Proof usesGap states · Linear gaps as affine gaps, from any gap state
Used byGotoh with equal gap scores is Needleman–Wunsch

TheoremGotoh with equal gap scores is Needleman–Wunsch#✓fully proved

Let \(\sigma\) be a substitution score and \(g\) an integer. If the gap-open and gap-extend scores both equal \(g\), then for all sequences \(x\) and \(y\) the Gotoh score (optimal affine-gap alignment score) of \(x\) and \(y\) equals the Needleman–Wunsch score of \(x\) and \(y\) with substitution score \(\sigma\) and gap score \(g\).

theorem gotohScore_eq_nwScore (gap : ℤ) (hopen : gapOpen = gap) (hext : gapExtend = gap)
    (xs ys : List α) :
    gotohScore σ gapOpen gapExtend xs ys = nwScore σ gap xs ys
Uses 11 · Used by 1
Statement usesGotoh score · Needleman–Wunsch score
Proof usesAlignment · Valid alignment of two sequences · Affine-gap alignment score · Linear gaps are affine gaps with equal costs · Gotoh is optimal · Score of an alignment · Needleman–Wunsch is optimal · Gotoh is attained · Needleman–Wunsch is attained
Used byGotoh table with equal gap costs gives the Needleman–Wunsch score

DefinitionSpecification of a Gotoh table cell#✓fully proved

The specification of a cell: the three continuation values (M, X, Y) of the suffix pair (xs, ys), given that the previous column was a match, a gap in ys, or a gap in xs.

def cellSpec (xs ys : List α) : ℤ × ℤ × ℤ :=
  (gotohContNone σ gapOpen gapExtend xs ys, gotohContGapX σ gapOpen gapExtend xs ys,
    gotohContGapY σ gapOpen gapExtend xs ys)
Uses 3 · Used by 4
Statement usesGotoh continuation value after a gap in the second sequence · Gotoh continuation value after a gap in the first sequence · Gotoh value with no open gap run
Used byThe first row · The rows of the table · The table computes the optimal affine-gap score · One row of the table

DefinitionGotoh cell recurrence from diagonal, upper and left cells#✓fully proved

The cell of (a :: xs, b :: ys) from the cells diag of (xs, ys), up of (xs, b :: ys) and left of (a :: xs, ys): a match continues from M, a gap in ys from X (extending if the previous column was one), a gap in xs from Y.

def step (a b : α) (diag up left : ℤ × ℤ × ℤ) : ℤ × ℤ × ℤ :=
  (max (diag.1 + σ a b) (max (up.2.1 + gapOpen) (left.2.2 + gapOpen)),
    max (diag.1 + σ a b) (max (up.2.1 + gapExtend) (left.2.2 + gapOpen)),
    max (diag.1 + σ a b) (max (up.2.1 + gapOpen) (left.2.2 + gapExtend)))
Used by 2
Used byGotoh table row from the previous row · One row of the table

DefinitionGotoh cell recurrence against an empty second suffix#✓fully proved

The cell of (a :: xs, []) from the cell o of (xs, []): one more gap column in ys.

def stepX (o : ℤ × ℤ × ℤ) : ℤ × ℤ × ℤ :=
  (o.2.1 + gapOpen, o.2.1 + gapExtend, o.2.1 + gapOpen)
Used by 2
Used byGotoh table row from the previous row · One row of the table

DefinitionGotoh table row of the empty first suffix#✓fully proved

The row of the suffix [] of xs: the cells of ([], t) for the suffixes t of ys, longest first, each one gap column in xs more than the next.

def firstRow : List α → List (ℤ × ℤ × ℤ)
  | [] => [0]
  | _ :: ys =>
      let rest := firstRow ys
      ((rest.headD 0).2.2 + gapOpen, (rest.headD 0).2.2 + gapOpen,
        (rest.headD 0).2.2 + gapExtend) :: rest
Used by 2
Used byThe first row · Gotoh table row of a suffix of the first sequence

DefinitionGotoh table row from the previous row#✓fully proved

The row of a :: xs from the row prev of xs, over the remaining suffixes of ys, longest first; each cell uses the cell to its right in the same row. A row prev that is too short gives junk cells (this does not happen for rows of the table, nextRow_eq).

def nextRow (a : α) : List α → List (ℤ × ℤ × ℤ) → List (ℤ × ℤ × ℤ)
  | [], prev => [stepX gapOpen gapExtend (prev.headD 0)]
  | b :: ys, prev =>
      let rest := nextRow a ys prev.tail
      step σ gapOpen gapExtend a b (prev.tail.headD 0) (prev.headD 0) (rest.headD 0) :: rest
Uses 2 · Used by 3
Statement usesGotoh cell recurrence from diagonal, upper and left cells · Gotoh cell recurrence against an empty second suffix
Used byGotoh table row of a suffix of the first sequence · The rows of the table · One row of the table

DefinitionGotoh table row of a suffix of the first sequence#✓fully proved

The row of the suffix xs (of the first sequence) of the table, computed from the rows of its shorter suffixes.

def gotohRows (ys : List α) : List α → List (ℤ × ℤ × ℤ)
  | [] => firstRow gapOpen gapExtend ys
  | a :: xs => nextRow σ gapOpen gapExtend a ys (gotohRows ys xs)
Uses 2 · Used by 3
Statement usesGotoh table row of the empty first suffix · Gotoh table row from the previous row
Used byThe rows of the table · The Gotoh table · The table computes the optimal affine-gap score

DefinitionThe Gotoh table#✓fully proved

The M value of the cell (xs, ys).

def gotohTab (xs ys : List α) : ℤ :=
  ((gotohRows σ gapOpen gapExtend ys xs).headD 0).1
Uses 1 · Used by 4
Statement usesGotoh table row of a suffix of the first sequence
Used byThe table is an upper bound · The table is attained · The table computes the optimal affine-gap score · Gotoh table with equal gap costs gives the Needleman–Wunsch score

TheoremThe first row#✓fully proved

firstRow ys holds the cells of ([], t) for the suffixes t of ys.

theorem firstRow_eq (ys : List α) :
    firstRow gapOpen gapExtend ys = ys.tails.map (cellSpec σ gapOpen gapExtend [])
Uses 12 · Used by 1
Statement usesSpecification of a Gotoh table cell · Gotoh table row of the empty first suffix
Proof usesGap states · Gap cost · Cost of a gap run · Adding a column to a gap run · Gotoh continuation value after a gap in the second sequence · Continuation after a gap in the second sequence, empty first sequence · Gotoh continuation value after a gap in the first sequence · Continuation after a gap in the first sequence, empty first sequence · Gotoh value with no open gap run · Gotoh value against an empty first sequence
Used byThe rows of the table

TheoremOne row of the table#✓fully proved

From the row of the suffix xs, nextRow computes the row of a :: xs: the cells cellSpec (a :: xs) t for the suffixes t of ys, longest first.

theorem nextRow_eq (a : α) (xs ys : List α) :
    nextRow σ gapOpen gapExtend a ys (ys.tails.map (cellSpec σ gapOpen gapExtend xs)) =
      ys.tails.map (cellSpec σ gapOpen gapExtend (a :: xs))
Uses 17 · Used by 1
Statement usesSpecification of a Gotoh table cell · Gotoh table row from the previous row
Proof usesGap states · Gap cost · Cost of a gap run · Adding a column to a gap run · Gotoh continuation value after a gap in the second sequence · First-column recurrence for the continuation after a gap in the second sequence · Continuation after a gap in the second sequence, empty second sequence · Gotoh continuation value after a gap in the first sequence · First-column recurrence for the continuation after a gap in the first sequence · Continuation after a gap in the first sequence, empty second sequence · Gotoh value with no open gap run · First-column recurrence for the continuation after a match · Gotoh value against an empty second sequence · Gotoh cell recurrence from diagonal, upper and left cells · Gotoh cell recurrence against an empty second suffix
Used byThe rows of the table

TheoremThe rows of the table#✓fully proved

The row of xs holds cellSpec xs t for every suffix t of ys, longest first.

theorem gotohRows_eq (xs ys : List α) :
    gotohRows σ gapOpen gapExtend ys xs = ys.tails.map (cellSpec σ gapOpen gapExtend xs)
Uses 5 · Used by 1
Statement usesSpecification of a Gotoh table cell · Gotoh table row of a suffix of the first sequence
Proof usesThe first row · Gotoh table row from the previous row · One row of the table
Used byThe table computes the optimal affine-gap score

TheoremThe table computes the optimal affine-gap score#✓fully proved

The table computes the optimal affine-gap score (Gotoh 1982): gotohTab = gotohScore.

theorem gotohTab_eq_gotohScore (xs ys : List α) :
    gotohTab σ gapOpen gapExtend xs ys = gotohScore σ gapOpen gapExtend xs ys
Uses 5 · Used by 3
Statement usesGotoh score · The Gotoh table
Proof usesSpecification of a Gotoh table cell · Gotoh table row of a suffix of the first sequence · The rows of the table
Used byThe table is an upper bound · The table is attained · Gotoh table with equal gap costs gives the Needleman–Wunsch score

TheoremThe table is an upper bound#✓fully proved

Every alignment of xs and ys has affine-gap score at most gotohTab.

theorem affineScore_le_gotohTab (A : Alignment α) (xs ys : List α) (hA : IsAlignment A xs ys) :
    affineScore σ gapOpen gapExtend A ≤ gotohTab σ gapOpen gapExtend xs ys
Uses 7
Statement usesAlignment · Valid alignment of two sequences · Affine-gap alignment score · The Gotoh table
Proof usesGotoh is optimal · Gotoh score · The table computes the optimal affine-gap score

TheoremThe table is attained#✓fully proved

Some alignment of xs and ys has affine-gap score gotohTab.

theorem exists_affineScore_eq_gotohTab (xs ys : List α) :
    ∃ A, IsAlignment A xs ys ∧
      affineScore σ gapOpen gapExtend A = gotohTab σ gapOpen gapExtend xs ys
Uses 7
Statement usesAlignment · Valid alignment of two sequences · Affine-gap alignment score · The Gotoh table
Proof usesGotoh is attained · Gotoh score · The table computes the optimal affine-gap score

TheoremGotoh table with equal gap costs gives the Needleman–Wunsch score#✓fully proved

With gapOpen = gapExtend = gap, the Gotoh table computes the linear-gap Needleman–Wunsch score.

theorem gotohTab_eq_nwScore (gap : ℤ) (hopen : gapOpen = gap) (hext : gapExtend = gap)
    (xs ys : List α) : gotohTab σ gapOpen gapExtend xs ys = nwScore σ gap xs ys
Uses 5
Statement usesNeedleman–Wunsch score · The Gotoh table
Proof usesGotoh score · Gotoh with equal gap scores is Needleman–Wunsch · The table computes the optimal affine-gap score
45 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.