In the last ten years there has been a steady interest in optimal reduction of #lambda#-terms (or, more generally, of functional programs). The very story started, in fact, more than twenty years ago, with Jean-Jacques Levy's thesis [Lev78]. The problem he attacked was to find an execution strategy for #lambda#-terms minimizing the number of #beta#-reductions. It was already known that no such strategy exists which reduces only one redex (i.e., a single function call) at the time. Levy's insight was to discover that a parallel optimal strategy exists, the one reducing in a single step all the redexes belonging to the same family, a crucial notion he introduced. However, Levy lacked the programming technology to implement his strategy. He showed it was effective, but no one knew at that time what kind of data structure could be used to dynamically maintain the families in such a way that all the redexes of a given family could be somehow shared and, therefore, reduced as a single step. The solution came in 1989, when independently Kathail [Kat90] and Lamping [Lam90] gave abstract #lambda#-calculus machines which reduced terms as prescribed by Levy's optimality theory. Lamping's graph rewriting approach is the one that received most interest, and after his breakthrough other variants of optimal reducers have been proposed, especially by Gonthier, Abadi and Levy [GnAl92a] and Asperti [Asp95]. We will refer to all of them as the optimal sharing graph approach.
展开▼
