On strictness and its analysis

ABSTRACT

We study the strictness problem for the untyped lambda-calculus and for an ML-like typed calculus. We establish that strictness is a necessary and sufficient condition for the “eager” evaluation of function arguments. For the untyped calculus, we show that the strictness problem is elementary and describe a complete algorithm for strictness analysis of convergent terms. We show that typed terms possess a much richer set of strictness properties. A type-theoretic characterization of strictness is developed and it is shown that the strictness properties of a term can be represented as a collection of types related to the standard term type. A set of type inference rules that support reasoning about strictness related types is given. The inference rules are shown to be invariant under type change by substitution. This provides a sound basis for reasoning about strictness properties of terms by considering only their principal type. For our final result, we describe a practical system that carries out type checking and strictness analysis simultaneously in a unified framework. Our main result is thus the discovery that the problem of strictness analysis is a particular case of type inference.

REFERENCES

• Abramsky85: Samson Abramsky, Strictness analysis and polymorphic invariance, on Programs as data objects, p.1-23, April 1986, Copenhagen, Denmark
• Barendregt81: Barendregt, H. P., The Larnbda Calculus: Its Syntax and Semantics, North- Holland, 1981.
• Burns85: Burn, G. L., Hankin, C. L. and Abramsky, S., The Theory and Practice of Strictness Analysis for Higher-Order Functions, Research Report 85/6, Department of Computing, Imperial College.
• ClackJones85: 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
• MiDa82: 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]
• Goguen86: Goguen, J., Kirchner, C., Leinwald, S., Meseguer, J. and Winkler, T., Progress Report on the Rewrite Rule Machine, SIGARCH Newsletter, Maxch 1986.
• Haankin85: C L Hankin , G L Burn , S L Peyton Jones, A safe approach to parallel combinator reduction, Proc. of the European symposium on programming on ESOP 86, p.99-110, March 1986, Saarbru:9Aicken, Germany
• Hudak86a: 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]
• Hudak-Kranz: Hudak, P., Kranz, D., A combinatorbased compiler for a functional language, POPL XI, p. 121-131.
• Hughes85: John Hughes, Strictness detection in non-flat domains, on Programs as data objects, p.112-135, April 1986, Copenhagen, Denmark
• Johnsson: Thomas Johnsson, Efficient compilation of lazy evaluation, Proceedings of the 1984 SIGPLAN symposium on Compiler construction, p.58-69, June 17-22, 1984, Montreal, Canada
• Kowalski: Robert A. Kowalski, Logic for Problem Solving, Prentice Hall PTR, Upper Saddle River, NJ, 1979
• Kuo86: Kuo, T-M, A Practical Method for Strictness Analysis, Research Proficiency Paper, December 1986, SUNY Stony Brook.
• Lindstrom86: Gary Lindstrom, Static evaluation of functional programs, ACM SIGPLAN Notices, v.21 n.7, p.196-206, July 1986
• Milner78: Milner, R., A theory of type polymorphism in programming, JCSS 17,3, p348-375, 1978.
• MS82: David MacQueen , Gordon Plotkin , Ravi Sethi, An ideal model for recursive polymorphic types, Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.165-174, January 15-18, 1984, Salt Lake City, Utah, United States [doi>10.1145/800017.800528]
• Maurer85: Dieter Maurer, Strictness computation using special &lgr;-expressions, on Programs as data objects, p.136-155, April 1986, Copenhagen, Denmark
• Mitchell84: John C. Mitchell, Coercion and type inference, Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.175-185, January 15-18, 1984, Salt Lake City, Utah, United States [doi>10.1145/800017.800529]
• Mycroft80: 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
• Wadsworth71: Wadsworth, C. P., Semantics and Pragmatics of the lambda-calculus, Ph. D. Thesis, Oxford University, 1971.
• Wadsworth76: Wadsworth, C. P., The relation between Computational and Denotational Properties for Scott's Doo-models of the Lambda-Calculus, SIAM J. Comput., 5, 3, September 1976.
• Wray85: Wray, S. C., A New Strictness Detection Algorithm, Cambridge University, Manuscript, 21p, January 1985.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Lambda calculus and related systems

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications

          Nouns: ML
      D.3.3 Language Constructs and Features
          Subjects: Data types and structures

General Terms:
Algorithms, Languages, Theory