|
|
On the Power and Limitations of Strictness AnalysisStrictness analysis is an important technique for optimization of lazy functional
languages. It is well known that all strictness analysis methods are incomplete,
i.e., fail to report some strictness properties. In this paper, we provide the first
precise and formal characterization of the loss of information that leads to this
incompleteness. Specifically, we establish the following characterization theorem for
Mycroft's strictness analysis method and its natural generalization to non-flat domains
called ee-analysis: Mycroft's method will deduce a strictness property for program P
iff the property is independent of any constant appearing in any evaluation 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 develop 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 syntactic
characterization of information loss and E-rewriting provides an algorithm independent
proof technique for characterizing the power of strictness analysis methods. It can be
used to answer questions on completeness and incompleteness of Mycroft's method on certain
natural classes of programs. Finally, the techniques developed in this paper provide a
general principle for establishing similar results for other strictness analysis methods
such as those based on abstract interpretation. As a demonstration of the generality of
our technique, we give a characterization theorem for another variation of Mycroft's
method called dd-analysis. |
|
Maintained by Sekar, sekar@cs.sunysb.edu |