Wavefront alignment algorithm

14 fully proved

Linear Penalties

StructureLinear gap penalties#✓fully proved

Linear gap penalties: match 0, mismatch mismatch ≥ 1, each gap column gap ≥ 1.

structure LinearPenalties where
  /-- Cost of a column pairing two different letters. -/
  mismatch : ℕ
  /-- Cost of a gap column. -/
  gap : ℕ
  /-- Mismatches cost at least one. -/
  mismatch_pos : 0 < mismatch
  /-- Gap columns cost at least one. -/
  gap_pos : 0 < gap

Used by 10

Used byAlignment score is the negated linear-penalty cost · Cost of an alignment column under linear gap penalties · Cost of an alignment under linear gap penalties · Exactness of the wavefront alignment algorithm · The wavefront algorithm computes the optimal alignment cost · Substitution score from linear gap penalties · Furthest-reaching wavefront offset · Fuelled wavefront recurrence · Completeness of the wavefront algorithm · Soundness of the wavefront algorithm

DefinitionCost of an alignment column under linear gap penalties#✓fully proved

The cost of one alignment column.

def columnCost : Option α × Option α → ℕ
  | (some a, some b) => if a = b then 0 else P.mismatch
  | (some _, none) => P.gap
  | (none, some _) => P.gap
  | (none, none) => 0

Uses 1 · Used by 4

Statement usesLinear gap penalties

Used byAlignment score is the negated linear-penalty cost · Cost of an alignment under linear gap penalties · Completeness of the wavefront algorithm · Soundness of the wavefront algorithm

DefinitionCost of an alignment under linear gap penalties#✓fully proved

The cost of an alignment: the sum of its column costs.

def cost (A : Alignment α) : ℕ := (A.map P.columnCost).sum

Uses 3 · Used by 5

Statement usesAlignment · Linear gap penalties · Cost of an alignment column under linear gap penalties

Used byAlignment score is the negated linear-penalty cost · Exactness of the wavefront alignment algorithm · The wavefront algorithm computes the optimal alignment cost · Completeness of the wavefront algorithm · Soundness of the wavefront algorithm

Wavefront

DefinitionLargest valid offset on a diagonal#✓fully proved

The largest valid offset on diagonal k: h ≤ |ys| and v = h - k ≤ |xs|.

def maxOffset (xs ys : List α) (k : ℤ) : ℤ := min (ys.length : ℤ) (xs.length + k)

Used by 5

Used byExactness of the wavefront alignment algorithm · Fuelled extension of matches along a diagonal · Fuelled wavefront recurrence · Completeness of the wavefront algorithm · Soundness of the wavefront algorithm

DefinitionFuelled extension of matches along a diagonal#✓fully proved

Follow matching letters along diagonal k from offset h, with fuel.

def extend (xs ys : List α) (k : ℤ) : ℕ → ℤ → ℤ
  | 0, h => h
  | fuel + 1, h =>
      if h < maxOffset xs ys k ∧ xs[(h - k).toNat]? = ys[h.toNat]? then
        extend xs ys k fuel (h + 1)
      else h

Uses 1 · Used by 3

Statement usesLargest valid offset on a diagonal

Used byMatch extension (slide) along a diagonal · Completeness of the wavefront algorithm · Soundness of the wavefront algorithm

DefinitionMatch extension (slide) along a diagonal#✓fully proved

The match extension ("slide") along diagonal k from offset h.

def slide (xs ys : List α) (k h : ℤ) : ℤ := extend xs ys k (ys.length + 1) h

Uses 1 · Used by 3

Statement usesFuelled extension of matches along a diagonal

Used byFuelled wavefront recurrence · Completeness of the wavefront algorithm · Soundness of the wavefront algorithm

DefinitionFuelled wavefront recurrence#✓fully proved

The wavefront recurrence with fuel (fuel s + 1 suffices; see wavefront). none stands for an unreachable diagonal. Offsets proposed by an operation are clamped to the largest valid offset of the target diagonal before sliding.

Cslib.Algorithms.Lean.Wavefront.wavefrontAux · 16 lines

def wavefrontAux (P : LinearPenalties) (xs ys : List α) : ℕ → ℕ → ℤ → Option ℤ
  | 0, _, _ => none
  | fuel + 1, s, k =>
      if s = 0 then (if k = 0 then some (slide xs ys 0 0) else none)
      else if k < -(xs.length : ℤ) ∨ (ys.length : ℤ) < k then none
      else
        let fromMismatch : Option ℤ :=
          if P.mismatch ≤ s then (wavefrontAux P xs ys fuel (s - P.mismatch) k).map (· + 1)
          else none
        let fromInsertion : Option ℤ :=
          if P.gap ≤ s then (wavefrontAux P xs ys fuel (s - P.gap) (k - 1)).map (· + 1)
          else none
        let fromDeletion : Option ℤ :=
          if P.gap ≤ s then wavefrontAux P xs ys fuel (s - P.gap) (k + 1) else none
        (max fromMismatch (max fromInsertion fromDeletion)).map
          (fun h => slide xs ys k (min h (maxOffset xs ys k)))

Uses 3 · Used by 3

Statement usesLinear gap penalties · Largest valid offset on a diagonal · Match extension (slide) along a diagonal

Used byFurthest-reaching wavefront offset · Completeness of the wavefront algorithm · Soundness of the wavefront algorithm

DefinitionFurthest-reaching wavefront offset#✓fully proved

The furthest-reaching offset of score s on diagonal k = h - v.

def wavefront (P : LinearPenalties) (xs ys : List α) (s : ℕ) (k : ℤ) : Option ℤ :=
  wavefrontAux P xs ys (s + 1) s k

Uses 2 · Used by 4

Statement usesLinear gap penalties · Fuelled wavefront recurrence

Used byExactness of the wavefront alignment algorithm · The wavefront algorithm computes the optimal alignment cost · Completeness of the wavefront algorithm · Soundness of the wavefront algorithm

TheoremSoundness of the wavefront algorithm#✓fully proved

Soundness: a wavefront offset is a valid cell of its diagonal, reachable by an alignment of the corresponding prefixes with cost at most s.

theorem wavefront_sound (P : LinearPenalties) (xs ys : List α) (s : ℕ) (k h : ℤ)
    (hw : wavefront P xs ys s k = some h) :
    max 0 k ≤ h ∧ h ≤ maxOffset xs ys k ∧
      ∃ A, IsAlignment A (xs.take (h - k).toNat) (ys.take h.toNat) ∧ P.cost A ≤ s

Uses 10 · Used by 1

Statement usesAlignment · Valid alignment of two sequences · Linear gap penalties · Cost of an alignment under linear gap penalties · Largest valid offset on a diagonal · Furthest-reaching wavefront offset

Proof usesCost of an alignment column under linear gap penalties · Fuelled extension of matches along a diagonal · Match extension (slide) along a diagonal · Fuelled wavefront recurrence

Used byExactness of the wavefront alignment algorithm

TheoremCompleteness of the wavefront algorithm#✓fully proved

Completeness: every alignment of a pair of prefixes is dominated on its diagonal by the wavefront of its exact cost.

theorem wavefront_complete (P : LinearPenalties) (xs ys : List α) (v h : ℕ)
    (hv : v ≤ xs.length) (hh : h ≤ ys.length) (A : Alignment α)
    (hA : IsAlignment A (xs.take v) (ys.take h)) :
    ∃ h', wavefront P xs ys (P.cost A) ((h : ℤ) - v) = some h' ∧ (h : ℤ) ≤ h'

Uses 10 · Used by 1

Statement usesAlignment · Valid alignment of two sequences · Linear gap penalties · Cost of an alignment under linear gap penalties · Furthest-reaching wavefront offset

Proof usesCost of an alignment column under linear gap penalties · Fuelled extension of matches along a diagonal · Largest valid offset on a diagonal · Match extension (slide) along a diagonal · Fuelled wavefront recurrence

Used byExactness of the wavefront alignment algorithm

TheoremExactness of the wavefront alignment algorithm#✓fully proved

The wavefront algorithm is exact: the end cell is reached by some score s' ≤ s iff some alignment of xs and ys costs at most s. Hence the least such s is the optimal cost.

theorem exists_wavefront_end_iff (P : LinearPenalties) (xs ys : List α) (s : ℕ) :
    (∃ s' ≤ s, wavefront P xs ys s' ((ys.length : ℤ) - xs.length) = some ys.length) ↔
      ∃ A, IsAlignment A xs ys ∧ P.cost A ≤ s

Uses 8 · Used by 1

Statement usesAlignment · Valid alignment of two sequences · Linear gap penalties · Cost of an alignment under linear gap penalties · Furthest-reaching wavefront offset

Proof usesLargest valid offset on a diagonal · Completeness of the wavefront algorithm · Soundness of the wavefront algorithm

Used byThe wavefront algorithm computes the optimal alignment cost

Linear Penalties

DefinitionSubstitution score from linear gap penalties#✓fully proved

The substitution score in the maximization convention of nwScore: 0 for a match and -mismatch for a mismatch (the gap score is -gap).

def score (a b : α) : ℤ := if a = b then 0 else -(P.mismatch : ℤ)

Uses 1 · Used by 2

Statement usesLinear gap penalties

Used byAlignment score is the negated linear-penalty cost · The wavefront algorithm computes the optimal alignment cost

TheoremAlignment score is the negated linear-penalty cost#✓fully proved

Scores are negated costs.

theorem alignmentScore_eq_neg_cost (A : Alignment α) :
    alignmentScore P.score (-(P.gap : ℤ)) A = -(P.cost A : ℤ)

Uses 7 · Used by 1

Statement usesAlignment · Linear gap penalties · Cost of an alignment under linear gap penalties · Substitution score from linear gap penalties · Score of an alignment

Proof usesCost of an alignment column under linear gap penalties · Score of an alignment column

Used byThe wavefront algorithm computes the optimal alignment cost

Wavefront

TheoremThe wavefront algorithm computes the optimal alignment cost#✓fully proved

The end cell is reached by some score s' ≤ s iff s is at least the optimal Needleman–Wunsch cost.

theorem exists_wavefront_end_iff_nwScore (P : LinearPenalties) (xs ys : List α) (s : ℕ) :
    (∃ s' ≤ s, wavefront P xs ys s' ((ys.length : ℤ) - xs.length) = some ys.length) ↔
      -nwScore P.score (-(P.gap : ℤ)) xs ys ≤ s

Uses 12

Statement usesLinear gap penalties · Substitution score from linear gap penalties · Furthest-reaching wavefront offset · Needleman–Wunsch score

Proof usesAlignment · Valid alignment of two sequences · Alignment score is the negated linear-penalty cost · Cost of an alignment under linear gap penalties · Exactness of the wavefront alignment algorithm · Score of an alignment · Needleman–Wunsch is optimal · Needleman–Wunsch is attained

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.