Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.exact-inference

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

AHoF D2 worked exact Bayesian inference by enumeration. A two-node binary network: a uniform prior over A in {0,1} and a conditional P(B|A). Enumerating the hidden variable A gives P(B=1) = 1/2*1/2 + 1/2*1 = 3/4 and P(B=0) = 1/2*1/2 + 1/2*0 = 1/4, which sum to one. All values are exact rationals; the marginals are proved by cross-product reflexivity. 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.exact-inference` prints this classification.

ahof-d2/grid :
  → Finset ℕ

ahof-d2/prior :
  (x₁ : ℕ)
  → ℚ≥0

ahof-d2/likelihood-true :
  (x₁ : ℕ)
  → ℚ≥0

ahof-d2/likelihood-false :
  (x₁ : ℕ)
  → ℚ≥0

ahof-d2/marginal-true :
  → ℚ≥0

ahof-d2/marginal-false :
  → ℚ≥0

ahof-d2/marginal-values :
  → proposition/conjunction (ahof-d2/marginal-true = 3/4) (ahof-d2/marginal-false = 1/4)

ahof-d2/normalization :
  → ahof-d2/marginal-true + ahof-d2/marginal-false = 1

ahof-d2/exact-inference :
  → proposition/conjunction (conjunction) (ahof-d2/marginal-true + ahof-d2/marginal-false = 1)
  where conjunction := proposition/conjunction (ahof-d2/marginal-true = 3/4) (ahof-d2/marginal-false = 1/4)