|
 ABSTRACT
Strictness 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 a precise and formal characterization of the loss of information that leads to this incompletenss. Specifically, we establish the following characterization theorem for Mycroft's strictness analysis method and a generalization of this method, called ee-analysis, that reasons about exhaustive evaluation in nonflat domains: 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 and 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 programs. Finally, the techniques developed in this paper provide a general principle for establishing similar results for other 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.
REFERENCES
Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.
 |
1
|
|
| |
2
|
|
| |
3
|
|
| |
4
|
|
| |
5
|
ERNOULT, C., AND MYCROFT, A. 1995. Untyped Strictness Analysis. J. Funct. Prog. 5, 1 (Jan), 38-50.
|
| |
6
|
|
| |
7
|
|
| |
8
|
HUET, G., AND LEVY, J. 1979. Computations in nonambiguous linear term rewriting systems. Tech. Rep. 359, IRIA, Le Chesney, France.
|
| |
9
|
|
| |
10
|
HUNT, S., AND HANKIN, C. 1991. Fixed points and frontiers: a new perspective. In J. Funct. Prog. 1, 1, (Jan.), 91-120.
|
| |
11
|
O. Kaser , S. Pawagi , C. R. Ramakrishnan , I. V. Ramakrishnan , R. C. Sekar, Fast parallel implementation of lazy languages—the EQUALS experience, Proceedings of the 1992 ACM conference on LISP and functional programming, p.335-344, June 22-24, 1992, San Francisco, California, United States
|
| |
12
|
|
| |
13
|
|
| |
14
|
|
| |
15
|
C. R. Ramakrishnan , I. V. Ramakrishnan , R. C. Sekar, A symbolic constraint solving framework for analysis of logic programs, Proceedings of the 1995 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, p.12-23, June 21-23, 1995, La Jolla, California, United States
[doi> 10.1145/215465.215467]
|
| |
16
|
REDDY, U., AND KAMIN, S. 1992. On the power of abstract interpretation. In IEEE International Conference on Computer Languages. IEEE, New York, pp. 24-33.
|
| |
17
|
R. C. Sekar , Prateek Mishra , I. V. Ramakrishnan, On the power and limitation of strictness analysis based on abstract interpretation, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.37-48, January 21-23, 1991, Orlando, Florida, United States
[doi> 10.1145/99583.99591]
|
| |
18
|
|
| |
19
|
|
| |
20
|
WADLER, P. 1987. Strictness analysis on non-flat domains (by abstract interpretation over finite domains). In Abstract Interpretation of Declarative Languages, S. Abramsky and C. Hankin, eds. Ellis Horwood, Chichester, U.K., 266-275.
|
|
Adobe Acrobat
QuickTime
Windows Media Player
Real Player
Pdf
D.3