Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.coordinate-search

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/coordinate_search.clj5 definitions, 4 theorems

AHoF O32 worked cyclic coordinate search over signed-rational pair state. Rate 1 with per-coordinate gradients that read the positive part of each coordinate, starting from the point (2, 2). One cycle descends the first coordinate to 2 - 1 * 2 = 0, then descends the second coordinate of the updated state to 2 - 1 * 2 = 0, reaching (0, 0). The second update reads the state left by the first, so the coordinate optimizations compose in turn. The coordinates are proved by signed cross-product equivalence. Scope (measured by the kernel): this module has 4 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.coordinate-search` prints this classification.

ahof-o32/rate :
  → ℚ≥0

ahof-o32/gradient-first :
  (x₁ : data/Product ℚ ℚ)
  → ℚ≥0

ahof-o32/gradient-second :
  (x₁ : data/Product ℚ ℚ)
  → ℚ≥0

ahof-o32/initial :
  → data/Product ℚ ℚ

ahof-o32/trajectory :
  (x₁ : ℕ)
  → data/Product ℚ ℚ

ahof-o32/first-coordinate-descends-to-zero :
  → product/first ℚ ℚ (iterate) = signed/from-nnrat 0
  where iterate := search/coordinate-iterate ahof-o20/beta ahof-o32/gradient-first ahof-o32/gradient-second 1 ahof-o32/initial

ahof-o32/second-coordinate-descends-to-zero :
  → product/second ℚ ℚ (iterate) = signed/from-nnrat 0
  where iterate := search/coordinate-iterate ahof-o20/beta ahof-o32/gradient-first ahof-o32/gradient-second 1 ahof-o32/initial

ahof-o32/coordinate-recurrence :
  → proposition/conjunction (iterate₁ = ahof-o32/initial) (iterate = cycle)
  where cycle := search/coordinate-cycle ahof-o20/beta ahof-o32/gradient-first ahof-o32/gradient-second ahof-o32/initial
  where iterate := search/coordinate-iterate ahof-o20/beta ahof-o32/gradient-first ahof-o32/gradient-second 1 ahof-o32/initial
  where iterate₁ := search/coordinate-iterate ahof-o20/beta ahof-o32/gradient-first ahof-o32/gradient-second 0 ahof-o32/initial

ahof-o32/coordinate-search :
  → proposition/conjunction (first = signed/from-nnrat 0) (conjunction)
  where conjunction := proposition/conjunction (product/second ℚ ℚ (search/coordinate-iterate ahof-o20/beta ahof-o32/gradient-first ahof-o32/gradient-second 1 ahof-o32/initial) = signed/from-nnrat 0) (proposition/conjunction (search/coordinate-iterate ahof-o20/beta ahof-o32/gradient-first ahof-o32/gradient-second 0 ahof-o32/initial = ahof-o32/initial) (search/coordinate-iterate ahof-o20/beta ahof-o32/gradient-first ahof-o32/gradient-second 1 ahof-o32/initial = search/coordinate-cycle ahof-o20/beta ahof-o32/gradient-first ahof-o32/gradient-second ahof-o32/initial))
  where first := product/first ℚ ℚ (search/coordinate-iterate ahof-o20/beta ahof-o32/gradient-first ahof-o32/gradient-second 1 ahof-o32/initial)