Proving termination of programs having transition invariants of height ω Stefano Berardi1 , Paulo Oliva2 , and Silvia Steila1 1 Università degli studi di Torino 2 Queen Mary University of London Abstract. We study the proof of a recent and relevant result about termination of programs, the Termination Theorem by Podelski and Ry- balchenko [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. 1 Introducing the Termination Theorem 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 con- cept of “disjunctively well-founded transition invariant”. A disjunctively well- founded 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 termi- nating 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 ter- mination for a while-if program P in a simplified programming language. The Terminator algorithm takes P and looks for a disjunctively well-founded transi- tion 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 ∪ . . . ∪ Tn where 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. 237 S.Berardi et al. Proving termination of programs having transition invariants of height ω 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 im- plementation in Podelski-Rybalchenko while-if language with a well-founded dis- junctively 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 [1]. An independent proof of the same result, again in the form of preliminary draft, may be found in [8]. The authors follow a completely dif- ferent approach, they use a miniaturization of the Dickson Lemma to prove the Termination Theorem. 3 A sketch of our proof Our approach is based over the analysis a new intuitionistic proof of the Ter- mination Theorem [2] (another intuitionistic proof already existed, by Thierry Coquand [6]). The original proof of the Termination Theorem requires classical logic and Ramsey’s Theorem. In order to intuitionistically prove the Termina- tion Theorem we introduced a kind of contrapositive of Ramsey Theorem, the H-closure Theorem [2], which we are going to explain. 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 , . . . , xn i ∈ 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 ∈ 238 S.Berardi et al. Proving termination of programs having transition invariants of height ω I such that x0 T x1 T . . . 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 [4]. The proof uses a simulation of the ordering of H(R1 ∪ · · · ∪ Rk ) in the inclusion ordering over the set of k-branching trees, whose branches are decreasing sequences in R1 ⊕· · ·⊕Rk [1]. 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é [7] and Blass and Gurevich [3] have already observed that the computation of the ordinal height of a relation proven to be well-founded by the Termination Theorem is the natural product of the individual heights. 4 Conclusion and future work 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 ter- minating 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 Dick- son 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. 239 S.Berardi et al. Proving termination of programs having transition invariants of height ω References 1. S. Berardi, P. Oliva, and S. Steila. Proving termination with transition invariants of height omega. Preliminary Draft, 2014. 2. S. Berardi and S. Steila. Ramsey theorem as an intuitionistic property of well founded relations. pages 93–107, 2014. RTA-TLCA. 3. A. Blass and Y. Gurevich. Program termination and well partial orderings. ACM Trans. Comput. Logic, 9(3):18:1–18:26, 2008. 4. P. Carruth. Arithmetic of ordinals with applications to the theory of ordered abelian groups. Bull. Amer. Math. Soc., 48(4):223–334. 5. B. Cook, A. Podelski, and A. Rybalchenko. Abstraction refinement for termination. In SAS, pages 87–101, 2005. 6. T. Coquand. An analysis of ramsey’s theorem. Inf. Comput., 110(2):297–304, 1994. 7. C. Delhommé. Height of a Superposition. Order, 23(2-3):221–233, 2006. 8. D. Figueira, S. Figueira, S. Schmitz, and Ph. Schnoebelen. Ackermannian and primitive-recursive bounds with Dickson’s Lemma. In LICS 2011: Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, pages 269–278. IEEE Press, 2011. 9. A. Podelski and A. Rybalchenko. Transition invariants. In LICS, pages 32–41. IEEE Computer Society, 2004. 240