= Solution
Use the <sorted sparse dot product> merge, processing a coordinate only when it appears in both <supports of a vector>:
``
def dotProduct(vec1: Node, vec2: Node): Double = {
require(vec1 != null && vec2 != null)
require(vec1.index == vec2.index)
var p = vec1.next
var q = vec2.next
var result = 0.0
while ((p ne vec1) && (q ne vec2)) {
if (p.index < q.index) p = p.next
else if (q.index < p.index) q = q.next
else {
result += p.value * q.value
p = p.next
q = q.next
}
}
result
}
``
Both structures must satisfy the <representation invariant>; equal dimension is checked explicitly. The <loop invariant> says that `result` contains exactly the products for all matching indices already passed, and that every skipped unequal index has zero in the other <vector>. The latter follows from sortedness: if `p.index < q.index`, that index cannot appear at `q` or later, and all earlier entries of the other <vector> have already been settled. Equality contributes its product exactly once. The total number of remaining ordinary entries is a <loop variant>; every iteration advances at least one cursor. Once either cursor reaches its header, all remaining entries pair with zeros. Thus \b[the exact-arithmetic result is $\sum_i vec1_i vec2_i$]. With $k_1,k_2$ stored entries, <time complexity> is $O(k_1+k_2+1)$ and <auxiliary space> is constant. Floating-point products and additions may round or overflow even when input coordinates are finite; no exact real-arithmetic accuracy claim is made for `Double`.
Back to article page
