Abstract
A safe abstraction is presented for a restricted form of term graph rewriting. This abstraction can be seen as a formalisation of the rewrite system employed by the strictness analyser in the Concurrent Clean compiler. Programs written in a core functional language are interpreted as graph rewriting systems using a form of equational term graph rewriting due to Ariola and Arvind. Abstract graphs are defined by extending the signature of ordinary graphs and it is shown how to extend a rewriting system on ordinary graphs to one on abstract graphs. An abstraction relation between abstract graphs is used to define a notion of safety with respect to a variant of Ariola and Arvind’s direct approximation semantics, and this notion of safety is shown to be adequate for strictness analysis. Abstract reduction is defined as the union of the extended rewrite system with additional ‘heuristic’ reductions and shown to be safe.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abramsky, S., Hankin, C.L. (eds.): Abstract Interpretation of Declarative Languages. Computers and Their Applications. Ellis Horwood (1987)
Ariola, Z., Klop, J.W.: Equational term graph rewriting. Fundamentae Informatica 26(3,4), 207–240 (1996)
Ariola, Z., Arvind: Properties of a first-order functional language with sharing. Theoretical Computer Science 146(1-2), 69–108 (1995)
Ariola, Z., Blom, S.: Cyclic lambda calculi. In: Ito, T., Abadi, M. (eds.) TACS 1997. LNCS, vol. 1281. Springer, Heidelberg (1997)
Barendregt, H.P., van Eekelen, M.C.J.D., Glauert, J.R.W., Kennaway, J.R., Plasmeijer, M.J., Sleep, M.R.: Term graph rewriting. In: de Bakker, J.W., Nijman, A.J., Treleaven, P.C. (eds.) PARLE 1987. LNCS, vol. 259, pp. 141–158. Springer, Heidelberg (1987)
Barendsen, E., Smetsers, S.: Uniqueness typing for functional languages with graph rewriting semantics. Mathematical Structures in Computer Science 6, 579–612 (1996)
Chuang, T.-R., Goldberg, B.: A syntactic approach to fixed point computation on finite domains. In: Proc. 1992 ACM Conference on LISP and Functional Programming. ACM, New York (1992)
Clark, D.J., Hankin, C.: A lattice of abstract graphs. In: Penjam, J., Bruynooghe, M. (eds.) PLILP 1993. LNCS, vol. 714, pp. 318–331. Springer, Heidelberg (1993)
Clark, D.J.: Term Graph Rewriting and Event Structures. PhD thesis, Imperial College, University of London (1996)
Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixed points. In: Proc. Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, pp. 238–252 (1977)
Gordon, A.D., Pitts, A.M. (eds.): Higher Order Operational Techniques in Semantics. Publications of the Newton Institute. Cambridge University Press (1998)
Goubault, E., Hankin, C.L.: A lattice for the abstract interpretation of term graph rewriting systems. In: Term Graph Rewriting, theory and practice, pp. 131–140. John Wiley and Sons Ltd, Chichester (1993)
Kennaway, J.R., Klop, J.W., Sleep, M.R., de Vries, F.J.: Comparing curried and uncurried rewriting. J. Symbolic Computation 21, 15–39 (1996)
Klop, J.W.: Term rewriting systems. In: Abramsky, S., Gabbay, D.M., Maibaum, T. (eds.) Handbook of Logic in Computer Science, vol. 2, pp. 1–116. Oxford University Press, New York (1992)
Nielson, F., Nielson, H.R., Hankin, C.L.: Principles of Program Analysis. Springer, Heidelberg (1999)
Nöcker, E.: Strictness analysis based on abstract reduction of term graph rewrite systems. In: Proc. Workshop on Implementation of Lazy Functional Languages (1988)
Nöcker, E.: Strictness analysis using abstract reduction. In: Proc. Conference on Functional Programming Languages and Computer Architectures (FPCA 1993), Copenhagen. ACM Press, New York (1993)
Nöcker, E.: Efficient Functional Programming. PhD thesis, Department of Computer Science, University of Nijmegen, Toernooiveld 1, 6525 ED Nijmegen, The Netherlands (1994)
Sands, D., Moran, A.: Improvement in a lazy context: an operational theory for call-by-need. In: Proc. Twenty-sixth ACM Symposium on Principles of Programming Languages, San Antonio, Texas (January 1999)
Schütz, M., Schmidt-Schauß, M., Panitz, S.E.: Strictness analysis by abstract reduction using a tableau calculus. In: Mycroft, A. (ed.) SAS 1995. LNCS, vol. 983, pp. 348–365. Springer, Heidelberg (1995)
Turner, D.N., Wadler, P., Mossin, C.: Once upon a type. In: Proc. 7th International Conference on Functional Programming and Computer Architecture, San Diego, California (June 1995)
van Eekelen, M.C.J., Goubault, E., Hankin, C.L., Nöcker, E.: Abstract reduction: Towards a theory via abstract interpretation. In: Term Graph Rewriting, theory and practice, pp. 117–130. John Wiley and Sons Ltd, Chichester (1993)
van Oostrom, V.: Confluence for Abstract and Higher-Order Rewriting. PhD thesis, Vrije Universiteit, Amsterdam (1994)
Wansbrough, K., Jones, S.P.: Once upon a polymorphic type. In: Proc. Twenty-sixth ACM Symposium on Principles of Programming Languages, San Antonio, Texas (January 1999)
Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Information and Computation 115(1), 38–94 (1994)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Clark, D., Hankin, C., Hunt, S. (2000). Safety of Strictness Analysis via Term Graph Rewriting. In: Palsberg, J. (eds) Static Analysis. SAS 2000. Lecture Notes in Computer Science, vol 1824. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45099-3_6
Download citation
DOI: https://doi.org/10.1007/978-3-540-45099-3_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67668-3
Online ISBN: 978-3-540-45099-3
eBook Packages: Springer Book Archive