Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.trust-region

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/trust_region.clj5 definitions, 5 theorems

AHoF O16 worked trust region step acceptance over exact rationals. Threshold 1/2 and a descent candidate 0 against the current point 2. When the predicted reduction is matched (actual 1, predicted 1) the ratio is 1, which clears the threshold, so the step is accepted and the update moves to the candidate 0. When the model over-predicts (actual 1, predicted 4) the ratio is 1/4, which fails the threshold, so the step is rejected and the update keeps the current point 2. The two decisions exercise both sides of the accept-or-reject branch, and are proved by reflexivity of the decided comparison. Scope (measured by the kernel): this module has 5 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.trust-region` prints this classification.

ahof-o16/threshold :
  → ℚ≥0

ahof-o16/candidate :
  → ℚ

ahof-o16/current :
  → ℚ

ahof-o16/accept-ratio :
  → ℚ≥0

ahof-o16/reject-ratio :
  → ℚ≥0

ahof-o16/accept-decision-is-true :
  → lis/extends? ahof-v40/lo ahof-o16/accept-ratio = data/true

ahof-o16/reject-decision-is-false :
  → lis/extends? ahof-v40/lo ahof-o16/reject-ratio = data/false

ahof-o16/accepted-step-is-candidate :
  → decision/trust-region-update (extends?) ahof-d63/value ahof-o31/initial = ahof-d63/value
  where extends? := lis/extends? ahof-v40/lo ahof-o16/accept-ratio

ahof-o16/rejected-step-is-current :
  → decision/trust-region-update (extends?) ahof-d63/value ahof-o31/initial = ahof-o31/initial
  where extends? := lis/extends? ahof-v40/lo ahof-o16/reject-ratio

ahof-o16/trust-region :
  → proposition/conjunction (lis/extends? ahof-v40/lo ahof-o16/accept-ratio = data/true) (conjunction)
  where conjunction := proposition/conjunction (lis/extends? ahof-v40/lo ahof-o16/reject-ratio = data/false) (proposition/conjunction (decision/trust-region-update (lis/extends? ahof-v40/lo ahof-o16/accept-ratio) ahof-d63/value ahof-o31/initial = ahof-d63/value) (decision/trust-region-update (lis/extends? ahof-v40/lo ahof-o16/reject-ratio) ahof-d63/value ahof-o31/initial = ahof-o31/initial))