一句话：在良构、统一策略与平衡混合策略条件下，证明 eval-readback 与 eval-apply 大步求值器一步等价，并厘清 λ 演算策略空间。
论文研究纯 λ 演算中 eval-readback 与 eval-apply 两类大步求值器的等价性，区分同策略的一步等价与同最终结果的大步等价。作者给出一步等价成立的条件：readback 满足良构约束，eval 实现 uniform 策略，且 eval-apply 实现以 eval 为子策略的 balanced hybrid 策略；证明借助 lightweight fusion by fixed-point promotion 将 readback 与 eval 融合为 balanced hybrid。实现使用 Haskell 2010 的 monadic 风格以保证策略保持。论文还改进 uniform/hybrid 策略定义，结构化策略空间，综述自然操作语义下的典型求值器及其抽象机，并引入统一记号总结策略与求值器等价关系。
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.
@article{paperbot2698,
title = {Equivalence of eval-readback and eval-apply big-step evaluators by structuring the lambda-calculus's strategy space},
author = {Pablo Nogueira and Álvaro García-Pérez},
journal = {Logical Methods in Computer Science},
volume = {Volume 20, Issue 4},
year = {2024},
doi = {10.46298/lmcs-20(4:24)2024}
}