Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.frank-wolfe

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

AHoF O-family Frank-Wolfe (Conditional Gradient) method: minimize a convex objective over a convex set WITHOUT projections. Each iterate solves a linear subproblem for a vertex s (the linear-minimization oracle), then moves toward it by a convex combination with step gamma in [0,1]: x' = (1 - gamma) x + gamma s. Because x and s are both feasible and the update is a convex combination, x' stays feasible -- the projection-free property. Written with the complementary weights w0 = 1 - gamma and w1 = gamma (w0 + w1 = 1): fw-step x s w0 w1 = w0 * x + w1 * s over exact rationals. Proved native and axiom-free: the convex-combination step; a worked half-step; that a full step (w0=0, w1=1) jumps to the vertex s; and that a null step (w0=1, w1=0) stays at x -- all reducing by reflexivity. The gradient and the linear-minimization oracle are executable; what is proved is the convex-combination update. Requires nnrat/add, nnrat/multiply (both 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.frank-wolfe` prints this classification.

frank-wolfe/step :
  (x₁ x₂ x₃ x₄ : ℚ≥0)
  → ℚ≥0

frank-wolfe/half-step :
  → frank-wolfe/step 2 0 1/2 1/2 = 1

frank-wolfe/full-step-to-vertex :
  → frank-wolfe/step 2 7 0 1 = 7

frank-wolfe/null-step-stays :
  → frank-wolfe/step 2 7 1 0 = 2