Bounded fixed point iteration

ABSTRACT

In the context of abstract interpretation we study the number of times a functional need to be unfolded in order to give the least fixed point. For the cases of the total or monotone functions we obtain an exponential bound and in the case of strict and additive (or distributive) functions we obtain a quadratic bound. These bounds are shown to be tight. Specialising the case of strict and additive functions to functionals of a form that would correspond to iterative programs we show that a linear bound is tight. We demonstrate the relation to several analyses studied in the literature (including strictness analysis).

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: Bror Bjerner , S. Holmström, A composition approach to time analysis of first order lazy functional programs, Proceedings of the fourth international conference on Functional programming languages and computer architecture, p.157-165, September 11-13, 1989, Imperial College, London, United Kingdom [doi>10.1145/99370.99382]
• 3: G. GrS~tzer" Lattice Theory- First Concepts and Distributive Lattices, W. H. Freeman and Company, 1971.
• 4: Paul Hudak , Jonathan Young, Higher-order strictness analysis in untyped lambda calculus, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.97-109, January 01, 1986, St. Petersburg Beach, Florida [doi>10.1145/512644.512653]
• 5: J. Hughes" Backward analysis of functional programs, in Partial Evaluation and Mixed Computation (Eds. D. Bjcrner, A. P. Ershov, N. D. Jones), North-Holland, 1988.
• 6: Neil D. Jones , Alan Mycroft, Data flow analysis of applicative programs using minimal function graphs, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.296-306, January 01, 1986, St. Petersburg Beach, Florida [doi>10.1145/512644.512672]
• 7: A. Mycroft" Abstract interpretation and optimising transformations for applicative programs, Ph. D. thesis, University of Edinburgh, 1981.
• 8: 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]
• 9: 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]
• 10: H. R. Nielson, F. Nielson: Bounded Fixed Point Iteration, Technical report DAIMI PB-359, Computer Science Department, Aarhus University, 1991.
• 11: Hanne Riis Nielson , Flemming Nielson, Semantics with applications: a formal introduction, John Wiley & Sons, Inc., New York, NY, 1992
• 12: S. Peyton-jones, C. Clack: Finding fixpoints in abstract interpretations, in" Abstract Interpretations of Declarative Languages (edited by S. Abramsky & C. Hankin), Ellis Horwood, 1987.
• 13: 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:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Denotational semantics

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

General Terms:
Algorithms, Theory