Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.linear-regression-vf

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

AHoF D29 Linear Regression Value Function: approximate the value function as a linear combination of state features, V(s) = w . phi(s). The prediction is the weighted sum of the feature values by the fitted weights: predict w1 f1 w2 f2 = w1*f1 + w2*f2 over exact nonnegative rationals (two features; the general case folds over the feature vector). Proved native and axiom-free: the linear prediction and worked instances that reduce by reflexivity. The feature map phi (a supplied HOF from states to feature vectors) and the least-squares / TD weight fit are executable concerns; the weights and feature values are supplied rationals. What is proved here is the deterministic linear combination. Requires nnrat/add and nnrat/multiply (in the D63 checkpoint). Scope (measured by the kernel): this module has 1 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.linear-regression-vf` prints this classification.

linear-vf/predict :
  (x₁ x₂ x₃ x₄ : ℚ≥0)
  → ℚ≥0

linear-vf/predict-unfold :
  (w1 f1 w2 f2 : ℚ≥0)
  → ekf/update w1 f1 w2 f2 = w1 · f1 + w2 · f2

linear-vf/predict-example :
  → ekf/update 2 3 1 4 = 10