Reference · Algorithm guarantees

rainbow.algorithms.proofs.edit-distance

Algorithm guaranteessrc/rainbow/algorithms/proofs/edit_distance.clj1 definitions, 4 theorems

AHoF edit distance / Levenshtein alignment DP cell. Aligning two sequences, the dynamic-programming recurrence at each cell takes the cheapest of the three edit operations reaching it -- deletion, insertion, or match/substitution: cell del ins sub = min( del, min(ins, sub) ) over the exact-rational operation costs. This is the Needleman-Wunsch / Levenshtein backward recurrence. Proved native and axiom-free: worked instances with costs del 3, ins 5, sub 2 -- the cell is 2, and the worked certificates cell <= 3, cell <= 5, and cell <= 2. The alignment traceback and the full cost matrix are executable concerns; what is proved here is the cell recurrence at this instance. That the cell is at most each option for all costs, and the optimality of the edit-distance DP, are classical and not proved here. Requires nnrat/at-most, audit/decide-nnrat-at-most, nnrat/decide-at-most-true-sound, and logic/if-data (all carried by the D63 checkpoint). Scope (measured by the kernel): this module has 4 worked instances (statements about specific values). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.edit-distance` prints this classification.

edit-distance/cell :
  (x₁ x₂ x₃ : ℚ≥0)
  → ℚ≥0

edit-distance/cell-example :
  → edit-distance/cell 3 5 2 = 2

edit-distance/cell-below-delete :
  → edit-distance/cell 3 5 2 ≤ 3

edit-distance/cell-below-insert :
  → edit-distance/cell 3 5 2 ≤ 5

edit-distance/cell-below-substitute :
  → edit-distance/cell 3 5 2 ≤ 2