Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.qp

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

AHoF O56 Quadratic Programming: minimize a convex quadratic objective subject to linear constraints, typically by encoding the KKT stationarity system. The (scalar / separable) quadratic objective value is objective q x c = q * x * x + c * x over exact nonnegative rationals (the general form is 1/2 x^T Q x + c^T x; here the 1/2 is folded into q and the state is scalar or a separable coordinate). Proved native and axiom-free: the objective evaluation and worked instances that reduce by reflexivity, plus the gradient stationarity reading (the minimizer solves the KKT system, executable). The matrix Q, the constraint handling, and the linear-algebra solve are executable concerns; what is proved here is the deterministic quadratic-form evaluation. Requires nnrat/add and nnrat/multiply (in the D63 checkpoint). Scope (measured by the kernel): this module has 2 worked instances (statements about specific values) and 1 definitional unfoldings (true by unfolding a definition). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.ahof.qp` prints this classification.

qp/objective :
  (x₁ x₂ x₃ : ℚ≥0)
  → ℚ≥0

qp/objective-unfold :
  (q x c : ℚ≥0)
  → qp/objective q x c = q · (x · x) + c · x

qp/objective-example :
  → qp/objective 2 3 1 = 21

qp/objective-at-zero :
  → qp/objective 5 0 3 = 0