Reference · Algorithm guarantees
rainbow.algorithms.proofs.decision-network
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
decision/network-value : (outcomes : Finset ℕ) (probability utility : ℕ → ℚ≥0) → ℚ≥0
Finset = finset-data/Finsetℕ = data/Natℚ≥0 = nnrat/NonnegativeRational
decision/network-value-unfold
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