Size-change termination principle

Add links
Source: Wikipedia, the free encyclopedia.

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.[1] 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.[2] Size-change analysis is applicable to both first-order[1] and higher-order functional programs,[3] as well as imperative programs[4] and logic programs.[5] 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.[1] 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.[1]

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.[6]

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

  1. ^
    S2CID 12721873
    .
  2. S2CID 9093670
    .
  3. ISBN 978-3-540-29735-2
    .
  4. ISBN 978-3-540-33438-5
    .
  5. ^ Lindenstrauss, Naomi and Sagiv, Yehoshua. Automatic Termination Analysis of Prolog Programs. Proceedings of the Fourteenth International Conference on Logic Programming. MIT Press, 1997.
  6. ISBN 978-3-642-15768-4
    .

External links
Retrieved from "https://en.wikipedia.org/w/index.php?title=Size-change_termination_principle&oldid=1170137032"