Modeling, Sharing, and Recursion for Weak Reduction Strategies using Explicit Substitution

<p>We present the lambda sigma^a_w calculus, a formal synthesis of the concepts of<br />sharing and explicit substitution for weak reduction. We show how<br />lambda sigma^a_w can be used as a foundation of implementations of functional<br />programming languages by modelling the essential ingredients of such<br />implementations, namely weak reduction strategies, recursion, space<br />leaks, recursive data structures, and parallel evaluation, in a uniform way.<br />First, we give a precise account of the major reduction strategies<br />used in functional programming and the consequences of choosing <br /> lambda-graph-reduction vs. environment-based evaluation. Second, we show<br />how to add constructors and explicit recursion to give a precise account<br />of recursive functions and data structures even with respect to<br />space complexity. Third, we formalize the notion of space leaks in lambda sigma^a_w<br />and use this to define a space leak free calculus; this suggests optimisations<br />for call-by-need reduction that prevent space leaking and enables<br />us to prove that the "trimming" performed by the STG machine does<br />not leak space.<br />In summary we give a formal account of several implementation<br />techniques used by state of the art implementations of functional programming<br />languages.</p><p>Keywords. Implementation of functional programming, lambda<br />calculus, weak reduction, explicit substitution, sharing, recursion, space<br />leaks.</p>