TY  - UNPD
A1  - Schmidt-Schauß, Manfred
A1  - Schütz, Marko
A1  - Sabel, David
T1  - A complete proof of the safety of Nöcker's strictness analysis
T2  - Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik ; 20
N2  - 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.
T3  - Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik - 20 
KW  - Striktheitsanalyse
KW  - Lambda-Kalkül
KW  - Letrec-Kalkül
KW  - Abstrakte Reduktion
KW  - Clean
KW  - Haskell
KW  - Sharing
KW  - Call-by-Need
KW  - strictness analysis
KW  - abstract reduction
Y1  - 2005
UR  - http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/4394
UR  - https://nbn-resolving.org/urn:nbn:de:hebis:30-11005
UR  - http://www.ki.informatik.uni-frankfurt.de/papers/mann/pc_sim_ndnd_IB200106.pdf
EP  - 90
PB  - Johann Wolfgang Goethe-Univ., Fachbereich Informatik und Mathematik, Inst. für Informatik, Research group for Artificial Intelligence and Software Technology
CY  - Frankfurt [am Main]
ER  -