CMP.2:4 - Solution
State the answer → propose smaller questions → derive the join → strengthen what must be returned → establish return → compare the work.
CMP.2:4.1 - Fix the question and the available operations
Describe an input x, the information available about it, and what a returned answer must allow its recipient to do. Asking for an optimum value, one attaining object, or every attaining object gives different result requirements. State the empty and degenerate cases when they belong to the input family.
List the operations that can actually be performed on this input: inspect a constructor, split an interval, compare keys, compute a remainder, test a condition, or call a supplied procedure. A proposed step such as “choose the correct partition” remains a construction task until the partition can be obtained.
For example, maximum segment sum on a sequence of integers asks for a contiguous nonempty segment with largest sum. Returning its sum answers a value query; locating the segment also requires endpoints. Permitting the empty segment changes the base case and the answer on an all-negative input.
CMP.2:4.2 - Choose a decomposition by asking how answers would join
Take a representative input and suppose that selected smaller questions have been answered correctly. Try to construct the answer for this input from those returned values. This local design question avoids having to unfold the entire recursion while inventing it.
Useful proposals include removing one element, splitting into balanced parts, following the constructors of a structured input, or transforming the input while decreasing another measure. The last case includes Euclid’s replacement of a pair by a divisor and remainder. Input size need not decrease in every component.
For each proposal, account for every form a valid answer can take. If a sequence is split into left and right parts, an optimal contiguous segment lies wholly on one side or crosses the boundary. The crossing case shows what the two recursive answers must supply.
Keep the proposal that makes the join both justified and obtainable. If the only available join searches the original problem again, change the subproblem question, retain more information, or try another decomposition.
CMP.2:4.3 - Strengthen the returned result when the join needs more
Write the join using named values. Each value must come from the input, a smaller answer or an available local operation. A missing value identifies a specific revision of the subproblem, rather than a reason to discard recursion as a whole.
For maximum segment sum, the best segment on each side is insufficient: a crossing segment uses a suffix of the left side and a prefix of the right. Let each nonempty part return four quantities:
T: the sum of the whole part;P: the largest sum of a nonempty prefix;S: the largest sum of a nonempty suffix;B: the largest sum of a nonempty contiguous segment.
For a left summary L and right summary R, construct:
T = L.T + R.T
P = max(L.P, L.T + R.P)
S = max(R.S, R.T + L.S)
B = max(L.B, R.B, L.S + R.P)
The alternatives in each maximum come from the possible locations of the corresponding segment. To return an actual segment, carry the endpoints attaining each selected prefix, suffix and best segment. Choose a consistent rule for ties when only one witness is wanted.
This is the algorithmic use of strengthening an inductive result in MATH.4. The additional design decision is what summary enables an affordable join for the chosen problem decomposition. Further questions may require a different summary.
CMP.2:4.4 - Supply base cases and a decreasing measure
Give a direct result for each case on which recursion stops. Then show that every recursive call reaches such a case after finitely many steps. A nonnegative integer that strictly decreases is often enough. A finite input constructor or a well-founded ordering can supply the same argument when one numerical size is awkward.
For the segment procedure, a singleton v returns (v,v,v,v). Split every longer interval into two nonempty shorter intervals. Its length decreases along every call path. This also explains why an empty interval needs its own convention or must be excluded before calling the procedure.
For nonnegative integers with b>0, Euclid’s call (a,b) → (b,a mod b) decreases the second component because 0≤a mod b<b. The first component may increase relative to its old value; it is the selected measure that must decrease. At b=0, return a, with the intended convention for (0,0) fixed separately.
When a termination checker fails, inspect which decrease is absent from its account. A supplied difference, lexicographic measure or invariant may express the progress already present in the procedure. If progress is genuinely missing, repair the procedure or weaken its claimed result. A small successful run alone does not establish return on every allowed input.
CMP.2:4.5 - Establish the result and expose its computational cost
Use the base and smaller-call assumptions to establish the returned property. Recombination must work for every smaller answer allowed by its specification, including the selected tie behavior. When deriving a program from an existing proof, MATH.12 recovers the operations hidden in that proof.
Count the subcalls and local work. A recurrence for mathematical values and a recurrence for computational cost answer different questions. For balanced segment splitting with interval views, constant-cost arithmetic and the four-value join, the work satisfies W(n)=W(floor(n/2))+W(ceil(n/2))+O(1), giving O(n) operations. Sequential depth-first evaluation retains O(log n) summaries on its call stack. Copying each subarray instead adds work at each level; growing integer values also change the cost per addition.
If equal subproblems recur, CMP.3 can identify and share them. If the decomposition generates alternatives that can be ruled out, CMP.4 can construct those exclusions. If representation dominates the cost, compare the access and update operations before replacing the mathematical construction.
CMP.2:4.6 - Use the result and revisit the assumption that changed
Run a small case through the complete procedure, including the use of its returned answer. Change one condition that stresses the construction: empty input, a boundary case, a different output request or a resource limit. Follow the affected base, join and progress arguments.
The result may be a working procedure, an unaffordable but informative construction, or a located missing operation. Use that difference to choose the next algorithmic move. Formal proof or additional testing is chosen for the uncertainty that matters to the receiving use.