Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.prob-programming

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

AHoF V25 Probabilistic Programming: an observe/factor statement reweights the trace by the observation likelihood; the trace score combines two factors multiplicatively score a b = a * b. Proved native and axiom-free (worked scores by cross-product equivalence). Scope (measured by the kernel): this module has 3 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.prob-programming` prints this classification.

prob-prog/score :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

prob-prog/likely-trace :
  → ℚ≥0

prob-prog/unlikely-trace :
  → ℚ≥0

prob-prog/score-unfold :
  (a b : ℚ≥0)
  → prob-prog/score a b = a · b

prob-prog/likely-trace-is-one-eighth :
  → model-est/good-model = 1/8

prob-prog/unlikely-trace-is-one-sixteenth :
  → model-est/poor-model = 1/16

prob-prog/combined :
  → proposition/conjunction (model-est/good-model = 1/8) (model-est/poor-model = 1/16)