On Laziness and Optimality in Lambda Interpreters: Tools for Specification and Analysis

Other Titles


In this paper, we introduce a new formal system, ΛCCL, based on Curien's Categorical Combinators [Cur86a]. We show that ΛCCL has properties that make it especially suitable for analysis and implementation of a wide range of λ-reduction schemes using shared environments, closures, or λ-terms. In particular, the term structure of \LamdaCCL is very closely related to the structure of existing abstract machines for λ-reduction. ΛCCL is powerful enough to mimic arbitrary (strong) reduction in the λ-calculus, yet in contrast to the systems in [Cur86a] it is also confluent (on ground terms).As an example of the practical utility of this formalism, we use it to specify a simple lazy interpreter for the λ-calculus, whose correctness follows trivially from the properties of \LambdaCCL. We then describe a labeled variant of ΛCCL,ΛCCLL, which can be used as a tool to determine the degree of "laziness" possessed by various λ-reduction schemes. In particular, ΛCCLL is applied to the problem of optimal reduction in the λ-calculus. A reduction scheme for the λ-calculus is optimal if the number of redex contractions that must be performed in the course of reducing any λ-term to a normal form (if one exists) is guaranteed to be minimal. Results of Levy [Lev78, Lev80] showed that for a natural class of reduction strategies allowing shared redexes, optimal reductions were, at least in principle, possible. He conjectured that an optimal reduction strategy might be realized in practice using shared closures and environments as well as shared λ-terms. However, using ΛCCLL, we show that the sharing allowed by environments and closures in ΛCCL as implemented using standard term graph-rewriting techniques [BvEG$^{+}$87] is insufficient to implement optimal reduction.

Journal / Series

Volume & Issue



Date Issued



Cornell University


computer science; technical report


Effective Date

Expiration Date




Union Local


Number of Workers

Committee Chair

Committee Co-Chair

Committee Member

Degree Discipline

Degree Name

Degree Level

Related Version

Related DOI

Related To

Related Part

Based on Related Item

Has Other Format(s)

Part of Related Item

Related To

Related Publication(s)

Link(s) to Related Publication(s)


Link(s) to Reference(s)

Previously Published As

Government Document




Other Identifiers


Rights URI


technical report

Accessibility Feature

Accessibility Hazard

Accessibility Summary

Link(s) to Catalog Record