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

Resumé

We present the lambda sigma^a_w calculus, a formal synthesis of the concepts of
sharing and explicit substitution for weak reduction. We show how
lambda sigma^a_w can be used as a foundation of implementations of functional
programming languages by modelling 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
lambda-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 lambda sigma^a_w
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.

Keywords. Implementation of functional programming, lambda
calculus, weak reduction, explicit substitution, sharing, recursion, space
leaks.