Reduction Strategies in the Lambda Calculus and Their Implementation through Derivable Abstract Machines: Introduction

TL;DR

This paper introduces new abstract machines for evaluating lambda calculus expressions using various reduction strategies, including strong call-by-value and call-by-need, with efficiency analyses and systematic surveys.

Contribution

It systematically surveys lambda calculus reduction strategies and derives, improves, and analyzes abstract machines for strong call-by-value and call-by-need evaluation.

Findings

Derived an abstract machine for strong call-by-value

Improved the machine for efficiency with time complexity analysis

Presented the first provably efficient machine for strong call-by-need

Abstract

The lambda calculus since more than half a century is a model and foundation of functional programming languages. However, lambda expressions can be evaluated with different reduction strategies and thus, there is no fixed cost model nor one canonical implementation for all applications of the lambda calculus. This article is an introduction to a dissertation is composed of four conference papers where: we present a systematic survey of reduction strategies of the lambda calculus; we take advantage of the functional correspondence as a tool for studying implementations of the lambda calculus by deriving an abstract machine for a precisely identified strong call-by-value reduction strategy; we improve it to obtain an efficient abstract machine for strong call by value and provide a time complexity analysis for the new machine with the use of a potential function; and we present the first provably efficient abstract machine for strong call by need.