Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.projection-methods

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/projection_methods.clj3 definitions, 6 theorems

Kochenderfer constrained/rounded update rules as higher-order-function compositions, proved axiom-free, extending the 222 AHoF catalog: O10.1 projected gradient descent : project the updated point onto a box [lo,hi] D12.3 restricted policy gradient : clip the update to a trust region [lo,hi] O22.2 LP-relaxation-and-round : round a fractional LP value by a 1/2 threshold Both projection/clipping rules are clamp compositions; the feasibility guarantees (result lies in [lo,hi]) reuse rainbow.math.logic.clamp-range (clamp-at-most-hi, lo-at-most-clamp). Rounding uses the decidable order + if-data. Native and axiom-free; chains clamp-range (-> nnrat-minmax) on d63.

Depends onmath.rational.nnrat.minmaxmath.logic.clamp-range

opt/projected-gradient-step :
  (x₁ x₂ x₃ : ℚ≥0)
  → ℚ≥0

policy/restricted-gradient-step :
  (x₁ x₂ x₃ : ℚ≥0)
  → ℚ≥0

opt/lp-round :
  (x₁ : ℚ≥0)
  → ℚ≥0

opt/projected-below-hi :
  (x lo hi : ℚ≥0)
  → opt/projected-gradient-step x lo hi ≤ hi

opt/projected-above-lo :
  (x lo hi : ℚ≥0)
  (ordered : lo ≤ hi)
  → lo ≤ opt/projected-gradient-step x lo hi

policy/restricted-within-trust-hi :
  (raw lo hi : ℚ≥0)
  → opt/projected-gradient-step raw lo hi ≤ hi

policy/restricted-within-trust-lo :
  (raw lo hi : ℚ≥0)
  (ordered : lo ≤ hi)
  → lo ≤ opt/projected-gradient-step raw lo hi

opt/lp-round-up-example :
  → opt/lp-round 3/4 = 1

opt/lp-round-down-example :
  → opt/lp-round 1/4 = 0