Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.reachability-eda

The Applied Higher-Order Functions catalogue src/rainbow/algorithms/proofs/ahof/reachability_eda.clj6 definitions, 6 theorems

Final Kochenderfer straggler cores (reachability, robustness envelope, adaptive SA, estimation-of-distribution program search) as higher-order-function compositions, proved axiom-free, extending the 222 AHoF catalog: V10.3 backward reachability : a state is back-reachable if SOME successor is (OR) V9.3 conservative linearization : reachable-set upper envelope = center + radius O8.7 adaptive simulated annealing: accept-if-better keeps the lower cost (min) O23.10 probabilistic grammar EDA : move the grammar toward elite (convex update) O23.14 PIPE prototype tree EDA : move the prototype toward elite (convex update) Includes a small boolean-OR (dual of rainbow.math.logic.boolean-and) for reachability. Native and axiom-free; chains nnrat-convex (-> wsum2, minmax) on d63.

Depends onmath.rational.nnrat.convex

boolean/or

DefinitionSource, line 50

boolean/or :
  (x₁ x₂ : data/Bool)
  → data/Bool

reach/backward-reachable

DefinitionSource, line 65

reach/backward-reachable :
  (x₁ x₂ : data/Bool)
  → data/Bool

reach/conservative-upper

DefinitionSource, line 80

reach/conservative-upper :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

ℚ≥0 = nnrat/NonnegativeRational

opt/asa-accept

DefinitionSource, line 92

opt/asa-accept :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

ℚ≥0 = nnrat/NonnegativeRational

eda/grammar-update

DefinitionSource, line 105

eda/grammar-update :
  (x₁ x₂ x₃ x₄ : ℚ≥0)
  → ℚ≥0

ℚ≥0 = nnrat/NonnegativeRational

eda/pipe-update

DefinitionSource, line 123

eda/pipe-update :
  (x₁ x₂ x₃ x₄ : ℚ≥0)
  → ℚ≥0

ℚ≥0 = nnrat/NonnegativeRational

boolean/or-true-left

TheoremHolds by unfolding a definitionNo axiomsSource, line 58

boolean/or-true-left :
  (b : data/Bool)
  → boolean/or data/true b = data/true

= = equality/Eq

reach/backward-reach-from-successor

TheoremFor all inputsNo axiomsSource, line 71

reach/backward-reach-from-successor :
  (succ1 : data/Bool)
  → reach/backward-reachable data/true succ1 = data/true

= = equality/Eq

reach/conservative-upper-example

TheoremWorked exampleNo axiomsSource, line 86

reach/conservative-upper-example :
  → astar/f-value 1 1/2 = 3/2

1 = nnrat/one= = nnrat/equivalent: equality of rational values

opt/asa-accept-not-worse

TheoremFor all inputsNo axiomsSource, line 97

opt/asa-accept-not-worse :
  (current candidate : ℚ≥0)
  → opt/asa-accept current candidate ≤ current

ℚ≥0 = nnrat/NonnegativeRational≤ = nnrat/at-most

eda/grammar-update-within-max

TheoremFor all inputsNo axiomsSource, line 111

eda/grammar-update-within-max :
  (w0 w1 old elite : ℚ≥0)
  (hw : w0 + w1 = 1)
  → eda/pipe-update w0 w1 old elite ≤ minmax/max old elite

+ = nnrat/add1 = nnrat/one= = nnrat/equivalent: equality of rational valuesℚ≥0 = nnrat/NonnegativeRational≤ = nnrat/at-most

eda/pipe-update-within-max

TheoremFor all inputsNo axiomsSource, line 129

eda/pipe-update-within-max :
  (w0 w1 old elite : ℚ≥0)
  (hw : w0 + w1 = 1)
  → eda/pipe-update w0 w1 old elite ≤ minmax/max old elite

+ = nnrat/add1 = nnrat/one= = nnrat/equivalent: equality of rational valuesℚ≥0 = nnrat/NonnegativeRational≤ = nnrat/at-most