通过结构化λ演算的策略空间，证明eval-readback与eval-apply大步求值器的等价性
Equivalence of eval-readback and eval-apply big-step evaluators by structuring the lambda-calculus's strategy space
AI总结：
本文通过结构化λ演算策略空间，证明在特定条件下eval-readback与eval-apply大步求值器的一步等价性，并系统调查策略空间。
摘要：
我们在纯λ演算的一般设置下研究eval-readback与eval-apply大步求值器之间的等价性。我们研究“一步”等价性（相同策略），并讨论“大步”等价性（相同最终结果）。一步等价性通过限制项（封闭、收敛）同时保持策略，可免费扩展到其他设置（演算、编程语言、证明助手等）中的求值器。我们给出一个证明，证明当（1）“readback”阶段满足简单的良构性条件，（2）“eval”阶段实现“统一”策略，且（3）eval-apply求值器实现“平衡混合”策略且以“eval”作为辅助策略时，一步等价性成立。该证明通过对求值器实现进行“通过不动点提升的轻量级融合”程序变换，将readback和eval融合为平衡混合。该证明无需预先了解该变换即可理解。我们使用Haskell 2010作为实现语言，所有求值器均以单子风格编写以保证语义（策略）保持，但实现语言的选择无关紧要。为了说明等价性的广泛适用范围，我们使用代码中的规范eval-apply求值器和大步“自然”操作语义对策略空间进行了广泛调查。我们讨论策略的性质、它们的一些用途及其抽象机。我们改进了统一和混合策略的形式定义，用它来结构化策略空间，并获得用于等价性证明的通用高阶求值器。我们为两种求值器风格引入系统化记号，并用它来总结策略和求值器的等价性，包括风格内的（非）等价性以及变换未证明的风格间的（非）等价性。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
