Closure analysis in constraint form

ABSTRACT

Flow analyses of untyped higher-order functional programs have in the past decade been presented by Ayers, Bondorf, Consel, Jones, Heintze, Sestoft, Shivers, Steckler, Wand, and others. The analyses are usually defined as abstract interpretations and are used for rather different tasks such as type recovery, globalization, and binding-time analysis. The analyses all contain a global closure analysis that computes information about higher-order control-flow. Sestoft proved in 1989 and 1991 that closure analysis is correct with respect to call-by-name and call-by-value semantics, but it remained open if correctness holds for arbitrary beta-reduction.This article answers the question; both closure analysis and others are correct with respect to arbitrary beta-reduction. We also prove a subject-reduction result: closure information is still valid after beta-reduction. The core of our proof technique is to define closure analysis using a constraint system. The constraint system is equivalent to the closure analysis of Bondorf, which in turn is based on Sestoft's.

REFERENCES

• 1: Ole Agesen , Jens Palsberg , Michael I. Schwartzbach, Type Inference of SELF, Proceedings of the 7th European Conference on Object-Oriented Programming, p.247-267, July 26-30, 1993
• 2: AYERS, A. 1992. Efficient closure analysis with reachability. In Proceedzngs of WSA '92, Analyse Statique. IRISA, Rennes, France, 126-134.
• 3: BARENDREGT, H. P. 1981. The Lambda Calculus: Its Syntax and Semantics. North-HoIland, Amsterdam.
• 4: BONDORF, A. 1993. Similix 5.0 Manual. DIKU, University of Copenhagen, Denmark. Included in Similix 5.0 distribution.
• 5: Anders Bondorf, Automatic autoprojection of higher order recursive equations, Science of Computer Programming, v.17 n.1-3, p.3-34, Dec. 1991
• 6: Anders Bondorf , Olivier Danvy, Automatic autoprojection of recursive equations with global variable and abstract data types, Science of Computer Programming, v.16 n.2, p.151-195, Sept. 1991 [doi>10.1016/0167-6423(91)90002-F]
• 7: BONDORF, A. AND JOaGENSEN, J. 1993. Efficient analyses for realistic off-line partial evaluation. J. Func~wnal Program. 3, 3, 315-346.
• 8: Charles Consel, Binding time analysis for high order untyped functional languages, Proceedings of the 1990 ACM conference on LISP and functional programming, p.264-272, June 27-29, 1990, Nice, France [doi>10.1145/91556.91668]
• 9: GIANNINI, P. AND ROCCA, S. R. D. 1988. Characterization of typings in polymorphic type discipline. In Proceedings of LICS'88, 3rd Annual Symposium on Logic in Computer Science. IEEE, New York, 61-70.
• 10: Nevin Heintze, Set-based analysis of ML programs, Proceedings of the 1994 ACM conference on LISP and functional programming, p.306-317, June 27-29, 1994, Orlando, Florida, United States
• 11: Nevin Charles Heintze, Set based program analysis, Carnegie Mellon University, Pittsburgh, PA, 1992
• 12: Neil D. Jones, Flow Analysis of Lambda Expressions (Preliminary Version), Proceedings of the 8th Colloquium on Automata, Languages and Programming, p.114-128, July 13-17, 1981
• 13: PALSBERG, J. 1993. Correctness of binding-time analysis. J. Functional Program. 3, 3,347-363.
• 14: PALSBERG, J. AND SCHWARTZBACH, M. I. 1994a. Binding-time analysis: Abstract interpretation versus type inference. In Proceedzngs of ICCL '9~, 5th IEEE International Conference on Computer Languages. IEEE, New York, 289-298.
• 15: Jens Palsberg , Michael I. Schwartzbach, Object-oriented type systems, John Wiley and Sons Ltd., Chichester, UK, 1994
• 16: Jens Palsberg , Michael I. Schwartzbach, Safety analysis versus type inference, Information and Computation, v.118 n.1, p.128-141, April 1995 [doi>10.1006/inco.1995.1058]
• 17: Jens Palsberg , Michael I. Schwartzbach, Safety analysis versus type inference for partial types, Information Processing Letters, v.43 n.4, p.175-180, Sept. 28, 1992 [doi>10.1016/0020-0190(92)90196-3]
• 18: Jens Palsberg , Michael I. Schwartzbach, Object-oriented type inference, Conference proceedings on Object-oriented programming systems, languages, and applications, p.146-161, October 06-11, 1991, Phoenix, Arizona, United States
• 19: SESTOFT, P. 1991. Analysis and efficient implementation of functional programs. Ph.D. thesis, DIKU, University of Copenhagen.
• 20: SESTOFT, P. 1989. Replacing function parameters by global variables. M.S. thesis, DIKU, University of Copenhagen.
• 21: SmvErtS, O. 1991a. Control-flow analysis of higher-order languages. Ph.D. thesis, CMU-CS- 91-145, Carnegie Mellon University, Pittsburgh, Pa.
• 22: SHIVERS~ O. 1991b. Data-flow analysis and type recovery in Scheme. In Topics in Advanced Language Implementation, P. Lee, Ed. MIT Press, Cambridge, Mass., 47-87.
• 23: David Ungar , Randall B. Smith, Self: The power of simplicity, Conference proceedings on Object-oriented programming systems, languages and applications, p.227-242, October 04-08, 1987, Orlando, Florida, United States
• 24: Mitchell Wand , Paul Steckler, Selective and lightweight closure conversion, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.435-445, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.178044]

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications
          Subjects: Applicative (functional) languages
      D.3.4 Processors
          Subjects: Optimization

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Logics of programs
      F.3.2 Semantics of Programming Languages
          Subjects: Operational semantics
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.3 Formal Languages
          Subjects: Operations on languages

General Terms:
Languages, Theory

Keywords:
constraints, correctness proof, flow analysis