Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.direct

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

AHoF O37 DIRECT (DIvided RECTangles): a Lipschitzian global optimizer that partitions the domain into rectangles and subdivides the 'potentially optimal' ones. Among rectangles of comparable size the more promising one has the smaller center value, so the selection core is the minimum of two center values: prefers-lower? a b = decide (a <= b) more-promising a b = if (a <= b) then a else b (the smaller center value) over exact rationals. Proved native and axiom-free: the preference decision, the more-promising (min) selection in both orders, and a worked preference. Requires audit/decide-nnrat-at-most, logic/if-data (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.direct` prints this classification.

direct-opt/prefers-lower? :
  (x₁ x₂ : ℚ≥0)
  → data/Bool

direct-opt/more-promising :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

direct-opt/selects-lower-center :
  → astar-fal/expand-value 1/2 3/4 = 1/2

direct-opt/selects-lower-center-symmetric :
  → astar-fal/expand-value 3/4 1/2 = 1/2

direct-opt/prefers-lower-example :
  → ce-is/elite? 1/2 3/4 = data/true