Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.rabin-karp

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

AHoF Rabin-Karp string matching: find a pattern in a text in expected O(n+m) by comparing a ROLLING HASH of each text window against the pattern's hash -- updating the window hash in O(1) as it slides (remove the leaving character, add the entering one). A hash match is only a CANDIDATE (two different strings can collide), so it is verified by a direct comparison; but a hash MISMATCH proves the strings differ, skipping the comparison. The candidate test is a hash equality: candidate-match? window-hash pattern-hash = (window-hash <= pattern-hash) AND (pattern-hash <= window-hash) (the hashes are equal), over exact-rational (integer) hashes. Proved native and axiom-free: the candidate test as the equality of the two hashes (a boolean conjunction of two comparisons via logic/if-data); that equal hashes flag a candidate to verify; the certificates that a candidate's hashes coincide (each at most the other, native nnrat/at-most); and that unequal hashes are a proven mismatch (no comparison needed). The rolling hash and the verification are executable; what is proved is the hash-candidate decision. Requires 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.rabin-karp` prints this classification.

rabin-karp/candidate-match? :
  (x₁ x₂ : ℚ≥0)
  → data/Bool

rabin-karp/equal-hashes-candidate :
  → floyd-cycle/meet? 42 42 = data/true

rabin-karp/candidate-hashes-coincide :
  → 42 ≤ 42

rabin-karp/unequal-hashes-mismatch :
  → floyd-cycle/meet? 17 42 = data/false