Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.feasibility

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

Constraint feasibility checking (the conjunctive dual of the SAT clause and the model-checking companion of V50): a candidate is feasible when ALL of its constraints are satisfied. Given the per-constraint truth values, feasibility is their conjunction: feasible? constraints = fold and true constraints. Proved native and axiom-free (a boolean fold via data/List.rec + logic/if-data, no rational arithmetic): the fold, its cons recurrence, and worked constraint sets. This is the feasibility test underlying constraint-satisfaction search and the safety-specification check of bounded model checking (a run is a counterexample when it violates any constraint, i.e. is NOT feasible). The constraint evaluation itself is an executable concern; what is proved here is the conjunctive feasibility fold. Requires data/Bool, data/List.rec, and logic/if-data (all in the D63 checkpoint). 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.feasibility` prints this classification.

feasibility/feasible? :
  (x₁ : List data/Bool)
  → data/Bool

feasibility/feasible-cons :
  (head : data/Bool) (tail : List data/Bool)
  → feasibility/feasible? (data/cons data/Bool head tail) = logic/if-data data/Bool (head = head) head (feasibility/feasible? tail) data/false

feasibility/all-satisfied-feasible :
  → feasibility/feasible? [data/true, data/true] = data/true

feasibility/one-violated-infeasible :
  → feasibility/feasible? [data/true, data/false, data/true] = data/false

feasibility/unconstrained-feasible :
  → feasibility/feasible? [] = data/true