Call-by-Need, Neededness and All That

TL;DR

This paper demonstrates that call-by-need evaluation is equivalent to weak-head needed reduction, using a novel intersection type system to semantically characterize and syntactically identify needed redexes.

Contribution

It establishes the equivalence between call-by-need and weak-head needed reduction through a semantical proof and introduces a type system that identifies needed redexes.

Findings

Call-by-need and weak-head needed reduction are observationally equivalent.

The type system $ ext{V}$ semantically characterizes needed redexes.

The system $ ext{V}$ syntactically identifies all weak-head needed redexes.

Abstract

We show that call-by-need is observationally equivalent to weak-head needed reduction. The proof of this result uses a semantical argument based on a (non-idempotent) intersection type system called $\mathcal{V}$. Interestingly, system $\mathcal{V}$ also allows to syntactically identify all the weak-head needed redexes of a term.