Higher-Order Strictness Analysis in Untyped Lambda Calculus

Authors:

Paul Hudak and Jonathan Young

Abstract:

A function is said to be strict 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 free variables, 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.

Bibtex:

 @InProceedings{hudak-young:86,
  author =      "P. Hudak and J. Young",
  title =       "Higher-Order Strictness Analysis in Untyped Lambda Calculus",
  booktitle =   "ACM Symposium on Principles of Programming Languages",
  pages     =   "97-109",
  year =        "1986",
  month ==      "January"
} 

Links:

HOStrictness.pdf