## 2010-05-28

### 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 < jj′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 qN.

• sum > s

By (3) we can shrink the segment on the left, provided we can, that is, if pq. But since s > 0, this is implied by pN, 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.