Smith–Waterman local alignment

DefinitionAuxiliary row computation for the Smith–Waterman table#✓fully proved

The cells H[i+1][j+1], H[i+1][j+2], … of a row from the remaining letters b :: ys of the second sequence, the remaining cells up :: prev of the previous row, the previous row's cell diag to the upper left and the cell left just computed. A previous row that is too short ends the row early (this does not happen for rows of the table, nextRow_eq).

def nextRowAux (a : α) : List α → List ℤ → ℤ → ℤ → List ℤ
  | [], _, _, _ => []
  | _ :: _, [], _, _ => []
  | b :: ys, up :: prev, diag, left =>
      max 0 (max (max (diag + σ a b) (up + gap)) (left + gap)) ::
        nextRowAux a ys prev up (max 0 (max (max (diag + σ a b) (up + gap)) (left + gap)))

Used by 2

Used byNext row of the Smith–Waterman table · One row of the table

DefinitionNext row of the Smith–Waterman table#✓fully proved

The row of the table for the prefix extended by a, from the previous row: H[i+1][0] = 0, then the recurrence left to right.

def nextRow (a : α) (ys : List α) (prev : List ℤ) : List ℤ :=
  0 :: nextRowAux σ gap a ys prev.tail (prev.headD 0) 0

Uses 1 · Used by 3

Statement usesAuxiliary row computation for the Smith–Waterman table

Used byOne row of the table · Row-by-row filling of the Smith–Waterman table · The table computes the Smith–Waterman score

DefinitionRow-by-row filling of the Smith–Waterman table#✓fully proved

The Smith–Waterman table, filled row by row over the remaining letters of the first sequence: row is the current row and best the largest cell of the earlier rows.

def swTabAux (ys : List α) : List α → List ℤ → ℤ → ℤ
  | [], row, best => max best (listMax row)
  | a :: xs, row, best => swTabAux ys xs (nextRow σ gap a ys row) (max best (listMax row))

Uses 2 · Used by 2

Statement usesMaximum of an integer list with floor zero · Next row of the Smith–Waterman table

Used byThe Smith–Waterman table · The table computes the Smith–Waterman score

DefinitionThe Smith–Waterman table#✓fully proved

The largest cell of the (|xs| + 1) × (|ys| + 1) table, with the zero row H[0][j] = 0 to start.

def swTab (xs ys : List α) : ℤ :=
  swTabAux σ gap ys xs (0 :: ys.map fun _ => 0) 0

Uses 1 · Used by 2

Statement usesRow-by-row filling of the Smith–Waterman table

Used byThe table computes the optimal local alignment score · The table computes the Smith–Waterman score

TheoremOne row of the table#✓fully proved

From the row of the prefix px, nextRow computes the row of px ++ [a]: the cells H[i+1][j] = swCellScore σ gap (px ++ [a]) py for the prefixes py of ys, shortest first.

theorem nextRow_eq (a : α) (px ys : List α) :
    nextRow σ gap a ys (ys.inits.map (swCellScore σ gap px)) =
      ys.inits.map (swCellScore σ gap (px ++ [a]))

Uses 5 · Used by 1

Statement usesThe terminal Smith–Waterman cell · Next row of the Smith–Waterman table

Proof usesThe Smith–Waterman recurrence · The terminal cell vanishes when the second sequence is empty · Auxiliary row computation for the Smith–Waterman table

Used byThe table computes the Smith–Waterman score

TheoremThe table computes the Smith–Waterman score#✓fully proved

swTab is the largest cell swCellScore σ gap px py over all pairs of prefixes.

theorem swTab_eq_swScore (xs ys : List α) : swTab σ gap xs ys = swScore σ gap xs ys

Uses 11 · Used by 1

Statement usesThe Smith–Waterman score · The Smith–Waterman table

Proof usesMaximum of an integer list with floor zero · Pairs of prefixes · The terminal Smith–Waterman cell · Each prefix-pair cell is at most the Smith–Waterman score · The terminal cell vanishes when the first sequence is empty · Bounding the Smith–Waterman score by its cells · Next row of the Smith–Waterman table · One row of the table · Row-by-row filling of the Smith–Waterman table

Used byThe table computes the optimal local alignment score

TheoremThe table computes the optimal local alignment score#✓fully proved

The table computes the optimal local alignment score (Smith–Waterman 1981, gap ≤ 0): swTab is the maximum, over all pairs of infixes of xs and ys (including the empty ones, which give the floor 0), of their optimal global alignment score nwScore.

theorem swTab_eq_localScore (hgap : gap ≤ 0) (xs ys : List α) :
    swTab σ gap xs ys = localScore σ gap xs ys

Uses 5

Statement usesLocal alignment score · The Smith–Waterman table

Proof usesThe local score equals the Smith–Waterman score · The Smith–Waterman score · The table computes the Smith–Waterman score

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.