Proving termination of programs having transition invariants of height ω

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