We study the proof of a recent and relevant result about termination of programs, the Termination Theorem by Podelski and Rybalchenko [9]. We prove that in a special case, the only case which is used in applications, all programs proved to be terminating may be described by some primitive recursive map. Fix any transition relation R over the set S of possible states of a program P . Assume In ⊆ S is the set of possible initial states of P , and that Acc is the set of accessible states of P , if we start from some state in In and we use the relation R finitely many times. The Termination Theorem by Podelski and Rybalchenko [9] may be stated as follows. The transition relation R is terminating from any initial state if and only if the transitive closure R+ of R, restricted to the set Acc of accessible states, is included in some finite union of well-founded relations. The authors formulate the Termination Theorem by introducing the concept of “disjunctively well-founded transition invariant”. A disjunctively wellfounded transition invariant is any binary relation T which is the union of a family T1, . . . , Tn of well-founded relations, and which includes the restriction to Acc of R+. The original statement of the Termination Theorem is: “R is terminating from any initial state if and only if R has some disjunctively well-founded transition invariant T ”. By building over this result the same authors and Byron Cook designed an algorithm they called Terminator [5], checking a sufficient condition for termination for a while-if program P in a simplified programming language. The Terminator algorithm takes P and looks for a disjunctively well-founded transition invariant T = T1 ∪ . . . ∪ Tn for P , with T1, . . . , Tn well-founded relations of height ω. The extra feature “of height ω” is found in the algorithm but not in the Theorem. If the Terminator algorithm finds T1, . . . , Tn as above, it deduces the termination for the program P using the Termination Theorem. This particular application of the Termination Theorem raises an interesting question: what is the status of a transition relation R having a disjunctively well-founded transition invariant T = T1 ∪ . . . ∪ Tnwhere each Ti has height ω? An answer to this question can lead to a characterization of the set of while-if programs which the termination algorithm can prove to be terminating.
2
A characterization of the Termination Theorem in the case of invariants of height ω Our first result is the following. The Termination Theorem may derive that a transition relation R is terminating using n relations T1, . . . , Tn of height ω if and only if R has height ≤ ωn. Besides, in the case T1, . . . , Tn are primitive recursive and R itself is (the graph of) the restriction of some primitive recursive map to some primitive recursive subset, we may say more. In this case, indeed, the final state of the program P is computable by some primitive recursive map in the initial state.
As a corollary we derive that the set of functions, having at least one
implementation in Podelski-Rybalchenko while-if language with a well-founded
disjunctively transition invariant where each relation has height ω, is exactly the
set of primitive recursive functions. This is an ongoing work: a preliminary draft
may be found in [
Our approach is based over the analysis a new intuitionistic proof of the
Termination Theorem [
First of all, we introduce the notion of H-well-foundation. Let T be any binary relation on some set I. We say that a sequence s is T -homogeneous if s ∈ H(T ), where H(T ) is defined as follows.
Let T be a binary relation on some set I. H(T ) is the set of the T -decreasing transitive finite sequences on I: hx1, . . . , xni ∈ H(T ) ⇐⇒ ∀i, j ∈ [1, n].i < j =⇒ xj T xi.
T is H-well-founded if H(T ) is well-founded by one-step extension. If T is well-founded that T is H-well-founded, but H-well-foundation is much weaker than well-foundation. The notion of H-closure is new, therefore we provide some examples. The relation T ≡ (6=) over {0, 1} is not well-founded because we have the infinite chain 0 6= 1 6= 0 6= 1 . . .. Any sequence s ∈ H(T ), by definition unfolding, has any two elements in relation 6=, therefore has pairwise distinct elements, hence has length ≤ 2. Thus, H(T ) has height 2 w.r.t. the one-step extension relation, therefore H(T ) is well-founded, and T is H-well-founded. Another example (for which we skip the proof): a relation T over a finite set is well-founded if and only if there are no T -cycles, that is, there are no x0, . . . , xn ∈ I such that x0T x1T . . . T xn = x0. A relation T over a finite set is H-well-founded if and only if there are no T -loops, that is, there is no x ∈ I such that xT x. This second condition is much weaker that the first one, a loop is a cycle but a cycle in general is not a loop.
The H-closure Theorem says that if R1, . . . , Rk are H-well-founded then
(R1 ∪ · · · ∪ Rk) is also H-well-founded. H-closure has an intuitionistic proof,
and, as we said, intuitionistically derives the Termination Theorem. In order to
characterize the Termination Theorem in the case of height ω relations, we first
strengthen H-closure as follows. If each Ri has ordinal height less or equal than
αi, then H(R1 ∪ · · · ∪ Rk) has ordinal height less or equal than 2α1⊕···⊕αk , where
⊕ is the natural sum of ordinals, defined as the smallest binary function which is
increasing in both arguments w.r.t. the pointwise ordering [
Eventually, we embed the ordering of H(R1 ∪ · · · ∪ Rk) into the ordering over [0, ωk], and we use the characterization for the decreasing sequences over [0, ωk] in order to characterize the sequences of transitions for a given program P .
After this proof was done, we were informed that Delhomm´e [
We proved the following characterization of the Termination Theorem. Assume we have a program P whose transition relation R is the graph of a partial recursive map restricted to a primitive recursive domain. Assume we have a disjunctively well-founded transition invariant T = T1 ∪ . . . . . . Tn for R, with T1, . . . , Tn primitive recursive and of height ω. Then we may compute the number of steps of R and the final state by some primitive recursive function in the initial state.
We conjecture that the same result holds for the Terminator Algorithm based on the Termination Theorem: a function has at least one implementation in Podelski-Rybalchenko language which the Terminator Algorithm may catch terminating if and only if the function is primitive recursive. One of the authors is working on a proof of it. The result is not self-evident because there is much more in the Terminator algorithm than just the Termination Theorem.
If compared to the characterization of Termination Theorem based on Dickson Lemma, our characterization has the advantage of being based over the original proof of the Theorem. For this reason, we hope in a future work to be able characterize the Termination Theorem in general, in the case of well-founded relations of any ordinal height.