Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.concrete-reachability

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

AHoF V44 Concrete Reachability: the simplest reachability analysis -- push a finite set of concrete sample states one step forward through the dynamics and collect the images. The one-step reachable set is the map of the transition over the current states: reach-step step states = [ step x | x in states ]. Iterating this from the initial set traces a concrete under-approximation of the reachable set (exact for the sampled points; the set-valued over-approximation is the job of the interval/zonotope propagators). Proved native and axiom-free: the reach-step map (built by List.rec producing a list), its cons recurrence, and a worked forward image. What is proved is the concrete forward image; the sampling density and the abstraction to a covering set are executable concerns. Requires nat/nnrat, nnrat/add, and data/List.rec (all 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.concrete-reachability` prints this classification.

reachability/reach-step :
  (x₁ : ℚ≥0 → ℚ≥0) (x₂ : List ℚ≥0)
  → List ℚ≥0

reachability/reach-step-cons :
  (step : ℚ≥0 → ℚ≥0) (head : ℚ≥0) (tail : List ℚ≥0)
  → reachability/reach-step step (data/cons ℚ≥0 head tail) = data/cons ℚ≥0 (step head) (reachability/reach-step step tail)

reachability/reach-step-example :
  → reachability/reach-step (fun x => 1 + x) [1, 2, 3] = [2, 3, 4]

reachability/reach-step-empty :
  → reachability/reach-step (fun x => 1 + x) [] = []