CMP.13:5 - Archetypal Grounding

CMP.13:5.1 - A graph summary invents a path

The original graph has vertices a,b,c,d, edges a->b and c->d, and initial vertex a. The question is whether d is reachable. Merge b and c into abstract vertex q, while keeping a and d separate. An abstract edge exists when any original edge connects the corresponding classes.

The abstract graph has a->q and q->d. Searching it returns the path a,q,d. Each edge has an original witness, yet the first edge arrives at b and the second leaves c.

Reconstruction gives X0={a}, X1={b} and X2=empty, since b has no successor. Split q into {b} and {c}. The recomputed reachable set is {a,b}, so d is unreachable. The useful result is both the answer and the reason the original summary could not establish it.

Changed condition: add edge b->c. The abstract path a,q,q,d now reconstructs to a,b,c,d; this is a real path. The shorter path a,q,d still has no consecutive realization, but its failure no longer excludes reachability. The transition change requires the affected search and reconstruction to be updated.

CMP.13:5.2 - Obtain a loop property without enumerating its iterations

Consider unbounded integers, positive integer N, and:

x = 0
while x < N:
    x = x + 1

At the loop head, a set X of possible values is transformed by F(X)={0} ∪ {x+1: x∈X and x<N}. An interval hull supplies an abstract transformer. Starting at [0,0] produces [0,1], [0,2] and so on until [0,N]; this takes a number of expansions proportional to N even though N can be written with logarithmically many bits.

Widen the increasing upper endpoint of [0,0] and [0,1] to obtain [0,+infinity]. It contains the initial value and is closed under the guarded update. It already establishes that x is never negative.

Suppose the receiving question instead asks for the value on exit. Apply the guard to [0,+infinity]: the integer inputs admitted by x<N are [0,N-1]; adding one and joining the initial value gives [0,N]. This smaller interval is itself closed under F, and contains 0. The exit condition x>=N then leaves [N,N]. Therefore every terminating execution exits with x=N.

For a termination conclusion, add a different argument: while the guard holds, the nonnegative integer N-x decreases by one, and the arithmetic is unbounded. This proves termination from 0 for the stated positive N. It explains why the exit value is obtained, rather than merely describing it if obtained.

Changed condition: replace the update by x=x+2, retaining N=5. The guarded interval calculation now gives [0,6]; exit intersection gives [5,6]. If that bound is sufficient, stop. If the final value is needed, retain the invariant that x is even as well. The exit result becomes {6}. The old answer 5 was tied to the former update.

CMP.13:5.3 - Independent ranges lose the determining relation

Let input b be either 0 or 1. Execute x=b; y=b, then test whether x!=y. Independent intervals give x∈[0,1] and y∈[0,1]. Their product contains (0,1), so it cannot exclude the unequal branch.

Recover the construction: both assignments use the same b. Retain x=y, or keep the two input cases separate. Each choice excludes the unequal branch. The shared equality is the needed distinction; refining both independent endpoint ranges cannot recover it.

If the second assignment becomes y=1-b, both inputs take the unequal branch. A retained relation must be derived again from the changed operation. The earlier equality is an invalid assumption in the new computation.