Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.lis

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

AHoF Longest Increasing Subsequence (LIS): find the length of the longest strictly-increasing subsequence of a sequence -- underlying diff/patience sorting, box-stacking, and scheduling. Patience sorting achieves O(n log n) by maintaining piles of increasing tails and, for each element, either extending the active subsequence when the element exceeds the current tail, or replacing the smallest tail that is at least the element. The extend decision is: extends? tail element = decide (tail <= element) (the element extends the run when it is at least the current tail), over exact-rational keys. Proved native and axiom-free: the extend test; that an element at least the tail extends the subsequence; the certificate that an extending element really is at least the tail (native nnrat/at-most) -- keeping the run increasing; and that a smaller element cannot extend it (it starts a new pile). The pile bookkeeping / binary search is executable; what is proved is the extend decision. Requires nnrat/at-most, audit/decide-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.lis` prints this classification.

lis/extends? :
  (x₁ x₂ : ℚ≥0)
  → data/Bool

lis/element-extends-run :
  → lis/extends? 5 7 = data/true

lis/extension-keeps-increasing :
  → 5 ≤ 7

lis/smaller-element-cannot-extend :
  → lis/extends? 5 3 = data/false