Hostname: page-component-8448b6f56d-c47g7 Total loading time: 0 Render date: 2024-04-24T00:00:56.060Z Has data issue: false hasContentIssue false
  • English
  • Français

Safety of Nöcker's strictness analysis

Part of: JFP Research Articles

Published online by Cambridge University Press:  08 November 2007

MANFRED SCHMIDT-SCHAUSS ,
DAVID SABEL  and
MARKO SCHÜTZ
MANFRED SCHMIDT-SCHAUSS
Affiliation:
Institut für Informatik, Johann Wolfgang Goethe-Universität, Postfach 11 19 32, D-60054 Frankfurt, Germany (e-mail: schauss@ki.informatik.uni-frankfurt.de)
DAVID SABEL
Affiliation:
Institut für Informatik, Johann Wolfgang Goethe-Universität, Postfach 11 19 32, D-60054 Frankfurt, Germany (e-mail: schauss@ki.informatik.uni-frankfurt.de)
MARKO SCHÜTZ
Affiliation:
University of Puerto Rico at Mayagüez, Department of Mathematical Sciences, Mayagüez, PR 00681
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

This paper proves correctness of Nöcker's method of strictness analysis, implemented in the Clean compiler, which is an effective way for strictness analysis in lazy functional languages based on their operational semantics. We improve upon the work Clark, Hankin and Hunt did on the correctness of the abstract reduction rules in two aspects. Our correctness proof is based on a functional core language and a contextual semantics, thus proving a wider range of strictness-based optimizations as correct, and our method fully considers the cycle detection rules, which contribute to the strength of Nöcker's strictness analysis.

Our algorithm SAL is a reformulation of Nöcker's strictness analysis algorithm in a functional core language LR. This is a higher order call-by-need lambda calculus with case, constructors, letrec, and seq, which is extended during strictness analysis by set constants like Top or Inf, denoting sets of expressions, which indicate different evaluation demands. It is also possible to define new set constants by recursive equations with a greatest fixpoint semantics. The operational semantics of LR is a small-step semantics. Equality of expressions is defined by a contextual semantics that observes termination of expressions. Basically, SAL is a nontermination checker. The proof of its correctness and hence of Nöcker's strictness analysis is based mainly on an exact analysis of the lengths of evaluations, i.e., normal-order reduction sequences to WHNF. The main measure being the number of “essential” reductions in evaluations.

Our tools and results provide new insights into call-by-need lambda calculi, the role of sharing in functional programming languages, and into strictness analysis in general. The correctness result provides a foundation for Nöcker's strictness analysis in Clean, and also for its use in Haskell.

Type
Articles
Information
Journal of Functional Programming , Volume 18 , Issue 4 , July 2008 , pp. 503 - 551
Copyright
Copyright © Cambridge University Press 2007

References

Abramsky, S. & Hankin, C. (1987) Abstract Interpretation of Declarative Languages. Chichester, UK: Ellis Horwood.Google Scholar
Ariola, Zena M. & Blom, S. (2002) Skew confluence and the lambda calculus with letrec. Ann. Pure Appl. Logic, 117, 95–168.CrossRefGoogle Scholar
Ariola, Zena M., & Klop, Jan Willem. (1997) Lambda calculus with explicit recursion. Inf. Comput., 139 (2), 154–233.CrossRefGoogle Scholar
Ariola, Z. M., & Arvind, . (1995) Properties of a first-order functional language with sharing. Theor. Comput. Sci., 146 (3), 69–108.CrossRefGoogle Scholar
Ariola, Z. M., Felleisen, M., Maraist, J., Odersky, M., & Wadler, P. (1995) A call-by-need lambda calculus. In Principles of Programming Languages. San Francisco, California: ACM Press, pp. 233–246.Google Scholar
Baader, Franz, & Nipkow, Tobias. (1998) Term Rewriting and All That. Cambridge: Cambridge University Press.CrossRefGoogle Scholar
Barendregt, H. P. (1984) The Lambda Calculus. Its Syntax and Semantics. Amsterdam, New York: North-Holland.Google Scholar
Burn, G. L., Hankin, C. L., & Abramsky, S. (1985) The theory for strictness analysis for higher order functions. In Programs as Data Structures. Gazinger, H. & Jones, N. D. (eds) Lecture Notes in Computer Science, vol. 217.) pp. 42–62. New York: Springer.Google Scholar
Burn, Geoffrey. (1991) Lazy Functional Languages: Abstract Interpretation and Compilation. London: Pitman.Google Scholar
Clark, David, Hankin, Chris, & Hunt, Sebastian. (2000) Safety of strictness analysis via term graph rewriting. SAS 2000, pp. 95–114.CrossRefGoogle Scholar
Coppo, M., Damiani, F., & Giannini, P. (2002) Strictness, totality, and non-standard type inference. Theor. Comput. sci., 272 (1-2), 69–112.CrossRefGoogle Scholar
Cousot, Patrick, & Cousot, Radhia. (1977) Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the Fourth ACM Symposium on Principles of Programming Languages. New York: ACM Press.Google Scholar
Dezani-Ciancaglini, Mariangiola, Tiuryn, Jerzy, & Urzyczyn, Pawel. (1999) Discrimination by parallel observers: The algorithm. Inf. Comput., 150 (2), 153–186.CrossRefGoogle Scholar
Felleisen, Matthias, & Hieb, R. (1992) The revised report on the syntactic theories of sequential control and state. Theor. Comput. Sci., 103, 235–271.CrossRefGoogle Scholar
Gasser, Kirsten Lackner Solberg, Nielson, Hanne Riis, & Nielson, Flemming. (1998) Strictness and totality analysis. Sci. Comput. Prog., 31 (1), 113–145.CrossRefGoogle Scholar
Gordon, Andrew D. (1994) A tutorial on coinduction and functional programming. In Functional programming, Glasgow 1994. Workshops in Computing.) New York: Springer pp. 78–95.Google Scholar
Jensen, Thomas P. (1998) Inference of polymorphic and conditional strictness properties. In Symposium on Principles of Programming Languages. San Diego: ACM Press, pp. 209–221.Google Scholar
Kennaway, Richard, Klop, Jan Willem, Sleep, M. Ronan, & deVries, Fer-Jan Vries, Fer-Jan. (1993) Infinitary lambda calculi and böhm models. In Proc. RTA 95. LNCS, no. 914. Hisang, J. (ed), New York: Springer, pp. 257–270.Google Scholar
Kuo, Tsun-Ming, & Mishra, Prateek. (1989) Strictness analysis: A new perspective based on type inference. In Functional Programming Languages and Computer Architecture. San Diego: ACM Press, pp. 260–272.Google Scholar
Launchbury, John, & Peyton Jones, Simon. (1995) State in Haskell. LISP Symb. Comput., 8 (2), 293–341.Google Scholar
Lévy, J.-J. (1976) An algebraic interpretation of the λβκ-calculus and an application of a labelled λ-calculus. Theor. Comput. Sci., 2 (1), 97–114.CrossRefGoogle Scholar
Mann, Matthias. (2004) Towards sharing in lazy computation systems. Frank Report 18. Institut für Informatik, J. W. Goethe-Universität Frankfurt, Germany.Google Scholar
Moran, A. K. D., & Sands, D. (1999) Improvement in a lazy context: An operational theory for call-by-need. POPL 1999. New York: ACM Press, pp. 43–56.Google Scholar
Moran, Andrew K. D., Sands, David, & Carlsson, Magnus. (1999) Erratic fudgets: A semantic theory for an embedded coordination language. In Coordination '99. Lecture Notes in Computer Science, vol. 1594. New York: Springer, pp. 85–102.Google Scholar
Mycroft, Alan. (1981) Abstract interpretation and optimising transformations for applicative programs. Ph.D. thesis, University of Edinburgh.Google Scholar
Nöcker, E., Smetsers, J. E., vanEekelen, M. Eekelen, M., & Plasmeijer, M. J. (1991) Concurrent Clean. In Proceedings of Parallel Architecture and Languages Europe (parle'91). New York: Springer Verlag, pp. 202–219.CrossRefGoogle Scholar
Nöcker, Eric. (1990) Strictness analysis using abstract reduction. Technical Report 90-14. Department of Computer Science, University of Nijmegen.Google Scholar
Nöcker, Eric. (1992) Strictness analysis by abstract reduction in orthogonal term rewriting systems. Technical Report 92-31. University of Nijmegen, Department of Computer Science.CrossRefGoogle Scholar
Nöcker, Eric. (1993) Strictness analysis using abstract reduction. In Functional Programming Languages and Computer Architecture. San Diego: ACM Press, pp. 255–265.Google Scholar
Pape, Dirk. (1998) Higher order demand propagation. In Implementation of Functional Languages (IFL '98) London. Hammond, K., Davie, A.J.T., & Clack, C. (eds), (Lecture Notes in Computer Science, vol. 1595.) New York: Springer. pp. 155–170.Google Scholar
Pape, Dirk. (2000) Striktheitsanalysen funktionaler Sprachen. Ph.D. thesis, Fachbereich Mathematik und Informatik, Freie Universität Berlin. (in German.)Google Scholar
Paterson, Ross. (1996) Compiling laziness using projections. In Static Analysis Symposium. (LNCS, vol. 1145). Aachen, Germany: Springer.Google Scholar
PeytonJones, Simon Jones, Simon. (2003) Haskell 98 Language and Libraries. Cambridge: Cambridge University Press. http://www.haskell.org.Google Scholar
PeytonJones, Simon Jones, Simon, & Marlow, Simon. (2002) Secrets of the Glasgow Haskell compiler inliner. J. Funct. Prog., 12 (4&5), 393–434.CrossRefGoogle Scholar
Peyton, Jones, Simon, L., & Santos, André. (1994) Compilation by transformation in the Glasgow Haskell Compiler. In Functional programming, Glasgow 1994. Workshops in Computing. New York: Springer, pp. 184–204.Google Scholar
Pitts, A. M. (1994) A coinduction principle for recursively defined domains. Theor. Comput. Sci., 124, 195–219.CrossRefGoogle Scholar
Pitts, Andrew D. (2000) Parametric polymorphism and operational equivalence. Math. Struct. Comput. Sci., 10, 321–359.CrossRefGoogle Scholar
Pitts, Andrew M. (2002) Operational semantics and program equivalence. Applied Semantics. (Lecture Notes in Computer Science, Vol. 2395. O'Donnell, J. T. (ed), New York: Springer pp. 378–412.CrossRefGoogle Scholar
Plasmeijer, R., & vanEekelen, M. Eekelen, M. (2003) The Concurrent Clean Language Report: Version 1.3 and 2.0. Tech. rept. Dept. of Computer Science, University of Nijmegen. http://www.cs.kun.nl/~clean/.Google Scholar
Plotkin, Gordon D. (1975) Call-by-name, call-by-value, and the lambda-calculus. Theor. Comput. Sci., 1, 125–159.CrossRefGoogle Scholar
Sands, D., Gustavsson, J., & Moran, A. (2002) Lambda calculi and linear speedups. The Essence of Computation 2002, New York, NY: Springer-Verlag, pp. 60–84.CrossRefGoogle Scholar
Santos, A. (1995) Compilation by Transformation in Non-Strict Functional Languages. Ph.D. thesis, University of Glasgow.Google Scholar
Schmidt-Schauß, M. (2003) FUNDIO: A lambda-calculus with a letrec, case, constructors, and an IO-interface: Approaching a theory of unsafePerformIO. Frank report 16. Institut für Informatik, J.W. Goethe-Universität Frankfurt am Main.Google Scholar
Schmidt-Schauß, M., Schütz, M. & Sabel, D. (2007) Appendix to “Safety of Nöcker's strictness analysis”. J. Funct. Programm. Available at: http://www.cambridge.org/journals/JFP/.CrossRefGoogle Scholar
Schmidt-Schauß, M., Panitz, S. E., & Schütz, M. (1995) Strictness analysis by abstract reduction using a tableau calculus. In Proceedings of the Static Analysis Symposium. Lecture Notes in Computer Science, no. 983. Springer-Verlag, pp. 348–365.CrossRefGoogle Scholar
Schmidt-Schauß, M., Schütz, M., & Sabel, D. (2004) On the safety of Nöcker's strictness analysis. Tech. Rept. Frank-19. Institut für Informatik. J.W. Goethe-University.Google Scholar
Schmidt-Schauß, M., Schütz, M. & Sabel, D. (2005) Deciding subset relationship of co-inductively defined set constants. Tech. Rept. Frank-23. Institut für Informatik. J.W. Goethe-University. report revised in 2006; published as Schmidt-Schauß et al. (2007) in 2007.Google Scholar
Schmidt-Schauß, M., Sabel, D. & Schütz, M. (2007) Deciding inclusion of set constants over infinite nonstrict data structures. Rairo-Theor. Inform. Appl. 41 (2), 225–241.CrossRefGoogle Scholar
Schütz, M. (1994) Striktheits-Analyse mittels abstrakter Reduktion für den Sprachkern einer nicht-strikten funktionalen Programmiersprache. Diploma thesis, Johann Wolfgang Goethe-Universität, Frankfurt.Google Scholar
Schütz, M. (2000) Analysing Demand in Nonstrict Functional Programming Languages. Dissertation, J.W. Goethe-Universität Frankfurt. Available at http://www.ki.informatik.uni-frankfurt.de/papers/marko.Google Scholar
vanEekelen, M. Eekelen, M., Goubault, E., Hankin, C. L. & Nöcker, E. (1993) Abstract reduction: Towards a theory via abstract interpretation. In Term Graph Rewriting - Theory and Practice, Sleep, M. R., Plasmeijer, M. J. & van Eekelen, M. C. J. D. (eds). Chichester: Wiley, chap. 9.Google Scholar
Wadler, P. (1987) Strictness analysis on non-flat domains (by abstract interpretation over finite domains). In Abstract interpretation of declarative languages, Abramsky, S. & Hankin, C. (eds). Chichester: Ellis Horwood Limited, chap. 12.Google Scholar
Wadler, P. & Hughes, J. (1987) Projections for strictness analysis. In Functional programming languages and computer architecture. Lecture Notes in Computer Science, no. 274. Springer, pp. 385–407.CrossRefGoogle Scholar
Supplementary material: PDF

Schmidt-Schauss Supplementary Material

Appendix.pdf

Download Schmidt-Schauss Supplementary Material(PDF)
PDF 448.4 KB
Submit a response

Discussions

No Discussions have been published for this article.