ON THE POWER AND LIMITATIONS OF STRICTNESS ANALYSIS

Strictness analysis is an important technique for optimization of lazy functional languages. It is well known that all strictness analysis m ethods are incomplete, i.e., fair to report some strictness properties . In this paper, we provide a precise and formal characterization of t he loss of information that leads to this incompleteness. Specifically , we establish the following characterization theorem for Mycroft's st rictness analysis method and a generalization of this method, called e e-analysis, that reasons about exhaustive evaluation in nonflat domain s: Mycroft's method will deduce a strictness property for program P if f the property is independent of any constant appearing in any evaluat ion of P. To prove this, we specify a small set of equations, called E -axioms, that capture the information loss in Mycroft's method and dev elop a new proof technique called E-rewriting. E-rewriting extends the standard notion of rewriting to permit the use of reductions using E- axioms interspersed with standard reduction steps. E-axioms are a synt actic characterization of information loss and E-rewriting provides an algorithm-independent proof technique for characterizing the power of analysis methods. It can be used to answer questions on completeness and incompleteness of Mycroft's method on certain natural classes of p rograms. Finally, the techniques developed in this paper provide a gen eral principle for establishing similar results for other analysis met hods such as those based on abstract interpretation. As a demonstratio n of the generality of our technique, we give a characterization theor em for another variation of Mycroft's method called dd-analysis.