Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.shooting

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

AHoF V16 Shooting Methods: trajectory-based trajectory optimization / open-loop control. A candidate open-loop plan is scored by SIMULATING it -- threading the action sequence through the dynamics from the initial state to obtain the resulting state: simulate dynamics initial actions = fold dynamics initial actions where `dynamics : state -> action -> state` is the (pluggable) transition. The shooting method maps this simulation over a batch of candidate action sequences and keeps the best. Proved native and axiom-free: the simulation fold (built by List.rec applying the supplied two-argument dynamics), its cons recurrence, and a worked additive-dynamics trajectory. The candidate generation and objective scoring are executable concerns; what is proved here is the deterministic rollout. Requires nnrat and data/List.rec (both in the D63 checkpoint). Scope (measured by the kernel): this module has 1 worked instances (statements about specific values) and 2 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.shooting` prints this classification.

shooting/simulate :
  (x₁ : ℚ≥0 → ℚ≥0 → ℚ≥0) (x₂ : ℚ≥0) (x₃ : List ℚ≥0)
  → ℚ≥0

shooting/simulate-cons :
  (dynamics : ℚ≥0 → ℚ≥0 → ℚ≥0) (initial action : ℚ≥0) (tail : List ℚ≥0)
  → shooting/simulate dynamics initial (data/cons ℚ≥0 action tail) = dynamics (shooting/simulate dynamics initial tail) action

shooting/simulate-empty :
  (dynamics : ℚ≥0 → ℚ≥0 → ℚ≥0) (initial : ℚ≥0)
  → shooting/simulate dynamics initial [] = initial

shooting/simulate-example :
  → shooting/simulate (fun state => fun action => state + action) 0 [1, 2, 3] = 6