Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.bayesian-learning

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

AHoF D11 worked Bayesian parameter learning over exact rationals. Starting from a prior mass 1/2, the first datum has likelihood 3/2, updating the mass to 1/2 * 3/2 = 3/4; the second datum has likelihood 4/3, updating the posterior to 3/4 * 4/3 = 1. Folding the likelihoods through the prior gives the posterior mass, proved by cross-product equivalence. 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.bayesian-learning` prints this classification.

ahof-d11/prior :
  → ℚ≥0

ahof-d11/first-update :
  → ℚ≥0

ahof-d11/posterior :
  → ℚ≥0

ahof-d11/first-update-is-three-quarters :
  → ahof-d11/first-update = 3/4

ahof-d11/posterior-is-one :
  → ahof-d11/posterior = 1

ahof-d11/bayesian-learning :
  → proposition/conjunction (ahof-d11/first-update = 3/4) (ahof-d11/posterior = 1)