Finding the Maximum Segment Sum

1. Introduction

Suppose you're given a sequence of numbers. From this sequence you can create many different subsequences of contiguous numbers — we'll call them segments. For example, if your sequence is [2; -3; 4; -1; 3], then [2; -3], [2], [-3; 4; -1], and [2; -3; 4; -1; 3] are all examples of segments. For each of these segments, you can add up all of the numbers to get the sum of the segment. So here's the question: for a given sequence, what's the greatest sum you can get among all possible segments?

In the above example, it would be 6, which is the sum of the segment [4; -1; 3]. We call this sum the maximum segment sum. How do we find it? Can we write a program to find it for any sequence? Can we prove that the program is correct?

This problem of finding the maximum segment sum is useful for illustrating several key concepts in programming, such as writing specifications, utilizing dependent types, and showing how proofs reveal programs and programs reveal proofs. It was originally brought to us by Jon Bentley through David Gries. In one of his columns on "Programming Pearls" [1], Bentley provides a brief history of the problem and discusses various solutions. Bates and Constable use it as an example in "Proofs as Programs" [2] to show how the PRL system can help a programmer with the underlying task of solving a mathematical problem. In the account given here, we'll follow the main steps of their algorithm and proof but also incorporate some new definitions now available in the Nuprl proof assistant.

2. The Algorithm

Before we write a detailed specification and formal proof, let's first think informally about how we might find the maximum segment sum of a sequence of numbers. We'll use an integer list as our sequence. Consider the empty list first. Since there's nothing in the list, the maximum segment sum is just 0. We'll call this m₀. What about a single-element list, [z], where z is any integer? This is also easy: the maximum segment sum is just z, i.e. m₁ = z.

Now let's add another integer, y, to the front of the list to get [y; z]. The segment that has the greatest sum will either include y or it won't. If it doesn't include y, then the maximum segment sum is the same as it was previously: m₂ = m₁ = z. If it includes y, then the segment is what we call an initial segment, a segment which starts at the first element of the list. We'll label the sum of this initial segment as i₂. Putting the two cases together, we can say that m₂ = max(m₁, i₂).

Let's take a closer look at the initial segments. The maximum initial segment sum is the greatest sum you can get among all possible initial segments. Analogous to m above, i₀ = 0 for the empty list and i₁ = z for the single-element list [z]. When we add another number to the front of the list to get [y; z], however, all initial segments must include this new front number y. The new maximum might just be y, or it could be the result of y added to the previous maximum initial segment sum. Putting these two cases together, i₂ = max(y, y + i₁).

Substituting this result into our observation about m₂, we can say that m₂ = max(m₁, max(y, y + i₁)). This pattern continues as we keep adding integers to the front of the list: for [x; y; z], m₃ = max(m₂, max(x, x + i₂)). Thus we can calculate the maximum segment sum based on the value at the head of the list and the result from the tail, which means we have found a recursive algorithm as a solution. We can use this algorithm to help us write a formal proof that the maximum segment sum exists, since recursion can often be translated into a proof by induction, and vice versa.

Since our method involves both the maximum segment sum and the maximum initial segment sum, we'll actually prove that both values exist, in the form of a pair 〈m, i 〉. In Nuprl, we can extract a program from a constructive existence proof. In fact, once we finish the formal proof, we can extract the following recursive program which uses exactly the method just described. Note that in Nuprl the empty list is represented as [], while a nonempty list is represented as a pair 〈h, t 〉 where h is the head of the list and t is the tail.

3. Specification

We use an integer list, ℤ List, as our sequence. As mentioned above, the empty list in Nuprl is represented as [], while a nonempty list is represented as a pair 〈h, t 〉 where h is the head of the list and t is the tail. A nonempty list can also be represented using the "cons" operator, displayed as [h / t].

What exactly do we mean by the maximum segment sum? That is, for m to be the maximum segment sum of an integer list L, what conditions must m satisfy? Intuitively, we know that m must be the sum of a segment of L, and m must be greater than or equal to the sum of any other segment of L. Here is the full specification:

We arrive at this definition after careful consideration of the possible segments of L that could arise. In particular, notice that if the empty list is considered a segment, then the maximum segment sum of a list of all negative integers would always be zero, since the sum of [] is zero whereas all other segments would have a negative sum. Since this is not our intention, we make the decision not to include the empty list as a valid segment in our specification.

We define seg_sum(p;q;L) to be the sum of the segment of L starting at index p and ending at index q. To avoid [] as a possible segment, we specify that 0 ≤ p ≤ q < ||L||, where ||L|| is the length of L. Lists in Nuprl begin at index 0, so the last element of the list is at index (||L|| - 1). We can state these restrictions in Nuprl since Nuprl has dependent types. The type for p is dependent on L, since it must be the case that 0 ≤ p < ||L||. Then the type for q is dependent on both the length of L and the value of p, since p ≤ q < ||L||. These type declarations are displayed in Nuprl as p:ℕ||L|| and q:{p..||L||-}.

What happens if L itself is the empty list? The maximum segment sum m should be 0, but because of our restrictions on the indices, we can't define a valid segment for m — there are no p, q such that 0 ≤ p ≤ q < ||L|| when L = [], since ||L|| = 0. Therefore we split the definition into two cases as shown: either L = [] and m = 0, or L ≠ [] and m must satisfy the conditions listed in order to be the maximum segment sum of L.

We create an analogous definition for the maximum initial segment sum, where initseg_sum(r;L) is the sum of the initial segment of the list L ending at index r. The following conditions must be satisfied for i to be the maximum initial segment sum of L:

As described in Section 2, we use the maximum initial segment sum in our method for finding the maximum segment sum. Therefore we will need to prove that both values exist. More specifically, our goal is to prove that for a given list L, there exists a pair 〈m, i 〉 such that m is the maximum segment sum of L and i is the maximum initial segment sum of L:

4. Proof by List Induction - Overview

List induction works well for this proof, since the algorithm shown in Section 2 involves recursion on the tail of the list. For the proof, we assume that the theorem holds for the tail v of a list and then use this assumption (i.e. the induction hypothesis) to show that the theorem also holds for the list [u / v]. But first we must prove the base case, where we assume that the list is empty.

Base Case

The base case follows directly from Definitions 1 and 2. When the list is empty, the maximum segment sum and maximum initial segment sum are both 0, so the pair we are looking for is 〈0, 0〉. Notice that this matches the first "if" case of the algorithm in Section 2.

Induction

For the induction step, we must prove that the theorem holds for a nonempty list [u / v], assuming that it holds for the tail v:

Case v = []

First we consider the case when the tail v is empty, so that [u / v] = [u]. Both the maximum segment sum and the maximum initial segment sum of a single-element list [x] are just x, proven separately as Lemma 1. So the pair we are looking for is 〈u, u 〉. Notice that this matches the second "if" case of the algorithm in Section 2.

Case v ≠ []

For the case when the tail is nonempty, Nuprl declares this explicitly by replacing v with the list [u1 / v] (note that in the algorithm from Section 2, this is labeled [u1 / v1], since v already appears as a variable). So now the induction hypothesis is that the theorem holds for the list [u1 / v] and we must prove that it also holds for [u; u1 / v]. By the induction hypothesis, there exists a pair of integers 〈p1, p2 〉 such that p1 is the maximum segment sum of [u1 / v] and p2 is the maximum initial segment sum of [u1 / v]. As we discovered in Section 2, we can use these values together with the head of the list, u, to find the result for [u; u1 / v]: the maximum segment sum is max(p1, max(u, u + p2)), where max(u, u + p2) is the maximum initial segment sum.

The rest of the proof is devoted to proving this claim that max(p1, max(u, u + p2)) is the maximum segment sum and max(u, u + p2) is the maximum initial segment sum. We show more detail in Section 5 about how this is done.

5. Proof Detail

To prove that max(p1, max(u, u + p2)) is the maximum segment sum of the list [u; u1 / v], we first prove that max(u, u + p2) is the maximum initial segment sum and then use this result to prove the maximum segment sum. In other words, we prove I ∧ (I ⇒ M) in order to prove the goal M ∧ I, where M is the claim about the maximum segment sum and I is the claim about the maximum initial segment sum. In the proof we use the following lemmas about segment sums and integer maximums:

Maximum Initial Segment Sum

We start by first proving the claim that max(u, u + p2) is the maximum initial segment sum of the list [u; u1 / v]. We unfold the definition of max_initseg_sum as follows:

Since [u; u1 / v] is obviously nonempty, we prove the right side of the "or" statement. When we break apart this right side, we have three separate statements to prove. The first is trivial because the list is nonempty. The next two require some explanation.

Proof: ∀r:ℕ||[u; u1 / v]||. (imax(u;u + p2) ≥ initseg_sum(r;[u; u1 / v]))

Here we have to prove that for any r in the range of indices of the list, max(u, u + p2) is greater than or equal to the sum of the initial segment ending at index r. Consider the case when r = 0. Then initseg_sum(r;[u; u1 / v]) = initseg_sum(0;[u; u1 / v]) = u by Lemma 2. Since max(u, u + p2) ≥ u by Lemma 6, the claim holds when r = 0.

When r ≠ 0, we can apply Lemma 4 to redefine the sum by shifting the index as follows:

The induction hypothesis states that p2 is the maximum initial segment sum of the list [u1 / v]. This means that p2 is greater than or equal to the sum of any initial segment of [u1 / v], including the one ending at index (r - 1). Together with Lemma 7, we can conclude the following: imax(u;u + p2) ≥ (u + p2) ≥ (u + initseg_sum(r - 1;[u1 / v])) = initseg_sum(r;[u; u1 / v])).

Proof: ∃c:ℕ||[u; u1 / v]||. (imax(u;u + p2) = initseg_sum(c;[u; u1 / v])))

Now we need to prove that there exists an initial segment with a sum equal to max(u, u + p2). Consider the case when u ≤ u + p2, so that max(u, u + p2) = (u + p2). By the induction hypothesis, p2 is the maximum initial segment sum of the list [u1 / v], and so there exists an integer c such that p2 is the sum of the initial segment of [u1 / v] ending at index c. Then (u + p2) = (u + initseg_sum(c;[u1 / v]) = initseg_sum(c + 1;[u; u1 / v]). We use Lemma 4 again to prove the second equality. So when u ≤ u + p2, the initial segment of [u; u1 / v] ending at index (c + 1) has a sum equal to max(u, u + p2).

The case of u > u + p2 has a simpler proof. When u > u + p2, max(u, u + p2) = u, and the initial segment of [u; u1 / v] ending at index 0 has a sum equal to u by Lemma 2.

Maximum Segment Sum

Next we prove that max(p1, max(u, u + p2)) is the maximum segment sum of the list [u; u1 / v], using the fact that max(u, u + p2) is the maximum initial segment sum. We begin by unfolding the definition of max_seg_sum as follows:

Since [u; u1 / v] is obviously nonempty, we prove the right side of the "or" statement. When we break apart this right side, we again have three separate statements to prove. As before, the first is trivial because the list is nonempty, but the next two require some explanation.

Proof: ∀p:ℕ||[u; u1 / v]||. ∀q:{p..||[u; u1 / v]||-}. (imax(p1;imax(u;u + p2)) ≥ seg_sum(p;q;[u; u1 / v]))

For this part we must prove that max(p1, max(u, u + p2)) is greater than or equal to the sum of the segment from index p to index q for any p, q in the interval 0 ≤ p ≤ q < ||[u; u1 / v]||. Consider the case when p = 0, so that we are looking at the initial segments of [u; u1 / v]. By Lemma 3, seg_sum(0;q;[u; u1 / v]) = initseg_sum(q;[u; u1 / v]). Since we've already proven that max(u, u + p2) is the maximum initial segment sum, we know that max(u, u + p2) is greater than or equal to the sum of any initial segment of [u; u1 / v], including the one ending at index q. Together with Lemma 7, we conclude that imax(p1;imax(u;u + p2)) ≥ imax(u;u + p2) ≥ initseg_sum(q;[u; u1 / v]) = seg_sum(0;q;[u; u1 / v]). Thus imax(p1;imax(u;u + p2)) ≥ seg_sum(p;q;[u; u1 / v]) for p = 0.

When p ≠ 0, we can use Lemma 5 to shift the indices of the segment sum as follows: seg_sum(p;q;[u; u1 / v]) =
seg_sum(p - 1;q - 1;tl([u; u1 / v])) = seg_sum(p - 1;q - 1;[u1 / v]). The induction hypothesis states that p1 is the maximum segment sum of the list [u1 / v], which means that p1 is greater than or equal to the sum of any segment of [u1 / v], including the one that starts at index (p - 1) and ends at index (q - 1). With Lemma 6 we can therefore conclude that imax(p1;imax(u;u + p2)) ≥ p1 ≥ seg_sum(p - 1;q - 1;[u1 / v]) = seg_sum(p;q;[u; u1 / v]).

Proof: ∃a:ℕ||[u; u1 / v]||. ∃b:{a..||[u; u1 / v]||-}. (imax(p1;imax(u;u + p2)) = seg_sum(a;b;[u; u1 / v]))

In this part we need to show that there exists a segment of [u; u1 / v] which has a sum equal to max(p1, max(u, u + p2)). Consider the case when p1 ≤ max(u, u + p2), so that the outer maximum function evaluates to max(u, u + p2). We've already proven that max(u, u + p2) is the maximum initial segment sum of [u; u1 / v], which means that there exists a number c such that max(u, u + p2) is the sum of the initial segment ending at index c. Thus the segment starting at index 0 and ending at index c has a sum equal to max(p1, max(u, u + p2)) when p1 ≤ max(u, u + p2).

If p1 > max(u, u + p2), then the outer maximum function evaluates to p1. By the induction hypothesis, p1 is the maximum segment sum of the list [u1 / v], and there exist numbers a, b such that p1 is the sum of the segment of [u1 / v] starting at index a and ending at index b. Using Lemma 5 again, we can shift these indices to restate p1 as the sum of a segment of [u; u1 / v]: p1 = seg_sum(a;b;[u1 / v]) = seg_sum(a + 1;b + 1; [u; u1 / v]). Thus the segment starting at index (a + 1) and ending at index (b + 1) has a sum equal to max(p1, max(u, u + p2)) when p1 > max(u, u + p2).

This finishes the proof.

6. Projections from Nuprl

• View the complete proof as a PDF


• Step through the proof in the frame:

7. References

1. Jon Bentley. Programming pearls: algorithm design techniques. In Communications of the ACM, Vol. 27, No. 9, September 1984. Pages 865-871.


2. Joseph L. Bates and Robert L. Constable. Proofs as Programs. In ACM Transactions on Programming Languages and Systems, Vol. 7, No. 1, January 1985. Pages 113-136.