The size-change termination principle (SCT) guarantees termination for a

computer program A computer program is a sequence or set of instructions in a programming language for a computer to Execution (computing), execute. It is one component of software, which also includes software documentation, documentation and other intangibl ...

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 In computability theory and computational complexity theory, a decision problem is a computational problem that can be posed as a yes–no question on a set of input values. An example of a decision problem is deciding whether a given natura ...

for SCT is

PSPACE-complete In computational complexity theory, a decision problem is PSPACE-complete if it can be solved using an amount of memory that is polynomial in the input length (PSPACE, polynomial space) and if every other problem that can be solved in polynomial sp ...

; 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 In mathematics, a monotonic function (or monotone function) is a function between ordered sets that preserves or reverses the given order. This concept first arose in calculus, and was later generalized to the more abstract setting of orde ...

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 computer science, abstract interpretation is a theory of sound approximation of the semantics of computer programs, based on monotonic functions over ordered sets, especially lattices. It can be viewed as a partial execution of a computer pro ...

, in particular to a technique called ''predicate abstraction''.

Relationship to the halting problem

The

halting problem In computability theory (computer science), computability theory, the halting problem is the problem of determining, from a description of an arbitrary computer program and an input, whether the program will finish running, or continue to run for ...

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

{{reflist

External links

Amir Ben-Amram's SCT web page
Theory of computation Static program analysis