How hard is it to reduce termination to partial correctness? If you are familiar with program verification you are likely to prefer reading the Question before the Background. If you are not familiar with program verification then you may still be able to answer this question, but you are likely to prefer reading the Background first.

Background

It is often stated that checking partial correctness is undecidable. For the sake of discussion, let's pick one very particular way of making this statement precise, in the style of Floyd--Hoare. A flowgraph is a digraph with a distinguished initial node from which all nodes are reachable. A program is a flowgraph whose nodes are commands. There are three types of commands (1) assumptions assume q, (2) assertions assert q, and (3) assignments v:=e. Here q is a fol (first-order logic) formula, e is a fol term, and v is a variable.

We say that a program is partially correct when there is a way to annotate each node x with a precondition a(x) and a postcondition b(x) such that (1) the precondition of the initial node is valid, (2) {a(x)} x {b(x)} holds for all commands x, and (3) (b(x) implies a(y)) is valid for all edges from x to y. Here the Hoare triples are defined as follows:


{p} assert q {r} means that (p implies (q and r)) is valid
{p} assume q {r} means that ((p and q) implies r) is valid
{p} v:=e {r} means that ((p with e substituted for v) implies r) is valid


Here's a hand-wavy argument of why checking this partial correctness is undecidable: Once you fill in some a(x) and some b(x) you need to check if some fol formulas are valid, and that is undecidable.

A typical way to encode termination in partial correctness is to add some special assertions that essentially say "since last time I was executed, there was progress towards termination." These progress assertions must be placed such that all infinite walks on the flowgraph (that start at the initial node) contain infinitely many progress assertions. To be more specific, let's say that progress assertions always have the form assert u &lt; v, where u and v are positive integers, are preceded by the assignment u:=f, and are followed by the assignment v:=u. Here f is a variant function, u is its current value, and v is its former value. Now, since we talk about "positive integers" and we compare them, we need to ensure that a bit more than fol is available: Let's say Peano arithmetic is available. (I don't feel strongly about this choice. Feel free to disregard if convenient.) Of course, f may use any other functions and constants that are mentioned in the program. (Note that adding assumptions at the beginning of the program is equivalent to introducing non-logical axioms.)

Now, if the program with progress assertions is still partially correct, then we know that the original program terminates.

Question

Given a terminating program, it feels that coming up with variant functions for progress assertions is hard. But how hard? (I know that even with the huge background above, I still left this question sort of open-ended, or ill-defined, depending on how you want to look at it.)

To put it differently: I'm looking for a reference that formalizes the problem of reducing termination to partial correctness and then says something about its complexity. An answer that does all this would of course be welcome.
One way to answer this is to consider the computational complexity of the decision problems for the classes of partial correctness and termination queries that are known to be decidable.  Abstract interpretation using the polyhedral domain can infer the partial correctness annotations you mention in cases where the required annotations are conjunctions of linear inequalities.  Computing the abstract post-condition is exponential in the number of variables.  Then there is the overhead of finding the fixed point.  See Cousot's early papers for more on this and the Apron library if you want to play with it directly.

Finding variant functions is decidable when the variant functions are linear.  I couldn't find a complete characterization of the complexity of this, but "Termination of Linear Programs" by Tiwari has a section that discusses complexity.  See also "A Complete Method for the Synthesis of Linear Ranking Functions" by Podelski and Rybalchenko.  Also, Byron Cook has done work on leveraging abstract interpretation to help construct termination arguments.  See, for example, "Ranking Abstractions" and "Variance Analyses from Invariance Analyses".  These may give further insight into the relationship between partial correctness and termination.

Links:


http://www.csl.sri.com/users/tiwari/html/cav04.html
http://www7.in.tum.de/~rybal/papers/vmcai04-linear-ranking.pdf
http://www.dcs.qmul.ac.uk/~hyang/paper/esop08.pdf
http://research.microsoft.com/terminator/popl07a.pdf