Reference · Algorithm guarantees

rainbow.algorithms.proofs.inner-product

Algorithm guaranteessrc/rainbow/algorithms/proofs/inner_product.clj1 definitions, 3 theorems

The vector dot product (inner product) over signed-rational vectors: dot [a1..an] [b1..bn] = sum_i a_i * b_i This is a zip of the two component lists with signed multiplication, summed with signed addition -- a nested `data/List.rec` that reduces the two vectors to a single signed scalar (the shape of `vector/add`, but accumulating a sum of products rather than a vector). It reuses `signed/multiply` and unblocks inner-product methods: hypergradient learning-rate updates, cosine similarity, and conjugate-gradient direction tests. Requires `signed/multiply` (from rainbow.math.rational.signed.multiply) in the environment. Scope (measured by the kernel): this module has 3 worked instances (statements about specific values). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.inner-product` prints this classification.

Depends onmath.rational.signed.multiply

vector/dot :
  (x₁ x₂ : List ℚ)
  → ℚ

vector/dot-nil :
  → vector/dot [] [] = 0

vector/dot-example :
  → vector/dot [signed/from-nnrat 2, signed/from-nnrat 3] [signed/from-nnrat 1, signed/from-nnrat 2] = signed/from-nnrat 8

vector/dot-3d-example :
  → vector/dot [signed/from-nnrat 1, signed/from-nnrat 2, signed/from-nnrat 3] [signed/from-nnrat 1, signed/from-nnrat 1, signed/from-nnrat 1] = signed/from-nnrat 6