Equivalence of eval-readback and eval-apply big-step evaluators by structuring the lambda-calculus's strategy space

TL;DR

This paper develops a unified framework to compare two big-step evaluator styles for the pure lambda calculus: eval-readback and eval-apply. It proves a one-step equivalence between them via a lightweight fusion by fixed-point promotion ($LWF$) under well-formedness provisos, yielding a balanced hybrid eval-apply evaluator with a modular proof that can be instantiated for canonical strategies. It also refines the conceptual landscape by introducing uniform/hybrid and balanced-hybrid notions, provides generic templates for evaluators, and surveys a wide strategy space with systematic notation and equivalence results. The work clarifies when an eval-readback evaluator can be faithfully transformed into an eval-apply form, and vice versa, with implications for abstraction, compiler optimisations, and the design of interpreters and proof assistants in a principled way. It demonstrates that equivalence results extend beyond the pure calculus to restricted term classes and varied languages, highlighting the practical impact on correctness-preserving translator mechanisms between semantic devices.

Abstract

We study the equivalence between eval-readback and eval-apply big-step evaluators in the general setting of the pure lambda calculus. We study `one-step' equivalence (same strategy) and also discuss `big-step' equivalence (same final result). One-step equivalence extends for free to evaluators in other settings (calculi, programming languages, proof assistants, etc.) by restricting the terms (closed, convergent) while maintaining the strategy. We present a proof that one-step equivalence holds when (1) the `readback' stage satisfies straightforward well-formedness provisos, (2) the `eval' stage implements a `uniform' strategy, and (3) the eval-apply evaluator implements a `balanced hybrid' strategy that has `eval' as a subsidiary strategy. The proof proceeds the `lightweight fusion by fixed-point promotion' program transformation on evaluator implementations to fuse readback and eval into the balanced hybrid. The proof can be followed with no previous knowledge of the transformation. We use Haskell 2010 as the implementation language, with all evaluators written in monadic style to guarantee semantics (strategy) preservation, but the choice of implementation language is immaterial. To illustrate the large scope of the equivalence, we provide an extensive survey of the strategy space using canonical eval-apply evaluators in code and big-step `natural' operational semantics. We discuss the strategies' properties, some of their uses, and their abstract machines. We improve the formal definition of uniform and hybrid strategy, use it to structure the strategy space, and to obtain generic higher-order evaluators which are used in the equivalence proof. We introduce a systematic notation for both evaluator styles and use it to summarise strategy and evaluator equivalences, including (non-)equivalences within a style and (non-)equivalences between styles not proven by the transformation.

Figures (1)

• Figure 1: Main sets of terms in Extended BNF where $\{\mathsf{X}\}^*$ denotes zero or more occurrences of non-terminal $\mathsf{X}$, that is, $\mathsf{X}_1 \cdots \mathsf{X}_n$ with $n\geq0$.