论文标题
通过构建Lambda-Calculus的策略空间，评估式读书和评估的大型评估者的等效性
Equivalence of eval-readback and eval-apply big-step evaluators by structuring the lambda-calculus's strategy space
论文作者
论文摘要
我们研究了纯lambda演算的一般环境中评估读取和评估的大步评估者之间的等价性。我们研究“一步”等效性（相同的策略），并讨论“大步”等效性（相同的最终结果）。一步等效性通过限制术语（闭合，收敛），同时维护策略，以在其他设置（计算，编程语言，证明助手等）中自由扩展到评估者。我们提供了一个证明，即（1）（1）“回回式阶段”满足直接良好形式的规定，（2）“ eval”阶段实现“统一”策略，以及（3）评估评估者实现“平衡的混合”策略，该策略具有“评估”作为子公司策略。该证明在评估者实现上进行了“通过定点促销的轻量级融合”计划转换，以融合回顾并评估平衡的混合动力。可以遵循证据，没有以前对转换的了解。我们将Haskell 2010用作实施语言，所有评估者都以单声学风格编写，以保证语义（策略）保存，但是实施语言的选择是无关紧要的。为了说明等效性的巨大范围，我们使用规范评估评估者在代码和大步骤“自然”操作语义上提供了对战略空间的广泛调查。我们讨论了策略的特性，它们的某些用途及其抽象机器。我们改善了对统一和混合策略的形式定义，使用它来构建策略空间，并获得在等价证明中使用的通用高阶评估者。我们介绍了两种评估者样式的系统符号，并使用它来总结策略和评估者等价，包括样式内（非）等价的（非）等价，以及未经转换证明的样式之间的（非）等价。
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.
