Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.astar

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

AHoF D37 A* / heuristic search: the priority by which A* expands nodes is the estimated total cost through a node, the path cost so far plus the heuristic estimate of the cost to go: f g h = g + h over exact-rational costs. A* pops the frontier node of least f. Proved native and axiom-free: the f-value is the sum, and the admissibility bound -- when the heuristic h underestimates the true remaining cost c (h <= c), the priority underestimates the true total path cost (f g h <= g + c), which is exactly what guarantees A* returns an optimal path. The frontier, the expansion, and the successor generation are executable concerns; what is proved here is the f-value and the admissibility bound. Requires nnrat/add, nnrat/at-most, and the decidable nnrat order (D63). 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.astar` prints this classification.

astar/f-value :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

astar/f-value-unfold :
  (g h : ℚ≥0)
  → astar/f-value g h = g + h

astar/f-value-example :
  → astar/f-value 3 4 = 7

astar/admissibility-bound :
  → astar/f-value 3 4 ≤ 3 + 5