Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.decision-network

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/decision_network.clj4 definitions, 4 theorems

AHoF D18 worked decision network evaluation over exact rationals. A chance node has two outcomes with probabilities 3/4 and 1/4; the utility node pays 1 for the first outcome and 0 for the second. Evaluating the network is the expected utility 3/4 * 1 + 1/4 * 0 = 3/4. The value is proved by cross-product equivalence over the finite expectation. Scope (measured by the kernel): this module has 4 worked instances (statements about specific values). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.ahof.decision-network` prints this classification.

ahof-d18/outcome-space :
  → Finset ℕ

ahof-d18/probability :
  (x₁ : ℕ)
  → ℚ≥0

ahof-d18/utility :
  (x₁ : ℕ)
  → ℚ≥0

ahof-d18/network-eu :
  → ℚ≥0

ahof-d18/network-eu-is-three-quarters :
  → ahof-d18/network-eu = 3/4

ahof-d18/utility-at-zero-is-one :
  → ahof-d18/utility 0 = 1

ahof-d18/utility-at-one-is-zero :
  → ahof-d18/utility 1 = 0

ahof-d18/decision-network :
  → proposition/conjunction (ahof-d18/network-eu = 3/4) (conjunction)
  where conjunction := proposition/conjunction (ahof-d18/utility 0 = 1) (ahof-d18/utility 1 = 0)