eCommons

 

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

Other Titles

Abstract

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

Description

Sponsorship

Date Issued

1990-02

Publisher

Cornell University

Keywords

computer science; technical report

Location

Effective Date

Expiration Date

Sector

Employer

Union

Union Local

NAICS

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)

References

Link(s) to Reference(s)

Previously Published As

http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR90-1091

Government Document

ISBN

ISMN

ISSN

Other Identifiers

Rights

Rights URI

Types

technical report

Accessibility Feature

Accessibility Hazard

Accessibility Summary

Link(s) to Catalog Record