Reference · Algorithm guarantees

rainbow.algorithms.proofs.network-scoring

Algorithm guaranteessrc/rainbow/algorithms/proofs/network_scoring.clj1 definitions, 2 theorems

Additive scoring of a Bayesian network. A decomposable score (BIC/BDeu style) is the sum of a per-node local score over the network's nodes: map the local score over the nodes, then reduce by addition. Because the score decomposes, adding a node adds only its local score -- the property that makes local structure search tractable. Scope (measured by the kernel): this module has 2 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.network-scoring` prints this classification.

scoring/nnrat-total-score :
  (x₁ : ℕ → ℚ≥0) (x₂ : List ℕ)
  → ℚ≥0

scoring/score-empty :
  (local : ℕ → ℚ≥0)
  → scoring/nnrat-total-score local [] = 0

scoring/score-cons :
  (local : ℕ → ℚ≥0) (head : ℕ) (tail : List ℕ)
  → scoring/nnrat-total-score local (data/cons ℕ head tail) = local head + scoring/nnrat-total-score local tail