Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.forward-search

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

AHoF D33 Forward Search: finite-horizon lookahead planning. Building the search tree to the horizon, the value of a decision (max) node is the best value achievable among its action branches: lookahead a b = max(a, b) over the exact-rational action values (the two-action case; the k-action node folds this over the branches). Defined: the lookahead value as the max of the branch values. Proved native and axiom-free, as worked instances: lookahead 4 7 = 7, and 4 <= lookahead 4 7 and 7 <= lookahead 4 7. That the lookahead value dominates every branch for all inputs, and the classical optimality of the extracted greedy action, are not proved here. The tree expansion, the successor generation, and the depth-horizon backups are executable concerns. Requires nnrat/at-most, audit/decide-nnrat-at-most, nnrat/decide-at-most-true-sound, and logic/if-data (all 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.forward-search` prints this classification.

forward-search/lookahead :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

forward-search/lookahead-example :
  → list-maximum/nnrat-max 4 7 = 7

forward-search/lookahead-above-a :
  → 4 ≤ list-maximum/nnrat-max 4 7

forward-search/lookahead-above-b :
  → 7 ≤ list-maximum/nnrat-max 4 7