Collecting interpretations 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. Exact collecting interpretations of expressions are developed for three abstract functional languages: a strict first-order language, a nonstrict first-order language, and a nonstrict higher order language (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 nonstrict higher order languages). Correctness of the interpretations with respect to the standard semantics is shown via a generalization of the notion of strictness. It is further shown how to form abstractions of these exact interpretations, using as an example a collecting strictness analysis which yields compile-time information not previously captured by conventional strictness analyses.

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: DONZEAU-GOuGE, V. Denotational definition of properties of program computations. In Program Flow Analysis: Theory and Applications. Prentice-Hall, Englewood Cliffs, N.J., pp. 343-379.
• 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: GOLDBERG, B., AND HUnAK, P. Detecting sharing of partial applications in functional languages. YALEU/DCS/RR-526, Dept. Computer Science, Yale University, New Haven, Conn., Mar. 1987.
• 8: 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]
• 9: HUD^K, P. Collecting interpretations of expressions. Res. Rep. YALEU/DCS/RR-497, Dep. Computer Science, Yale University, New Haven, Conn., 1986.
• 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: JONES, N.D. Private communications, June 1987.
• 13: JONES, N. D., AND MUCSNICK, S. S. Complexity of fiow analysis, inductive assertion synthesis, and a language due to Dijkstra. In Program Flow Analysis: Theory and Applications. Prentice-Hall, Englewood Cliffs, N. J, 1981, pp. 380-393.
• 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: JONES, N., AND SOND~RGAARD, H. A semantics-based framework for the abstract interpretation of 'Prolog.' In Abstract Interpretation of Declaratwe Languages. Ellis Horwood, Chichester, England, 1987, pp. 123-142.
• 16: Gary Lindstrom, Static evaluation of functional programs, ACM SIGPLAN Notices, v.21 n.7, p.196-206, July 1986
• 17: MELHSS, C. Abstract interpretation of PROLOG programs. In Abstract Interpretation of Declarative Languages. Ellis Horwood, Chichester, England, 1987, pp. 181-198.
• 18: MYCROF% A. Abstract interpretation and optimizing transformations for applicative programs. Ph.D. dissertation, University of Edinburgh, Edinburgh, Scotland, 1981
• 19: 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
• 20: NmLSON, F. Abstract Interpretation Using Domain Theory. Ph.D. dissertation, University of Edinburgh, Edmburgh, Scotland, Oct. 1984.
• 21: NmLSON, F. A denotational framework for data fiow analysis. Acta Inform. 18 (1982), 265-287.
• 22: David A. Schmidt, Denotational semantics: a methodology for language development, William C. Brown Publishers, Dubuque, IA, 1986
• 23: Joseph E. Stoy, Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory, MIT Press, Cambridge, MA, 1977
• 24: 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
• 25: YOUNG, J. The semantic analysis of functional programs: Theory and practice. Ph D. dissertation, Dep. Computer Science, Yale Umversity, New Haven, Conn., 1988.

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:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications
          Subjects: Applicative (functional) languages
      D.3.4 Processors
          Subjects: Compilers

  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES

General Terms:
Languages, Theory

Keywords:
theory