Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.natural-inclusion

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/natural_inclusion.clj1 definitions, 3 theorems

AHoF V41 Natural Inclusion Function: replace each variable in an expression by its interval and evaluate with interval arithmetic to get a guaranteed enclosure [lo, hi] of the range; the true range is contained, so a candidate value is certified within the enclosure exactly when it lies between the bounds: encloses? lo hi value = (lo <= value) AND (value <= hi) (boolean AND via logic/if-data over the two exact-rational order decisions). Proved native and axiom-free: the enclosure test with its unfold, an enclosed value, and a value below the lower bound. Requires audit/decide-nnrat-at-most, logic/if-data (both in the D63 checkpoint). Scope (measured by the kernel): this module has 2 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.natural-inclusion` prints this classification.

nat-incl/encloses? :
  (x₁ x₂ x₃ : ℚ≥0)
  → data/Bool

nat-incl/encloses-unfold :
  (lo hi value : ℚ≥0)
  → nat-incl/encloses? lo hi value = logic/if-data data/Bool (audit/decide-nnrat-at-most lo value = audit/decide-nnrat-at-most lo value) (audit/decide-nnrat-at-most lo value) (audit/decide-nnrat-at-most value hi) data/false

nat-incl/value-enclosed :
  → nat-incl/encloses? 1/2 3/2 1 = data/true

nat-incl/value-below-not-enclosed :
  → nat-incl/encloses? 1/2 3/2 1/4 = data/false