Reference · Algorithm guarantees

rainbow.algorithms.proofs.exact-inference

Algorithm guaranteessrc/rainbow/algorithms/proofs/exact_inference.clj2 definitions, 4 theorems

Exact Bayesian inference by enumeration over a finite hidden variable. A marginal is the sum, over every value of a finite hidden variable, of the factored joint `likelihood * prior`. This is exactly the finite rational expectation engine, exposed here under the inference reading and connected to the explicit enumerated factored joint, which opens the Bayesian-network cone (AHoF D1-D16).

inference/nnrat-joint.{u} :
  (H : Type u) (prior likelihood : H → ℚ≥0) (hidden : H)
  → ℚ≥0

inference/nnrat-marginal.{u} :
  (H : Type u) (grid : Finset H) (prior likelihood : H → ℚ≥0)
  → ℚ≥0

inference/nnrat-joint-unfold.{u} :
  (H : Type u) (prior likelihood : H → ℚ≥0) (hidden : H)
  → inference/nnrat-joint H prior likelihood hidden = likelihood hidden · prior hidden

inference/nnrat-marginal-unfold.{u} :
  (H : Type u) (grid : Finset H) (prior likelihood : H → ℚ≥0)
  → inference/nnrat-marginal H grid prior likelihood = probability/nnrat-expectation H grid prior likelihood

inference/nnrat-marginal-is-enumerated-joint.{u} :
  (H : Type u) (grid : Finset H) (prior likelihood : H → ℚ≥0)
  → inference/nnrat-marginal H grid prior likelihood = list/nnrat-map-sum H (joint) (finset-data/enumeration H grid)
  where joint := inference/nnrat-joint H prior likelihood

inference/nnrat-marginal-transfer.{u} :
  (H : Type u) (grid : Finset H) (prior left-likelihood right-likelihood : H → ℚ≥0)
  → proposition/conjunction (marginal₃ = expectation₁) (marginal = expectation)
  where expectation := probability/nnrat-expectation H grid prior right-likelihood
  where expectation₁ := probability/nnrat-expectation H grid prior left-likelihood
  where marginal := inference/nnrat-marginal H grid prior right-likelihood
  where marginal₃ := inference/nnrat-marginal H grid prior left-likelihood