Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.exploration-strategies

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/exploration_strategies.clj6 definitions, 8 theorems

Kochenderfer 'Algorithms for Decision Making' Ch.15 bandit exploration strategies, expressed as higher-order-function compositions and proved axiom-free (core structural property per algorithm), extending the 222 AHoF catalog: D15.3 epsilon-greedy : explore/exploit branch (Bool) over a random bit D15.4 explore-then-commit : two-phase branch on a round>=k threshold (decide-at-most) D15.5 softmax exploration : stochastic policy, probability = weight / total (divide) D15.6 quantile exploration : optimistic additive bonus (mean + bonus), pick the max Greedy exploitation reuses rainbow.math.rational.nnrat.minmax (max dominates both arms). Native and axiom-free; chains nnrat-minmax on the d63 base.

Depends onmath.rational.nnrat.minmax

explore/epsilon-greedy :
  (x₁ : Prop) (x₂ : data/Bool) (x₃ x₄ : ℚ≥0)
  → ℚ≥0

explore/greedy-value :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

explore/explore-then-commit :
  (x₁ : Prop) (x₂ : data/Bool) (x₃ x₄ : ℚ≥0)
  → ℚ≥0

explore/quantile-score :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

explore/quantile-select :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

explore/softmax-probability :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

explore/epsilon-greedy-exploits :
  (cond : Prop) (exploit random : ℚ≥0)
  → explore/epsilon-greedy cond data/false exploit random = exploit

explore/epsilon-greedy-explores :
  (cond : Prop) (exploit random : ℚ≥0)
  → explore/epsilon-greedy cond data/true exploit random = random

explore/greedy-dominates-left :
  (v0 v1 : ℚ≥0)
  → v0 ≤ dp/knapsack-cell v0 v1

explore/greedy-dominates-right :
  (v0 v1 : ℚ≥0)
  → v1 ≤ dp/knapsack-cell v0 v1

explore/explore-then-commit-commits :
  (cond : Prop) (greedy uniform : ℚ≥0)
  → explore/explore-then-commit cond data/true greedy uniform = greedy

explore/explore-then-commit-explores :
  (cond : Prop) (greedy uniform : ℚ≥0)
  → explore/explore-then-commit cond data/false greedy uniform = uniform

explore/quantile-optimism-example :
  → dp/knapsack-cell (astar/f-value 1/2 0) (astar/f-value 1/2 1/2) = 1

explore/softmax-probability-example :
  → accuracy/accuracy 3 4 = 3/4