Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.ucb1

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

AHoF D57 UCB1 (bandit arm selection): pull the arm with the largest upper- confidence-bound score UCB_i = mean_i + sqrt(2 ln t / n_i). With two arms the policy keeps the larger score and prefers arm 0 when its UCB is at least arm 1's: prefers-arm-zero? u0 u1 = decide (u1 <= u0) best-score u0 u1 = if (u1 <= u0) then u0 else u1 (the larger UCB) over exact rationals (the UCB eliminator over nnrat). Proved native and axiom-free: the preference decision, the best-score selection, a worked selection, and that the preference flips when arm 1's score is larger. Requires audit/decide-nnrat-at-most, logic/if-data (both in the D63 checkpoint). Scope (measured by the kernel): this module has 3 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.ucb1` prints this classification.

ucb1/prefers-arm-zero? :
  (x₁ x₂ : ℚ≥0)
  → data/Bool

ucb1/best-score :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

ucb1/prefers-higher-arm :
  → bo/is-safe 3/4 1/2 = data/true

ucb1/selects-higher-value :
  → rl-fal/best-q 3/4 1/2 = 3/4

ucb1/switches-when-lower :
  → bo/is-safe 1/2 3/4 = data/false