Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.discrete-search

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/discrete_search.clj4 definitions, 6 theorems

Kochenderfer discrete-search / sampling / metaheuristic cores as higher-order-function compositions, proved axiom-free, extending the 222 AHoF catalog: O22.7 0-1 knapsack DP : cell = max(exclude value, include value) V5.4 RRT nearest-node : steer toward the nearest existing node (min distance) V5.8 star discrepancy bound : worst-case box discrepancy = max over sub-boxes O22.10 ant colony optimization: pheromone update = evaporation*old + deposit DP/coverage reuse nnrat-minmax max (cell/upper-bound dominates each option); the RRT nearest reuses min (dominated by both candidates); the pheromone dynamics is an add/multiply composition with a worked instance. Native and axiom-free; chains nnrat-minmax on d63.

Depends onmath.rational.nnrat.minmax

dp/knapsack-cell :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

plan/rrt-nearest :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

sample/star-discrepancy-upper :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

aco/pheromone-update :
  (x₁ x₂ x₃ : ℚ≥0)
  → ℚ≥0

dp/knapsack-at-least-exclude :
  (exclude include : ℚ≥0)
  → exclude ≤ dp/knapsack-cell exclude include

dp/knapsack-at-least-include :
  (exclude include : ℚ≥0)
  → include ≤ dp/knapsack-cell exclude include

plan/rrt-nearest-below-left :
  (d0 d1 : ℚ≥0)
  → opt/ldp-min-norm d0 d1 ≤ d0

plan/rrt-nearest-below-right :
  (d0 d1 : ℚ≥0)
  → opt/ldp-min-norm d0 d1 ≤ d1

sample/star-discrepancy-bounds-box0 :
  (b0 b1 : ℚ≥0)
  → b0 ≤ dp/knapsack-cell b0 b1

aco/pheromone-update-example :
  → aco/pheromone-update 1/2 1 1/2 = 1