Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.polytope

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

AHoF V34 Polytope Propagation: represent a reachable set as an intersection of halfspaces (a polytope) and propagate it forward. A point lies in a two-constraint polytope exactly when it satisfies both halfspace inequalities a_i . x <= b_i: in-polytope? v1 b1 v2 b2 = (v1 <= b1) AND (v2 <= b2) (boolean AND via logic/if-data over the two exact-rational constraint decisions). Proved native and axiom-free: the membership conjunction with its unfold, a point inside both halfspaces, and a point violating one. 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.polytope` prints this classification.

polytope/in-polytope? :
  (x₁ x₂ x₃ x₄ : ℚ≥0)
  → data/Bool

polytope/in-polytope-unfold :
  (v1 b1 v2 b2 : ℚ≥0)
  → polytope/in-polytope? v1 b1 v2 b2 = logic/if-data data/Bool (audit/decide-nnrat-at-most v1 b1 = audit/decide-nnrat-at-most v1 b1) (audit/decide-nnrat-at-most v1 b1) (audit/decide-nnrat-at-most v2 b2) data/false

polytope/inside-both-halfspaces :
  → polytope/in-polytope? 1/2 3/4 1/2 3/4 = data/true

polytope/violates-halfspace-outside :
  → polytope/in-polytope? 1/2 3/4 3/4 1/2 = data/false