## 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.

## 2010-05-15

### 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 ≤ di < 10 such that for all iN, di = 0, and

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

and the decimal point separates the digits corresponding to 100 and 10-1, namely d0 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.