Skip to content
Rainbow docs menu

Reference · Algorithm guarantees

rainbow.algorithms.proofs.decision-network

Algorithm guaranteessrc/rainbow/algorithms/proofs/decision_network.clj1 definitions, 1 theorems

Decision network evaluation over exact rationals. A decision network combines a chance node (a finite probability distribution over outcomes) with a utility node (a payoff for each outcome); evaluating the network is taking the expected utility -- the probability-weighted sum of the utilities over the outcomes (AHoF D18). This reuses the finite exact-rational expectation engine, with the chance masses as the distribution and the utilities as the value function. Scope (measured by the kernel): this module has 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.decision-network` prints this classification.

decision/network-value

DefinitionSource, line 40

decision/network-value :
  (outcomes : Finset ℕ) (probability utility : ℕ → ℚ≥0)
  → ℚ≥0

Finset = finset-data/Finsetℕ = data/Natℚ≥0 = nnrat/NonnegativeRational

decision/network-value-unfold

TheoremHolds by unfolding a definitionNo axiomsSource, line 57

decision/network-value-unfold :
  (outcomes : Finset ℕ) (probability utility : ℕ → ℚ≥0)
  → decision/network-value outcomes probability utility = probability/nnrat-expectation ℕ outcomes probability utility

= = equality/EqFinset = finset-data/Finsetℕ = data/Natℚ≥0 = nnrat/NonnegativeRational