Ranking functions for size-change termination

ABSTRACT

This article explains how to construct a ranking function for any program that is proved terminating by size-change analysis.

The “principle of size-change termination” for a first-order functional language with well-ordered data is intuitive: A program terminates on all inputs, if every infinite call sequence (following program control flow) would imply an infinite descent in some data values. Size-change analysis is based on information associated with the subject program's call-sites. This information indicates, for each call-site, strict or weak data decreases observed as a computation traverses the call-site. The set DESC of call-site sequences for which the size-changes imply infinite descent is ω-regular, as is the set FLOW of infinite call-site sequences following the program flowchart. If FLOW ⊆ DESC (a decidable problem), every infinite call sequence would imply infinite descent in a well-ordering—an impossibility—so the program must terminate.

This analysis accounts for termination arguments applicable to different call-site sequences, without indicating a ranking function for the program's termination. In this article, it is explained how one can be constructed whenever size-change analysis succeeds. The constructed function has an unexpectedly simple form; it is expressed using only min, max, and lexicographic tuples of parameters and constants. In principle, such functions can be tested to determine whether size-change analysis will be successful. As a corollary, if a program verified as terminating performs only multiply recursive operations, the function that it computes is multiply recursive.

The ranking function construction is connected with the determinization of the Büchi automaton for DESC. While the result is not practical, it is of value in addressing the scope of size-change reasoning. This reasoning has been applied broadly, in the analysis of functional and logic programs, as well as term rewrite systems.

REFERENCES

• 1: Althoff, C. S., Thomas, W., and Wallmeier, N. 2005. Observations on Determinization of Büchi Automata. In Proceedings of the 10th International Conference on Implementation and Application of Automata, (CIAA'05). Springer.
• 2: Anderson, H. and Khoo, S. C. 2003. Affine-based size-change termination. In Proceedings of the 1st Asian Symposium on Programming Languages and Systems (APLAS'03), Ohori, Ed. Lecture Notes in Computer Science, vol. 2895. Springer, 122--140.
• 3: Avery, J. 2005. The size-change termination principle on non well founded data types. Tech. Rep., DIKU, Denmark.
• 4: Amir M. Ben-Amram, General size-change termination and lexicographic descent, The essence of computation: complexity, analysis, transformation, Springer-Verlag New York, Inc., New York, NY, 2002
• 5: Amir M. Ben-Amram , Chin Soon Lee, Program termination analysis in polynomial time, ACM Transactions on Programming Languages and Systems (TOPLAS), v.29 n.1, p.5-es, January 2007 [doi>10.1145/1180475.1180480]
• 6: Codish, M. Lagoon, V. and Stuckey, P. 2005. Testing for termination with monotonicity constraints. In Proceedings of the 21st International Conf. on Logic Programming, (ICLP'05).
• 7: Thomas H. Cormen , Clifford Stein , Ronald L. Rivest , Charles E. Leiserson, Introduction to Algorithms, McGraw-Hill Higher Education, 2001
• 8: Nachum Dershowitz , Zohar Manna, Proving termination with multiset orderings, Communications of the ACM, v.22 n.8, p.465-476, Aug. 1979 [doi>10.1145/359138.359142]
• 9: Frederiksen, C. C. 2001. A simple implementation of the size-change principle. Tech. Rep. D-442, DIKU, Denmark.
• 10: Frederiksen, C. C. 2002. Automatic runtime analysis for first order functional programs. Tech. Rep. D-470, DIKU, Denmark.
• 11: Glenstrup, A. and Jones, N. 2004. Termination analysis and specialization-point insertion in off-line partial evaluation. Tech. Rep. D-498, DIKU, Denmark.
• 12: Jones, N. D. and Bohr, N. 2004. Termination analysis of the untyped lambda calculus. In Proceedings of the 15th International Conference on Rewriting Techniques and Applications (RTA'04). Lecture Notes in Computer Science, vol. 3091. Springer, 1--23.
• 13: Chin Soon Lee , Neil D. Jones , Amir M. Ben-Amram, The size-change principle for program termination, Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.81-92, January 2001, London, United Kingdom
• 14: Manolios, P. and Vroon, D. 2006. Termination Analysis with Calling Context Graphs. In Proceedings of the 18th International Conf. on Computer Aided Verification (CAV'06). Springer, 401--414.
• 15: David E. Muller , Paul E. Schupp, Simulating alternating tree automata by nondeterministic automata: new results and new proofs of the theorems of Rabin, McNaughton and Safra, Theoretical Computer Science, v.141 n.1-2, p.69-107, April 17, 1995 [doi>10.1016/0304-3975(94)00214-4]
• 16: S. Safra, On the complexity of omega -automata, Proceedings of the 29th Annual Symposium on Foundations of Computer Science, p.319-327, October 24-26, 1988 [doi>10.1109/SFCS.1988.21948]
• 17: Thiemann, R. and Giesl, J. 2003. Size-change termination for term rewriting. In Proceedings of the 14th International Conf. on Rewriting Techniques and Applications (RTA'03). Lecture Notes in Computer Science, vol. 2706. Springer, 264--278.
• 18: Moshe Y. Vardi, An automata-theoretic approach to linear temporal logic, Proceedings of the VIII Banff Higher order workshop conference on Logics for concurrency : structure versus automata: structure versus automata, p.238-266, April 1996, Banff, Canada
• 19: Wahlstedt, D. 2000. Detecting termination using size-change in parameter values. Master's thesis, Göteborgs Universitet, Sweden.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

General Terms:
Theory

Keywords:
ω-Automaton, determinization, multiple recursion, ranking function, size-change termination, termination analysis