Size-change termination, monotonicity constraints and ranking functions

Abstract

Size-Change Termination (SCT) is a method of proving program termination based on the impossibility of infinite descent. To this end we may use a program abstraction in which transitions are described by monotonicity constraints over (abstract) variables. Size-change graphs are a subclass where only constraints of the form x > y′ and x ≥ y′ are allowed. Both theory and practice are now more evolved in this restricted framework than in the general framework of monotonicity constraints. This paper shows that it is possible to adapt and extend some theory from the domain of size-change graphs to the general case, thus complementing previous work on monotonicity constraints. In particular, we present precise decision procedures for termination; and we provide a procedure to construct explicit global ranking functions from monotonicity constraints in singly-exponential time, which is better than what has been published so far even for size-change graphs. © Ben-Amram.