Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.lcs

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/lcs.clj1 definitions, 3 theorems

AHoF Longest Common Subsequence (dynamic programming): the length of the longest subsequence common to two sequences -- the basis of diff, version control merges, and bioinformatics alignment. The DP recurrence: if the current characters MATCH, extend the diagonal subproblem by one; otherwise take the best of dropping a character from either sequence (the left or upper neighbor): cell matched? diag left up = if matched? then 1 + diag else max(left, up) over exact-rational subproblem lengths. Proved native and axiom-free: the DP cell composing a match branch (logic/if-data on the match bit), a successor on the diagonal, and the decidable rational max of the two neighbors; a worked match cell; a worked mismatch cell; and the certificate that a mismatch cell dominates both neighbors (native nnrat/at-most). The character comparison and the table sweep are executable; what is proved is the LCS recurrence cell. Requires nnrat/add, audit/decide-nnrat-at-most, logic/if-data, nnrat/at-most, nnrat/decide-at-most-true-sound (all in the D63 checkpoint). Scope (measured by the kernel): this module has 3 worked instances (statements about specific values). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.ahof.lcs` prints this classification.

lcs/cell :
  (x₁ : data/Bool) (x₂ x₃ x₄ : ℚ≥0)
  → ℚ≥0

lcs/match-extends-diagonal :
  → lcs/cell data/true 2 9 9 = 3

lcs/mismatch-takes-max :
  → lcs/cell data/false 5 2 3 = 3

lcs/dominates-left-neighbor :
  → 2 ≤ 3