On the Power and Limitation of Strictness Analysis Based on Abstract Interpretation

Abstract

Strictness analysis based on abstract interpretation 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 method called old-analysis.