First Class Call Stacks: Exploring Head Reduction

TL;DR

This paper investigates head reduction in the call-by-name lambda calculus, proposing new operational semantics and abstract machines to reconcile extensionality with effects, improving implementation while maintaining theoretical consistency.

Contribution

It introduces alternative operational semantics and abstract machines for head reduction that address extensionality issues in call-by-name lambda calculus.

Findings

Head reduction avoids extensionality problems.

Operational semantics enable easier implementation.

Abstract machines demonstrate practical head reduction methods.

Abstract

Weak-head normalization is inconsistent with functional extensionality in the call-by-name $\lambda$-calculus. We explore this problem from a new angle via the conflict between extensionality and effects. Leveraging ideas from work on the $\lambda$-calculus with control, we derive and justify alternative operational semantics and a sequence of abstract machines for performing head reduction. Head reduction avoids the problems with weak-head reduction and extensionality, while our operational semantics and associated abstract machines show us how to retain weak-head reduction's ease of implementation.