Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.interval-arithmetic

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

AHoF V40 worked interval arithmetic over exact rationals on the interval [1/2, 3/2]. The midpoint 1 lies inside (1/2 <= 1 <= 3/2); 1/4 lies below the lower endpoint and 2 lies above the upper endpoint, so both are outside. Interval addition [1/2,3/2] + [1/2,3/2] = [1, 3] has lower endpoint 1/2 + 1/2 = 1 and upper endpoint 3/2 + 3/2 = 3, each proved by cross-product equivalence (the sums land on non-canonical make-pairs, so nnrat/equivalent is used rather than reflexivity). Proved native and axiom-free. Scope (measured by the kernel): this module has 6 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.interval-arithmetic` prints this classification.

Depends onalgorithms.proofs.interval-membership

ahof-v40/lo :
  → ℚ≥0

ahof-v40/hi :
  → ℚ≥0

ahof-v40/sum-lo-endpoint :
  → ℚ≥0

ahof-v40/sum-hi-endpoint :
  → ℚ≥0

ahof-v40/midpoint-inside :
  → validation/interval-contains? ahof-v40/lo ahof-v40/hi 1 = data/true

ahof-v40/below-outside :
  → validation/interval-contains? ahof-v40/lo ahof-v40/hi 1/4 = data/false

ahof-v40/above-outside :
  → validation/interval-contains? ahof-v40/lo ahof-v40/hi 2 = data/false

ahof-v40/sum-lo :
  → ahof-v40/sum-lo-endpoint = 1

ahof-v40/sum-hi :
  → ahof-v40/sum-hi-endpoint = 3

ahof-v40/interval-arithmetic :
  → proposition/conjunction (validation/interval-contains? ahof-v40/lo ahof-v40/hi 1 = data/true) (contains? = data/false)
  where contains? := validation/interval-contains? ahof-v40/lo ahof-v40/hi 1/4