Gematric Search

Given an array A.(0 ≤ i < N) of nonnegative integers, that is:

(0)   ⟨∀ i : 0 ≤ i < N : A.i ≥ 0⟩

and a positive integer s > 0, we want to find a segment of A that sums to s, if it exists. Define:

      S.i.j = ⟨∑ k : 0 ≤ i ≤ k < j ≤ N : A.k⟩

The gematric search for s in A is to find, if possible, a pair (p, q) such that S.p.q = s (it is hoped that conoisseurs would readily make the connection). Note a number of things:

• S.i.j is a total function on i, j
• By definition, the sum on an empty range is zero:

  (1)   S.i.i = 0
  

  for all integer i.

• For arguments in range of A, S.i.j is monotone on its second argument and antitone on its first. That is, given 0 ≤ i′ ≤ i < j ≤ j′ ≤ N:

  (2)   S.i.j ≤ S.i.j′
  (3)   S.i.j ≤ S.i′.j
  

What should the result be if no such segment is present in A? One possibility would be setting a flag found, such that the program ensures:

      ¬found ∨ S.p.q = s

An alternative would be to guarantee some condition on (p, q) equivalent by design to found. Given that s ≠ 0, one such condition would be satisfied by S.p.q = 0 as a suitable sentinel. By (1), this is implied by p = q, and we choose the weaker postcondition:

(4)   p = q ∨ S.p.q = s

Now (4) is trivially satisfied by:

{ A.(0 ≤ i < N) ∧ s > 0 }
gemsearch ≡
   p := 0; q := 0; sum := 0;
   { reduce |sum - s| under invariance of (4) }
{ p = q ∨ S.p.q = s }

where sum = S.p.q at each step. How should we meet the refinement obligation in the program? We clearly have three cases:

• sum = s

  We have found our segment, and we can stop looking.

• sum < s

  By (2) we can extend the segment on the right, provided we can, that is, if q ≠ N.

• sum > s

  By (3) we can shrink the segment on the left, provided we can, that is, if p ≠ q. But since s > 0, this is implied by p ≠ N, a weaker condition symmetric to the previous one and thus preferable. It is also suitable for the repetition guard, since its negation implies the postcondition.

We have:

{ A.(0 ≤ i < N) ∧ s > 0 }
gemsearch ≡
   p := 0; q := 0; sum := 0;
   do p ≠ N ∧ sum ≠ s →
      if sum < s ∧ q ≠ N → sum := sum + A.q; q := q + 1
      [] sum > s         → sum := sum - A.p; p := p + 1
      [] … → ?
      fi
   od
{ p = q ∨ S.p.q = s }

The conditional is not exhaustive. Let's calculate what the obligations are for third case:

   ¬((sum < s ∧ q ≠ N) ∨ sum > s)
≡ { DeMorgan, twice }
   (sum ≥ s ∨ q = N) ∧ sum ≤ s
≡ { Distribute }
   (sum ≥ s ∧ sum ≤ s) ∨ (q = N ∧ sum ≤ s)
≡ { Tertium non datur }
   sum = s ∨ (q = N ∧ sum ≤ s)
⇐ { Loop condition }
   q = N ∧ sum < s

This condition expresses a deficient suffix of A which is, by (3), as large as it can be, hence we can quit the search. Left-factoring the common condition on s, we arrive at our final program:

{ A.(0 ≤ i < N) ∧ s > 0 }
gemsearch ≡
   p := 0; q := 0; sum := 0;
   do p ≠ N ∧ sum ≠ s →
      if sum < s →
         if q ≠ N → sum := sum + A.q; q := q + 1
         [] q = N → p := N
         fi
      [] sum > s → sum := sum - A.p; p := p + 1
      fi
   od
{ p = q ∨ S.p.q = s }

The algorithm is of complexity obviously linear on N, since no element of A is accessed more than twice.