Monday, August 15, 2011

An application of Ramsey Theory to Proving Programs Terminate

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 wi < wj or xi < xj. 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?
  1. 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!).
  2. 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).
  3. There are examples in my exposition and in their papers where the Ramsey approach really does give an easier proof.
  4. 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.)
  5. 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.

14 comments:

  1. What if the user enters "3" every time?

    ReplyDelete
  2. Typo- should have been control=input(1,2).
    I have fixed it.
    Thank you for the correction.

    ReplyDelete
  3. A typo: A. Rybalachenko is missing in your reference [1] (I talk about the pdf)

    ReplyDelete
  4. What role does the variable y play in this argument? (Is it a red herring?)

    ReplyDelete
  5. garethrees.org- Yes, y is a red herring- the example
    is supposed to be ... an example to make the point
    To see more real examples (hmmm- not sure its THAT real)
    see their papers or my exposition.

    ReplyDelete
  6. Re: garethrees: the variable y plays one important role: it rules out the most obvious proof attempt, which would be to show the sum x+w decreases every time. Pesky y, messing that all up!

    ReplyDelete
  7. Actually, ignore that last comment. Of course it didn't make any sense -_-

    ReplyDelete
  8. There is also a set-theoretic way of looking at it: Consider the lexicographic order for (w,x,y). It is a well-ordering, and in every iteration of the program you get a triple lower in the order. Hence the program halts on account of having no infinite decreasing sequence over a well ordered set. This would work also for more variables (and so would the Ramsey proof).

    ReplyDelete
  9. Re: twitter post on instant fame vs. long-term success.

    However, in academia if you get instant fame for something, then you get tenure. So it's quite different from the opera world, where if you are "over the hill" you could be unemployed.

    ReplyDelete
  10. The claim "either wi < wj or xi < xj" also yields termination by Dickson's Lemma.

    ReplyDelete
  11. sorry for being completely offtopic,
    I have a general question about NP reductions, is there a book or another collection out there covering let us say the 300 most important reductions ever published. According to wikipedia there are more than 3000 known NP problems, so a complete survey is quite infeasible, but many of the 3000 poblems may be just specialised versions of standard problems. What I'd really like to have atm, is a collection of reductions from Karps 21 problems to each other (where feasible) or at least to 3-SAT, CLIQUE, DHC/HC/TSP, which I consider the most basic NP problems. Most text books just do a few reductions in form of a chain ususally ending with 3-SAT or CLIQUE, which doesn't give you a hint how to do another reduction. Of course you could just "insert" one reduction into another, but this usually leads to hopelessly bloated situations and almost always there are different and/or much more efficient ways, hence my question.

    ReplyDelete
  12. For a famous example where you really need the Infinite Ramsey Theorem consider the Paris Harrington Theorem. There is a program which halts on every integer (coded triple of integers) iff the strengthed Ramsey theorem holds for that triple. This is not provable in PA but is deducible from the Infinite Ramsey Theorem.

    So sometimes you really really do need Ramsey theory or at least principles of infinitary reasoning.


    ---

    It's much easier to go from the Infinite Ramsey Theorem to the Finite Ramsey Theorem using Koneig's Lemma. As standard we number the vertices with non-negative integers and fix a bijection taking the set {x,y} to a non-negative integer.

    Fix k and let T be the set of finite sequences of integers from 0..c-1 viewed as colorings of the associated edges that don't witness the existence of a homogeneous set of size k. T is a finitely branching tree and by the infinite ramsey theorem it can't have an infinite path so by Koneig's Lemma T is finite and thus has a longest string in it. That length is at least RT(k,c).

    Of course things get funny if you do reverse math and don't assume WWKL0

    ---

    ReplyDelete
  13. Ohh and I also should add that there any true \Pi_2 statement will be a useful way to prove some program is total (the one that takes as input the \forall variable and then terminates on verifying the existential). So it's not clear what makes Ramsey theory special here.

    ReplyDelete