Proving programs terminate using well orderings, Ramsey Theory, and Matrices
Combinatorics
2014-11-04 v3 Logic in Computer Science
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.
Cite
@article{arxiv.1108.3347,
title = {Proving programs terminate using well orderings, Ramsey Theory, and Matrices},
author = {William Gasarch},
journal= {arXiv preprint arXiv:1108.3347},
year = {2014}
}
Comments
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