A collecting interpretation of expressions

ABSTRACT

A collecting interpretation of expressions is an interpretation of a program that allows one to answer questions of the sort: “What are all possible values to which an expression might evaluate during program execution?” Answering such questions in a denotational framework is akin to traditional data flow analysis, and when used in the context of abstract interpretation allows one to infer properties that approximate the run-time behavior of expression evaluation. In this paper collecting interpretations of expressions are developed for three abstract functional languages: (1) a first-order language with call-by-value semantics, (2) a first-order language with call-by-name semantics, and (3) a higher-order language with call-by-name semantics (i.e., the full untyped lambda calculus with constants). It is argued that the method is simple (in particular, no powerdomains are needed), natural (it captures the intuitive operational behavior of a cache), yet more expressive than existing methods (it is the first exact collecting interpretation for either lazy or higher-order programs).

REFERENCES

• 1: S. Abramsky , C. Hankin, Abstract interpretation of declarative languages, Halsted Press, New York, NY, 1987
• 2: G. L. Burn , C. L. Hankin , S. Abramsky, The theory of strictness analysis for higher order functions, on Programs as data objects, p.42-62, April 1986, Copenhagen, Denmark
• 3: Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• 4: Patrick Cousot , Radhia Cousot, Systematic design of program analysis frameworks, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.269-282, January 29-31, 1979, San Antonio, Texas [doi>10.1145/567752.567778]
• 5: V. Donzeau-Gouge. I)enotational definition of properties of program computations. In Program Flow Analysis" Theory and Applications, pages 343-379, Prentice-Hall, 1981.
• 6: Jon Fairbairn , Stuart C. Wray, Code generation techniques for functional languages, Proceedings of the 1986 ACM conference on LISP and functional programming, p.94-104, August 1986, Cambridge, Massachusetts, United States [doi>10.1145/319838.319853]
• 7: Benjamin Goldberg, Detecting sharing of partial applications in functional languages, Proc. of a conference on Functional programming languages and computer architecture, p.408-425, October 1987, Portland, Oregon, United States
• 8: P. Hudak. Collecting Interpretations o/Expressions. Research Report YALEU/DCS/RR-497, Yale University, Department of Computer Science, 1986.
• 9: Paul Hudak, A semantic model of reference counting and its abstraction (detailed summary), Proceedings of the 1986 ACM conference on LISP and functional programming, p.351-363, August 1986, Cambridge, Massachusetts, United States [doi>10.1145/319838.319876]
• 10: 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]
• 11: John Hughes, Strictness detection in non-flat domains, on Programs as data objects, p.112-135, April 1986, Copenhagen, Denmark
• 12: N.D. Jones. Private communication. June 1987.
• 13: N.D. Jones and S.S. Muchnick. Complexity of flow analysis~ inductive assertion synthesis, and a language due to dijkstra. :In Program Flow Analysis" Theory and Applications, pages 380-393, Prentice-Hall, 1981.
• 14: 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]
• 15: Gary Lindstrom, Static evaluation of functional programs, Proceedings of the 1986 SIGPLAN symposium on Compiler construction, p.196-206, June 25-27, 1986, Palo Alto, California, United States
• 16: A. Mycroft. Abstract Interpretation and Optimizing Transformations for Applicative Programs. PhD thesis, University of Edinburgh~ 1981.
• 17: Alan Mycroft, The Theory and Practice of Transforming Call-by-need into Call-by-value, Proceedings of the Fourth 'Colloque International sur la Programmation' on International Symposium on Programming, p.269-281, April 22-24, 1980
• 18: F. Nielson. Abstract Interpretation Using Domain Theory. PhD thesis, University of Edinburgh, October 1984.
• 19: F. Nielson. A denotational framework for data flow analysis. Acta Informatica, 18:265-287, 1982.
• 20: David A. Schmidt, Denotational semantics: a methodology for language development, William C. Brown Publishers, Dubuque, IA, 1986
• 21: Joseph E. Stoy, Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory, MIT Press, Cambridge, MA, 1977
• 22: 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:
  D. Software
  D.2 SOFTWARE ENGINEERING

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics
      D.3.4 Processors
          Subjects: Optimization

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

General Terms:
Algorithms, Languages, Theory