Size-Change Termination, Monotonicity Constraints and Ranking Functions

  • Amir M. Ben-Amram
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5643)


Size-change termination involves deducing program termination based on the impossibility of infinite descent. To this end we may use a program abstraction in which transitions are described by monotonicity constraints over (abstract) variables. When only constraints of the form x > y′ and x ≥ y′ are allowed, we have size-change graphs, for which both theory and practice are now more evolved then for general monotonicity constraints. This work shows that it is possible to transfer some theory from the domain of size-change graphs to the general case, complementing and extending previous work on monotonicity constraints. Significantly, we provide a procedure to construct explicit global ranking functions from monotonicity constraints in singly-exponential time, which is better than what has been published so far even for size-change graphs. We also consider the integer domain, where general monotonicity constraints are essential because the domain is not well-founded.


Logic Program Transition System Ranking Function Monotonicity Constraint Mixed Graph 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Ben-Amram, A.M., Lee, C.S.: Size-change analysis in polynomial time. ACM Transactions on Programming Languages and Systems 29(1) (2007)Google Scholar
  2. 2.
    Ben-Amram, A.M., Lee, C.S.: Ranking functions for size-change termination II. Logical Methods in Computer Science (to appear, 2009)Google Scholar
  3. 3.
    Brodsky, A., Sagiv, Y.: Inference of inequality constraints in logic programs. In: Proceedings of the Tenth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems (PODS), pp. 227–240. ACM Press, New York (1991)CrossRefGoogle Scholar
  4. 4.
    Codish, M., Lagoon, V., Stuckey, P.J.: Testing for termination with monotonicity constraints. In: Gabbrielli, M., Gupta, G. (eds.) ICLP 2005. LNCS, vol. 3668, pp. 326–340. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  5. 5.
    Codish, M., Taboch, C.: A semantic basis for termination analysis of logic programs. The Journal of Logic Programming 41(1), 103–123 (1999); preliminary (conference) version in LNCS 1298. Springer, Heidelberg (1997)Google Scholar
  6. 6.
    Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Conference Record of the Fifth annual ACM Symposium on Principles of Programming Languages, pp. 84–96. ACM, New York (1978)Google Scholar
  7. 7.
    Dershowitz, N., Lindenstrauss, N., Sagiv, Y., Serebrenik, A.: A general framework for automatic termination analysis of logic programs. Applicable Algebra in Engineering, Communication and Computing 12(1-2), 117–156 (2001)MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    Lee, C.S.: Ranking functions for size-change termination. ACM Transactions on Programming Languages and Systems (to appear, 2009)Google Scholar
  9. 9.
    Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. In: Proceedings of the Twenty-Eigth ACM Symposium on Principles of Programming Languages, vol. 28, pp. 81–92. ACM Press, New York (2001)Google Scholar
  10. 10.
    Lindenstrauss, N., Sagiv, Y.: Automatic termination analysis of Prolog programs. In: Naish, L. (ed.) Proceedings of the Fourteenth International Conference on Logic Programming, Leuven, Belgium, pp. 64–77. MIT Press, Cambridge (1997)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Amir M. Ben-Amram
    • 1
  1. 1.Academic College of Tel-Aviv YaffoIsrael

Personalised recommendations