Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.hmc

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

AHoF V24 Hamiltonian Monte Carlo -- the leapfrog integrator that simulates Hamiltonian dynamics to make distant, high-acceptance proposals. Leapfrog alternates a full position drift with momentum half-kicks; the position drift moves the state by the step size times the (mass-scaled) momentum: drift q step momentum = q + step * momentum over the finite-vector state. The potential-energy gradient (the momentum kick -step/2 * gradU) and the Metropolis-Hastings accept/reject on the Hamiltonian are separate concerns (the gradient is supplied; the accept test is ahof-metropolis / executable). What is proved here is the deterministic position-drift recurrence and worked instances from a zero position, where a unit step lands exactly on the momentum. Requires the shared finite-vector operations (vector/add, vector/scale) over signed rationals -- carried by the D63 checkpoint via the vector layer. 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.hmc` prints this classification.

Depends onmath.finite.vector

hmc/drift :
  (x₁ : List ℚ) (x₂ : ℚ≥0) (x₃ : List ℚ)
  → List ℚ

hmc/drift-unfold :
  (q : List ℚ) (step : ℚ≥0) (momentum : List ℚ)
  → hmc/drift q step momentum = vector/add q (vector/scale step momentum)

hmc/drift-unit-2d-example :
  → hmc/drift [signed/from-nnrat 0, signed/from-nnrat 0] 1 [signed/from-nnrat 3, signed/from-nnrat 2] = [signed/from-nnrat 3, signed/from-nnrat 2]

hmc/drift-unit-3d-example :
  → hmc/drift [signed/from-nnrat 0, signed/from-nnrat 0, signed/from-nnrat 0] 1 [signed/from-nnrat 2, signed/from-nnrat 4, signed/from-nnrat 6] = [signed/from-nnrat 2, signed/from-nnrat 4, signed/from-nnrat 6]