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.

Observable sharing and executable proofs

Every rational number has an infinite repeating decimal expansion. In particular, every integer admits two decimal expansions: one with and one without a "tail of nines". This means that 1 = 0.9999…, a provable fact that many people still choose to disbelieve. What do I mean here by "provable"? I mean "provable by finitistic reasoning", that is, by a purely algebraic proof free of notions of continuity or convergence. The proof in this particular (and particularly popular) case goes like this:

    x     = 0.9999…
≡ { product by base is shift of decimal point }
  10x     = 9.9999…
≡ { subtraction of finitely-expanded integer }
  10x - 9 = 0.9999…
≡ { identity of decimal expansion }
  10x - 9 = x
≡ { algebra }
   9x     = 9
≡ { cancellation of multiplication }
    x     = 1

The last two steps are elementary consequences of the fact that integers form a ring. The first three steps require justification. By definition, a decimal expansion of a positive real number x is a (possibly semi-infinite) sequence of digits 0 ≤ d_i < 10 such that for all i ≥ N, d_i = 0, and

x = ⟨∑ i :: 10i⋅di⟩

and the decimal point separates the digits corresponding to 10⁰ and 10^-1, namely d₀ from d_-1.

Lemma 0 Any decimal number x can be expressed as the sum of an integer and a (possibly infinite) decimal part

Proof: By definition, x has a finite number of decimal digits to the left of the decimal point, namely for 0 ≤ i < N, hence:

  x
= { definition }
  ⟨∑ i :: 10i⋅di ⟩
= { associativity of addition, a finite number N of times }
  ⟨∑ i : 0 ≤ i < N : 10i⋅di⟩ + ⟨∑ i : 0 > i : 10i⋅di⟩
= { naming the first term }
  n + ⟨∑ i : 0 > i : 10i⋅di⟩

This justifies representing a positive real number as a pair of an integer and a possibly infinite purely fractional decimal expansion:

type dec = Dec of int * int list

A sufficient condition for two numbers to be equal is that their decimal representations are the same:

let eq (Dec (e, ds)) (Dec (e', ds')) = e = e' && ds == ds'

Here, since the decimal expansions could be infinite, I use physical equality on lists. This is a stronger condition than stated above. Now, the proof for the first step:

Lemma 1 Multiplying a positive real number x by 10 shifts the decimal point in its decimal expansion one place to the right

Proof:

  10⋅x
= { lemma 0 }
  10⋅(n + ⟨∑ i : 0 > i : 10i⋅di⟩)
= { product finitely distributes over sum }
  10⋅n + 10⋅⟨∑ i : 0 > i : 10i⋅di⟩
= { product formally distributes over sum }
  10⋅n + ⟨∑ i : 0 > i : 10i+1⋅di⟩
= { substitute i := i-1 }
  10⋅n + ⟨∑ i : 1 > i : 10i⋅di-1⟩
= { lemma 0 }
  (10⋅n + d0) + ⟨∑ i : 0 > i : 10i⋅di-1⟩

Note that the third step is not strictly speaking finitist but formal: it requires taking the distributivity of product over a summation as axiomatic if induction is not accepted. This justifies the following:

let mul10 = function
| Dec (e, []     ) -> Dec (10 * e    , [])
| Dec (e, d :: ds) -> Dec (10 * e + d, ds)

The proof for the second step:

Lemma 2 Subtracting an integer k from a positive real number x only affects its integer part

Proof:

  x - k
= { lemma 0 }
  (n + ⟨∑ i : 0 > i : 10i⋅di⟩) - k
= { commutativity and associativity of sum }
  (n - k) + ⟨∑ i : 0 > i : 10i⋅di⟩

This justifies the following:

let subi (Dec (e, ds)) n =
  if e < n then failwith "subi" else
  Dec (e - n, ds)

Now the proof for the third step is purely executable and relies on physical equality of infinite lists of digits represented as circular lists:

let nines = let rec ds = 9 :: ds in Dec (0, ds)

Of course, for more general repeating expansions, equality on heads won't suffice, but this case is nicely handled by a one-liner:

let lemma = assert (eq nines (subi (mul10 nines) 9))

The purely verbal mathematical statement of this truth is that, since the first two steps operate on a finite prefix of the infinite expansion, the inifinite suffix is unchanged by the operations and hence identical to itself. In other words, the infinite summation is a purely formal object that remains unchanged from step to step.

Will this proof finally lay the "controversy" to rest, persuading even the staunchest finitist?

Edit: Thanks to id that alerted me in my confusion between structural and physical equality.