Higher-order strictness analysis in untyped lambda calculus

ABSTRACT

A function is said to be <i>strict</i> in one of its formal parameters if, in all calls to the function, either the corresponding actual parameter is evaluated, or the call does not terminate. Detecting which arguments a function will surely evaluate is a problem that arises often in program transformation and compiler optimization. We present a strategy that allows one to infer strictness properties of functions expressed in the lambda calculus. Our analysis improves on previous work in that (1) a set-theoretic characterization of strictness is used that permits treatment of <i>free variables,</i> which in turn permits a broader range of interpretations, and (2) the analysis provides an effective treatment of higher-order functions. We also prove a result due to Meyer [15]: the problem of first-order strictness analysis is complete in deterministic exponential time. However, because the size of most functions is small, the complexity seems to be tractable in practice.This research was supported in part by NSF Grant MCS-8302018, and a Faculty Development Award from IBM.

REFERENCES

• 1: Alfred V. Aho , John E. Hopcroft, The Design and Analysis of Computer Algorithms, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1974
• 2: Burn, G. L., Hankin, C. L., and Abramsky, S. The theory and practice of strictness analysis for higher order functions. DoC 85/6, Imperial College of Science and Technology, Department of Computing, April, 1985.
• 3: Ashok K. Chandra , Dexter C. Kozen , Larry J. Stockmeyer, Alternation, Journal of the ACM (JACM), v.28 n.1, p.114-133, Jan. 1981 [doi>10.1145/322234.322243]
• 4: Chris Clack , Simon L. Peyton Jones, Strictness analysis—a practical approach, Proc. of a conference on Functional programming languages and computer architecture, p.35-49, January 1985, Nancy, France
• 5: 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]
• 6: Luis Damas , Robin Milner, Principal type-schemes for functional programs, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.207-212, January 25-27, 1982, Albuquerque, Mexico [doi>10.1145/582153.582176]
• 7: Michael J. C. Gordon, The Denotational Description of Programming Languages: An Introduction, Springer-Verlag New York, Inc., Secaucus, NJ, 1979
• 8: Hudak, P. ALFL Reference Manual and Programmers Guide. Research Report YALEU/DCS/RR-322, Second Edition, Yale University, Oct., 1984.
• 9: Paul Hudak , David Kranz, A combinator-based compiler for a functional language, Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.122-132, January 15-18, 1984, Salt Lake City, Utah, United States [doi>10.1145/800017.800523]
• 10: Hudak, P. and Goldberg, B. Distributed execution of functional programs using serial combinators. Proceedings of 1985 Int'l Conf. on Parallel Proc. (and IEEE Trans. on Computers October 1985), Aug., 1985, pp. 831--839.
• 11: Paul Hudak , Benjamin Goldberg, Serial combinators: “optimal” grains of parallelism, Proc. of a conference on Functional programming languages and computer architecture, p.382-399, January 1985, Nancy, France
• 12: Hudak, P. and Young, J. A set-theoretic characterization of function strictness in the Lambda Calculus. Research Report YALEU/DCS/RR-391, Yale University, June, 1985.
• 13: Johnsson, T. Detecting when call-by-value can be used instead of call-by-need. Laboratory for Programming Methodology Memo 14, Chalmers University of Technology, Dept. of Computer Science, Oct., 1981.
• 14: Keller, R. M. FEL programmer's guide. AMPS TR 7, University of Utah, March, 1982.
• 15: Meyer, A. R. Complexity of program flow-analysis for strictness.
• 16: 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
• 17: Mycroft, A. <i>Abstract Interpretation and Optimizing Transformations for Applicative Programs.</i> Ph.D. Th., Univ. of Edinburgh, 1981.
• 18: Turner, D. A. SASL language manual University of St. Andrews, 1976.