Size-change termination principle
 | This article may be too technical for most readers to understand. (June 2018) |
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
[edit]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
[edit]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
[edit]- ^ a b c d 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. S2CID 12721873.
- ^ 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. S2CID 9093670.
- ^ Sereni, Damien; Jones, Neil D. (2005). "Termination Analysis of Higher-Order Functional Programs". Programming Languages and Systems. Lecture Notes in Computer Science. Vol. 3780. pp. 281–297. CiteSeerX 10.1.1.102.4934. 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. Vol. 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. Vol. 6337. pp. 22–50. CiteSeerX 10.1.1.167.8500. doi:10.1007/978-3-642-15769-1_4. ISBN 978-3-642-15768-4.