Finiteness conditions for fixed point iteration

ABSTRACT

This paper provides a link between the formulation of static program analyses using the framework of abstract interpretation (popular for functional languages and using the more classical framework of data flow anlysis (popular for imperative languages). In particular we show how the classical notions of fastness, rapidity and k-boundedness carry over to the abstract interpretation framework and how this may be used to bound the number of times a functional should be unfolded in order to yield the fixed point. This is supplemented with a number of results on how to calculate the bounds for iterative forms (as for tail recursion), for linear forms (as for one nested recursive call), and for primitive recursive forms. In some cases this improves the “worst case” results of, but more importantly it gives much better“average case” results.

REFERENCES

• 1: Alfred V. Aho , Ravi Sethi , Jeffrey D. Ullman, Compilers: principles, techniques, and tools, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1986
• 2: R. M. Burstall , John Darlington, A Transformation System for Developing Recursive Programs, Journal of the ACM (JACM), v.24 n.1, p.44-67, Jan. 1977 [doi>10.1145/321992.321996]
• 3: A.J. Field, P.G. Harrison: Functional Programming, Addison - Wesley (1988).
• 4: G. Gr~tzer: Lattice Theory- First Concepts and Distributive Lattices, W.H. Freeman and Company (1971).
• 5: T. J. Marlowe , B. G. Ryder, Properties of data flow frameworks: a unified model, Acta Informatica, v.28 n.2, p.121-163, Dec. 1990 [doi>10.1007/BF01237234]
• 6: A. Mycroft: Abstract Interpretation and Optimizing Transformations for Applicative Programs, University of Edinburgh Ph.D.- thesis (1981).
• 7: F. Nielson (editor): Design, Analysis and Reasoning about Tools: Abstracts from the First Workshop, Aarhus University report DAIMI PB-367 (1991).
• 8: F. Nielson, Two-level semantics and abstract interpretation, Theoretical Computer Science, v.69 n.2, p.117-242, Dec. 11, 1989 [doi>10.1016/0304-3975(89)90091-1]
• 9: Hanne Riis Nielson , Flemming Nielson, Bounded fixed point iteration, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.71-82, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143182]
• 10: F. Nielson, H.R. Nielson: Finiteness Conditions for Fixed Point Iteration, report DAIMI PB-384, Aarhus University, Denmark (February 1992).
• 11: Hanne Riis Nielson , Flemming Nielson, Transformations on higher-order functions, Proceedings of the fourth international conference on Functional programming languages and computer architecture, p.129-143, September 11-13, 1989, Imperial College, London, United Kingdom [doi>10.1145/99370.99380]
• 12: Philip Wadler , R. J. M. Hughes, Projections for strictness analysis, Proc. of a conference on Functional programming languages and computer architecture, p.385-407, October 1987, Portland, Oregon, United States

INDEX TERMS

Primary Classification:
  G. Mathematics of Computing
  G.1 NUMERICAL ANALYSIS
      G.1.5 Roots of Nonlinear Equations
          Subjects: Iterative methods

Additional Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Denotational semantics

General Terms:
Algorithms, Languages