Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.receding-horizon

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

AHoF D31 Receding Horizon Control (model-predictive control): rather than commit to a whole open-loop plan, the controller solves the finite-horizon problem, applies only the FIRST action of the resulting plan, then re-solves from the new state at the next step. The control law is the head of the plan: first-action default plan = head plan (default if the plan is empty). Proved native and axiom-free: the first-action extraction (built by List.rec), its cons law (the first action of a nonempty plan is its head), and a worked instance. Re-solving the finite-horizon optimization each step is an executable concern; what is proved here is that the applied control is exactly the plan's first action -- the defining feature that distinguishes receding-horizon from open-loop control. Requires nnrat and data/List.rec (both in the D63 checkpoint). 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.receding-horizon` prints this classification.

mpc/first-action :
  (x₁ : ℚ≥0) (x₂ : List ℚ≥0)
  → ℚ≥0

mpc/first-action-cons :
  (default head : ℚ≥0) (tail : List ℚ≥0)
  → mpc/first-action default (data/cons ℚ≥0 head tail) = head

mpc/first-action-example :
  → mpc/first-action 0 [5, 2, 8] = 5

mpc/first-action-empty :
  → mpc/first-action 0 [] = 0