Reference · Signed rationals

rainbow.math.rational.signed.stl

Signed rationalssrc/rainbow/math/rational/signed/stl.clj3 definitions, 2 theorems

Signed minimum and maximum for signal temporal logic (STL) robustness. The robustness of an STL formula is computed by structural recursion: an atomic predicate contributes a signed margin, conjunction takes the minimum of its parts, disjunction the maximum, and negation the sign flip. Minimum and maximum are selected by the signed comparison decision on cross products, so a worked robustness computation reduces to an exact signed rational.

validation/signed-decide-at-most :
  (x₁ x₂ : ℚ)
  → data/Bool

validation/signed-min :
  (x₁ x₂ : ℚ)
  → ℚ

validation/signed-max :
  (x₁ x₂ : ℚ)
  → ℚ

validation/signed-min-preserved :
  (left right : ℚ)
  (not-below : validation/signed-decide-at-most left right = data/false)
  → validation/signed-min left right = right

validation/signed-max-preserved :
  (left right : ℚ)
  (not-below : validation/signed-decide-at-most left right = data/false)
  → validation/signed-max left right = left