Modeling Sharing and Recursion for Weak Reduction Strategies using Explicit Substitution

Zine-El-Abidine Benaissa
Pierre Lescanne
Kristoffer H. Rose

December 1996


We present the tex2html_wrap_inline25 -calculus, a formal synthesis of the concepts of sharing and explicit substitution for weak reduction. We show how tex2html_wrap_inline25 can be used as a foundation of implementations of functional programming languages by modeling the essential ingredients of such implementations, namely weak reduction strategies, recursion, space leaks, recursive data structures, and parallel evaluation, in a uniform way.

First, we give a precise account of the major reduction strategies used in functional programming and the consequences of choosing tex2html_wrap_inline29 -graph-reduction vs. environment-based evaluation. Second, we show how to add constructors and explicit recursion to give a precise account of recursive functions and data structures even with respect to space complexity. Third, we formalize the notion of space leaks in tex2html_wrap_inline25 and use this to define a space leak free calculus; this suggests optimisations for call-by-need reduction that prevent space leaking and enables us to prove that the ``trimming'' performed by the STG machine does not leak space.

In summary we give a formal account of several implementation techniques used by state of the art implementations of functional programming languages

Available as PostScript, PDF.


Last modified: 2003-06-08 by webmaster.