Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.value-of-information

The Applied Higher-Order Functions catalogue src/rainbow/algorithms/proofs/ahof/value_of_information.clj3 definitions, 4 theorems

AHoF D19 worked value of information over signed rationals. The value of information is the signed difference EU(with info) - EU(without info). With a worked decision problem where informed expected utility is 3/4 and uninformed is 1/2, the value of information is exactly 1/4, and the worked certificates 1/2 <= 3/4 and 1/4 nonnegative are proved. That information never reduces expected utility is the classical property of the value of information and is not proved here. Signed subtraction is the addition-only Grothendieck construction, so no primitive subtraction is needed. 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.value-of-information` prints this classification.

ahof-d19/eu-with-info

DefinitionSource, line 108

ahof-d19/eu-with-info :
  → ℚ

ℚ = signed/SignedRational

ahof-d19/eu-without-info

DefinitionSource, line 112

ahof-d19/eu-without-info :
  → ℚ

ℚ = signed/SignedRational

ahof-d19/value-of-information

DefinitionSource, line 116

ahof-d19/value-of-information :
  → ℚ

ℚ = signed/SignedRational

ahof-d19/information-never-hurts

TheoremWorked exampleNo axiomsSource, line 128

ahof-d19/information-never-hurts :
  → 1/2 ≤ 3/4

≤ = nnrat/at-most

ahof-d19/voi-equals-quarter

TheoremWorked exampleNo axiomsSource, line 139

ahof-d19/voi-equals-quarter :
  → ahof-d19/value-of-information = signed/from-nnrat 1/4

= = signed/equivalent: equality of rational values

ahof-d19/voi-nonnegative

TheoremWorked exampleNo axiomsSource, line 148

ahof-d19/voi-nonnegative :
  → signed/nonnegative ahof-d19/value-of-information

ahof-d19/value-of-information-theorem

TheoremWorked exampleNo axiomsSource, line 157

ahof-d19/value-of-information-theorem :
  → proposition/conjunction (1/2 ≤ 3/4) (conjunction)
  where conjunction := proposition/conjunction (ahof-d19/value-of-information = signed/from-nnrat 1/4) (signed/nonnegative ahof-d19/value-of-information)

= = signed/equivalent: equality of rational values≤ = nnrat/at-most