A complete proof of the safety of Nöcker's strictness analysis
- 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 of Clark, Hankin and Hunt did on the correctness of the abstract reduction rules. Our method fully considers the cycle detection rules, which are the main strength of Nöcker's strictness analysis. Our algorithm SAL is a reformulation of Nöcker's strictness analysis algorithm in a higher-order call-by-need lambda-calculus with case, constructors, letrec, and seq, extended by set constants like Top or Inf, denoting sets of expressions. It is also possible to define new set constants by recursive equations with a greatest fixpoint semantics. The operational semantics is a small-step semantics. Equality of expressions is defined by a contextual semantics that observes termination of expressions. Basically, SAL is a non-termination 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 normal order reduction sequences. The main measure being the number of 'essential' reductions in a normal order reduction sequence. 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.
Author: | Manfred Schmidt-SchaußORCiDGND, Marko Schütz, David SabelORCiDGND |
---|---|
URN: | urn:nbn:de:hebis:30-11005 |
URL: | http://www.ki.informatik.uni-frankfurt.de/papers/mann/pc_sim_ndnd_IB200106.pdf |
Parent Title (German): | Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik ; 20 |
Series (Serial Number): | Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik (20) |
Publisher: | Johann Wolfgang Goethe-Univ., Fachbereich Informatik und Mathematik, Inst. für Informatik, Research group for Artificial Intelligence and Software Technology |
Place of publication: | Frankfurt [am Main] |
Document Type: | Working Paper |
Language: | English |
Year of Completion: | 2005 |
Year of first Publication: | 2005 |
Publishing Institution: | Universitätsbibliothek Johann Christian Senckenberg |
Release Date: | 2005/06/14 |
Tag: | Abstrakte Reduktion; Clean; Haskell; Letrec-Kalkül Call-by-Need; Sharing; abstract reduction; strictness analysis |
GND Keyword: | Striktheitsanalyse; Lambda-Kalkül |
Page Number: | 90 |
Last Page: | 90 |
HeBIS-PPN: | 344376680 |
Institutes: | Informatik und Mathematik / Informatik |
Dewey Decimal Classification: | 0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik |
Licence (German): | Deutsches Urheberrecht |