=Paper= {{Paper |id=Vol-1231/short1 |storemode=property |title=Proving termination of programs having transition invariants of height ω |pdfUrl=https://ceur-ws.org/Vol-1231/short1.pdf |volume=Vol-1231 |dblpUrl=https://dblp.org/rec/conf/ictcs/BerardiOS14 }} ==Proving termination of programs having transition invariants of height ω== https://ceur-ws.org/Vol-1231/short1.pdf

Proving termination of programs having
transition invariants of height ω

Stefano Berardi1 , Paulo Oliva2 , and Silvia Steila1
1
Università 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 Delhommé [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. Delhommé. 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