Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.strong-wolfe

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

AHoF O15 Strong Wolfe Line Search: accept a step only when it satisfies both the Armijo sufficient-decrease condition and the curvature condition: wolfe-ok? new armijo-bound curvature curvature-bound = (new <= armijo-bound) AND (curvature <= curvature-bound) (boolean AND via logic/if-data over the two exact-rational decisions). Proved native and axiom-free: the two-condition acceptance with unfold, a step meeting both, and a step failing the curvature condition. Requires audit/decide-nnrat-at-most, logic/if-data (both 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.strong-wolfe` prints this classification.

wolfe/wolfe-ok? :
  (x₁ x₂ x₃ x₄ : ℚ≥0)
  → data/Bool

wolfe/wolfe-ok-unfold :
  (new ab curv cb : ℚ≥0)
  → wolfe/wolfe-ok? new ab curv cb = logic/if-data data/Bool (audit/decide-nnrat-at-most new ab = audit/decide-nnrat-at-most new ab) (audit/decide-nnrat-at-most new ab) (audit/decide-nnrat-at-most curv cb) data/false

wolfe/both-conditions-accept :
  → wolfe/wolfe-ok? 1/2 3/4 1/2 3/4 = data/true

wolfe/curvature-fails-reject :
  → wolfe/wolfe-ok? 1/2 3/4 3/4 1/2 = data/false