Proof of correctness for optimal solution for sorted two-sum

Question

I have been solving the problem of two sum with a sorted array, which can described as follows:

Given a sorted array arr sorted in non-decreasing order and a target target, find whether two indices i and j exist such that arr[i] + arr[j] == target. The solution must use constant extra space.

The optimal solution to this problem involves using two pointers, left and right set to 0 and len(arr) - 1 respectively for either end of the array. While left < right, the sum of the elements at each respective pointer is checked. If said sum is less than the target sum, the left pointer is incremented. If the sum is greater than the target, the right pointer is decremented. If the sum equals the target, we return true. At the end of the function, we return false otherwise since no such pair was found.

What I'm struggling with is to understand why this is correct. I see that decrementing right when the sum is too big will reduce the sum, but I don't see why decrementing left would also not decrease the sum. Likewise, if the sum is too small, incrementing right would increase the sum just as much as incrementing right. I tried to construct a proof by contradiction for the latter case:

Incomplete proof:

Given two indices $l$ and $r$ in an array $A$ sorted in non-decreasing order and a target sum $t$, where $l < r$ and $A[l] + A[r] < t$, let us assume that there exists some index $r'$ such that $r' > r$ and $A[l] + A[r'] == t$.

Then, since $A[l] + A[r] < t$ and $A[l] + A[r'] == t$, we can state that $A[l] + A[r] < A[l] + A[r']$. From this, it follows that $A[r] < A[r']$

It's at this point I'm not sure where to go. The goal is to disprove the existence of some $r'$, because that would show that incrementing the right pointer is not the correct way to reach the target sum. I'd imagine that I could use a similar proof for decrementing the left pointer when the sum is too high as well. What would be the best way to continue this proof/fix any errors in my assumptions?

Answer 1

Indeed as you said if the two sum is too small than the target, then obviously you can either increase the right pointer or increase the left pointer. But since the base case of this algorithm is from both end of the array, the algo can only move both pointers inward during each loop to ensure its halting along with its loop invariant.

Here the loop invariant maintains that all pairs in the subarray between left and right pointers are still candidates for the target sum to guarantee no candidate pairs are missed. So in your attempted incomplete proof though you maintains the correctness of the loop invariant, but you cannot prove the loop will halt.

Incidentally you can also start from middle and keep the loop invariant outward only, it's an equivalent algo but needs extra beginning pointers' position decision and final array out-of-bound checks at both ends.

Answer 2

"Bad states" (pairs of left and right) from which the algorithm has no hope of finding the solution do exist. You are trying to prove that they don't exist, which is a doomed initiative. If A[i] + A[j] == t, then you can easily construct an example of such a bad state as left=i and right=i+1 (also assuming i+1 < j).

Instead, consider the idea that those bad states cannot be reached from the actual starting state of the algorithm.

Answer 3

Let us first write the algorithm (Python code) in a formal way:

def solve(arr, target):
  left = 0
  right = len(arr) - 1
  while left < right:
    sum = arr[left] + arr[right]
    if sum == target:
      return (left,right)
    elif sum < target:
      left += 1
    else:
      right -= 1
  return None

We will establish a loop invariant: if there is a solution, it always exists in the subarray arr[left:right].

The first case is easy. Now, if the sum is less than the target, then the sum has to be increased. Note that arr[right] is the highest element in it, so the only way to increase the sum is to forward the left pointer. A similar argument holds for the case when the sum is greater than the target, and the right pointer moves backward.

Following this loop invariant, we either find a suitable pair of indices whose values add up to the target, else we exhaust the array and thus no solution exists.