Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.belief-propagation

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

AHoF D4 Sum-Product (Belief Propagation): approximate marginal inference by passing messages on the factor graph until convergence. A variable node's outgoing message is the pointwise PRODUCT of the messages it receives from its other neighbors (the belief is the product of all incoming messages): combine-messages m1 m2 = m1 * m2 over exact nonnegative rationals (two incoming messages; the general node folds the product over all neighbors). Proved native and axiom-free: the combination unfolds to m1 * m2 for all messages m1 and m2, and two worked instances, 3 * 4 = 12 and a zero message 0 * 7 = 0, that reduce by reflexivity. The factor-node sum-product messages and the message schedule are executable concerns; what is proved here is the variable-node message product. Requires nnrat/multiply (in the D63 checkpoint). 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.belief-propagation` prints this classification.

belief-propagation/combine-messages :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

belief-propagation/combine-messages-unfold :
  (m1 m2 : ℚ≥0)
  → baseline/contribution m1 m2 = m1 · m2

belief-propagation/combine-messages-example :
  → baseline/contribution 3 4 = 12

belief-propagation/zero-message-annihilates :
  → baseline/contribution 0 7 = 0