B. Cook, Podelski, and Rybalchenko have done both practical and theoretical
work on proving that programs terminate.
They use Ramsey's Theorem (Yeah!). Jon Katz
send me their paper. After some emails with them and others I wrote an exposition.
Their papers are
here
(I used Transition Invariants (LICS 2004) and Proving Program Termination (CACM 2011), though there are others on that page that are relevant.)
My exposition is
here.
This post will briefly describe what they do. For more detail see
either their papers or my exposition.
If w is a variable in a program and A is a set then
w = input(A);
means that w gets SOME value in A, supplied by the user.
Consider the following program
w = input(N);
x = input(N);
y = input(N);
While w>0 and x>0 and y>0
control = input(1,2)
if control = 1 then
x=input(x+1,x+2,...)
y=input(y+1,y+2,...)
w=w-1
else
if control = 2 then
y=input(y+1,y+2,...)
x=x-1
A Proof that the Program terminates that does NOT use Ramsey's Theorem
How would you prove that it terminates?
One way is to (1) find a map f : NxNxN --> L where L is a well founded order,
(2) show that in each iteration of the loop
f(x,y,z) decreases, (3) show that if f(x,y,z) bottoms out then the program
has halted (perhaps earlier than this point).
For this program the key is not the function f, which will just be
f(w,x,y)=(w,x,y) but the ordering. We map to the ordering
(N x N x N, <
lex).
In every iteration either
(1) w decreases, so (w,x,y) decreases even though x and y may get
much larger, or
(2) w stays the same and x decreases, so (w,x,y) decreases even though
y may get much larger.
Hence (w,x,y) decreases. Hence, eventually, one of the components is 0,
and then the program halts.
A Proof that the Program Halts that Uses Ramsey's Theorem.
Assume, by way of contradiction, that there is a way the user could
supply initial w,x,y and also controls in every iteration, so that
the program runs forever. Let the infinite sequence of states of the
program be:
(w1,x1,y1), (w2,x2,y2), ..., (wi,xi,yi),..., (wj,xj,yj), ...
Claim: Either
w
i < w
j or x
i < x
j.
If between steps i and j we ever have control=1 then w will decrease.
If we only have control=2 then x will decrease.
We now color all (i,j) as follows: if w decreased then color it W,
if w did not decrease but x did then color it X.
By Ramsey's theorem there is a homogeneous subset.
i1 < i2 < i3 ...
If the color is W then we have
wi1 > wi2 > wi3 > ...
AH-HA- so w must eventually be 0 and the program terminates, contradiction.
Similar for if the color is X.
What to make of all of this?
-
In the first proof we only had to prove things about ONE step of
the program (YEAH!) but we had to deal with a complicated well founded
ordering (BOO!).
-
In the Second proof we had to prove things about ANY sequence of steps
of the program (BOO!) but only had to deal with a simple well founded
ordering (YEAH).
-
There are examples in my exposition and in their papers where the
Ramsey approach really does give an easier proof.
-
We didn't use the full strength of Ramsey's theorem (Henceforth RT).
Note that
the coloring is transitive: if i < j < k and
(i,j) is RED and (j,k) is RED then (i,k) is RED.
We used RT restricted to Transitive colorings.
We call this the Transitive Ramsey Theorem or TRT.
TRT for 2 colors is actually the Erdos-Szekeres theorem
(See here
for six or more proofs, article title Variations on the Monotone....)
TRT for c colors is a natural (and easy) generalization
of the Erdos-Szekeres theorem.
(I included the proof of this in my exposition for completeness, however,
if someone has a reference please leave a comment.)
-
Is RT actually stronger than TRT?
There are three ways to ask this question, and in all three
the answer is yes. See my exposition.
