MATH.11:5.2 - Derive an accumulated sum from an update

A construction starts at (n,s)=(0,0) and repeatedly applies:

(n,s) → (n+1,s+n+1).

The question is what s will be when n has reached a chosen nonnegative integer. The new term added to s depends on n, so try I(n,s)=a*s+b*n^2+c*n+d.

Substitution gives:

I(n+1,s+n+1)-I(n,s)=(a+2*b)*n+(a+b+c).

Set a+2*b=0 and a+b+c=0. Choose a=2, b=-1, c=-1 and d=0. The resulting invariant is I(n,s)=2*s-n^2-n. It starts at zero, so every state reached by the update satisfies:

2*s=n^2+n, hence s=n*(n+1)/2.

After three steps, (3,6) satisfies it. The proposed state (3,7) has invariant value 2 and cannot result from these updates.

The same relation can be used with a different start. Starting at (2,10) gives invariant value 14, so later states satisfy 2*s-n^2-n=14. One step produces (3,13), which satisfies that changed equation. The preservation proof is unchanged.

Now change the update to (n,s) → (n+1,s+2*n+1). Substitution into the old invariant gives change 2*n, so the old formula fails in general. Reusing the same candidate family gives equations 2*a+2*b=0 and a+b+c=0. Choose a=1, b=-1, c=0: the new invariant is s-n^2. From (0,0), it gives s=n^2.

These constructions use integer arithmetic without overflow. They also use the update as a simultaneous substitution: the expression for the new s contains the old n. An implementation that increments n before evaluating that expression would need a different calculation.