YALE

Abstract

Interaction nets provide a graphical paradigm of computation based on net rewriting. They have proved most successful in understanding the dynamics of reduction in the λ-calculus, where the prime example is the implementation of optimal reduction for the λ-calculus (Lamping's algorithm), given by Gonthier, Abadi and Lévy. However, efficient implementations of optimal reduction have had to break away from the interaction net paradigm. In this paper we give a new efficient interaction net encoding of the λ-calculus which is not optimal, but overcomes the inefficiencies caused by the bookkeeping operations in the implementations of optimal reduction. We believe that this implementation of the λ-calculus could provide the basis for highly efficient implementations of functional languages.