- Source: Size-change termination principle
The size-change termination principle (SCT) guarantees termination for a computer program by proving that infinite computations always trigger infinite descent in data values that are well-founded. Size-change termination analysis utilizes this principle in order to solve the universal halting problem for a certain class of programs. When applied to general programs, the principle is intended to be used conservatively, which means that if the analysis determines that a program is terminating, the answer is sound, but a negative answer means "don't know". The decision problem for SCT is PSPACE-complete; however, there exists an algorithm that computes an approximation of the decision problem in polynomial time. Size-change analysis is applicable to both first-order and higher-order functional programs, as well as imperative programs and logic programs. The latter application preceded by four years the general formulation of the principle by Lee et al.
Overview
The size-change termination principle was introduced by Chin Soon Lee, Neil D. Jones, and Amir M. Ben-Amram in 2001. It relies on intermediary objects called size-change graphs that describe the relationship between source and destination parameters in a given function call (for a functional program). The method analyzes these graphs to make conclusions about the existence of monotonically decreasing sequences of parameters throughout the execution of a program. The size-change termination principle is stated as such:If every infinite computation would give rise to an infinitely decreasing value sequence (according to the size-change graphs), then no infinite computation is possible.Size-change graphs express both the possible presence of a function call as well as whether parameters within function call decrease or do not increase. In order to derive termination from size-change graphs, Lee at al. formulate a sufficient condition in terms of the graphs (with no reference to the underlying program). This condition is decidable by an algorithm that operates solely on the graphs.
Size-change termination analysis is related to abstract interpretation, in particular to a technique called predicate abstraction.
Relationship to the halting problem
The halting problem for Turing-complete computational models states that the decision problem of whether a program will halt on a particular input, or on all inputs, is undecidable. Therefore, a general algorithm for proving any program to halt does not exist. Size-change termination is decidable because it only asks whether termination is provable from given size-change graphs.
References
External links
Amir Ben-Amram's SCT web page