Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.variable-elimination

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

AHoF D3 Variable Elimination: exact inference by successively eliminating (marginalizing out) variables from the factor graph. Eliminating a variable sums the factor over that variable's values; for a binary variable the marginal is the sum of the two slices: marginalize f-false f-true = f-false + f-true over exact nonnegative rational factor entries (the general case folds the sum over all values of the eliminated variable). Proved native and axiom-free: the marginalization sum, and the guarantee that a marginal dominates each of its summands (f-true <= marginal), so summing out never loses probability mass. The variable elimination ordering (a pluggable strategy) and the factor products that precede each elimination are executable concerns; what is proved here is the marginalization sum and its mass-preservation bound. Requires nnrat/add, nnrat/at-most, and the decidable nnrat order (D63). Scope (measured by the kernel): this module has 2 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.variable-elimination` prints this classification.

variable-elimination/marginalize :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

variable-elimination/marginalize-unfold :
  (f-false f-true : ℚ≥0)
  → astar/f-value f-false f-true = f-false + f-true

variable-elimination/marginalize-example :
  → astar/f-value 3 4 = 7

variable-elimination/marginal-dominates-slice :
  → 4 ≤ astar/f-value 3 4