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.^[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.0 ^1.1 ^1.2 ^1.3 Lee, Chin Soon; Jones, Neil D.; Ben-Amram, Amir M.; Lee, Chin Soon; Jones, Neil D.; Ben-Amram, Amir M. (2001-01-01). "The size-change principle for program termination, The size-change principle for program termination". ACM SIGPLAN Notices 36 (3): 81–92. doi:10.1145/360204.360210. ISSN 0362-1340.
↑ Ben-Amram, Amir M.; Lee, Chin Soon (2007-01-01). "Program termination analysis in polynomial time". ACM Transactions on Programming Languages and Systems 29 (1): 5. doi:10.1145/1180475.1180480. ISSN 0164-0925.
↑ Sereni, Damien; Jones, Neil D. (2005). "Termination Analysis of Higher-Order Functional Programs". Programming Languages and Systems. Lecture Notes in Computer Science. 3780. pp. 281–297. doi:10.1007/11575467_19. ISBN 978-3-540-29735-2.
↑ Avery, James (2006). "Size-Change Termination and Bound Analysis". Functional and Logic Programming. Lecture Notes in Computer Science. 3945. pp. 192–207. doi:10.1007/11737414_14. ISBN 978-3-540-33438-5.
↑ Lindenstrauss, Naomi and Sagiv, Yehoshua. Automatic Termination Analysis of Prolog Programs. Proceedings of the Fourteenth International Conference on Logic Programming. MIT Press, 1997.
↑ Heizmann, Matthias; Jones, Neil D.; Podelski, Andreas (2010). "Size-Change Termination and Transition Invariants". Static Analysis. Lecture Notes in Computer Science. 6337. pp. 22–50. doi:10.1007/978-3-642-15769-1_4. ISBN 978-3-642-15768-4.

External links

Amir Ben-Amram's SCT web page

0.00

(0 votes)

Original source: https://en.wikipedia.org/wiki/Size-change termination principle. Read more

[Lee_2001-1] 1.0 ^1.1 ^1.2 ^1.3 Lee, Chin Soon; Jones, Neil D.; Ben-Amram, Amir M.; Lee, Chin Soon; Jones, Neil D.; Ben-Amram, Amir M. (2001-01-01). "The size-change principle for program termination, The size-change principle for program termination". ACM SIGPLAN Notices 36 (3): 81–92. doi:10.1145/360204.360210. ISSN 0362-1340.

[2] Ben-Amram, Amir M.; Lee, Chin Soon (2007-01-01). "Program termination analysis in polynomial time". ACM Transactions on Programming Languages and Systems 29 (1): 5. doi:10.1145/1180475.1180480. ISSN 0164-0925.

[3] Sereni, Damien; Jones, Neil D. (2005). "Termination Analysis of Higher-Order Functional Programs". Programming Languages and Systems. Lecture Notes in Computer Science. 3780. pp. 281–297. doi:10.1007/11575467_19. ISBN 978-3-540-29735-2.

[4] Avery, James (2006). "Size-Change Termination and Bound Analysis". Functional and Logic Programming. Lecture Notes in Computer Science. 3945. pp. 192–207. doi:10.1007/11737414_14. 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] Heizmann, Matthias; Jones, Neil D.; Podelski, Andreas (2010). "Size-Change Termination and Transition Invariants". Static Analysis. Lecture Notes in Computer Science. 6337. pp. 22–50. doi:10.1007/978-3-642-15769-1_4. ISBN 978-3-642-15768-4.

[1]

[2]

[3]

[4]

[5]

[6]