Proving programs terminate using well orderings, Ramsey Theory, and Matrices
arXiv:1108.3347
Abstract
Many programs allow the user to input data several times during its execution. If the program runs forever the user may input data infinitely often. A program terminates if it terminates no matter what the user does. We discuss various ways to prove that program terminates. The proofs use well orderings, Ramsey Theory, and Matrices. These techniques are used by real program checkers.
While this is classified under Combinatorics (to tell combinatorists that someone is using their stuff) it should also be of interest to Logicians and Computer Scientists