Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.simplex

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

AHoF O54 Simplex Algorithm -- the minimum-ratio test that chooses the leaving variable (pivot row) each iteration. Having chosen an entering column, the simplex method pivots on the row with the smallest ratio of right-hand side to positive pivot-column entry, keeping the basic solution feasible: pivot-ratio r1 r2 = min(r1, r2) over the exact-rational ratios (the two-row case; the general test folds this over all rows with a positive column entry). Proved native and axiom-free: worked instances with ratios 7 and 2 -- pivot-ratio 7 2 = 2, and the worked certificates pivot-ratio 7 2 <= 7 and pivot-ratio 7 2 <= 2. The tableau pivot, entering-column selection (Bland's rule / steepest edge), and optimality test are executable concerns; what is proved here is the min-ratio choice at this instance. That the min-ratio step is the largest that preserves feasibility is the classical property of the test and is not proved here. Requires nnrat/at-most, audit/decide-nnrat-at-most, nnrat/decide-at-most-true-sound, and logic/if-data (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.simplex` prints this classification.

simplex/pivot-ratio :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

simplex/pivot-example :
  → ppo/nnrat-min 7 2 = 2

simplex/pivot-below-r1 :
  → ppo/nnrat-min 7 2 ≤ 7

simplex/pivot-below-r2 :
  → ppo/nnrat-min 7 2 ≤ 2