一句话：提出轻量级归纳方法，为传值调用可被传名调用模拟这一经典定理给出简单证明。
该论文研究操作语义中急切求值与惰性求值的关系。在 λ 演算中，经典结论是：一个程序按传值调用求值到弱头正规形式的过程，总可由传名调用求值模拟。该结论直观但朴素证明常失败，通常需借助更复杂的标准化定理。作者提出一种新颖而轻量的归纳方法，用于证明同一演算、不同求值顺序的两种语义之间的模拟关系，并在传值调用与传名调用这一经典例子上加以实现和形式化。文章报告了该方法带来的方法论启示，尤其讨论了所选语义风格对证明的影响。
Abstract One of the natural problems of operational semantics is to characterise the relationship between eager and lazy evaluation. In the context of $\lambda$ -calculus, this is expressed by the classic theorem that call-by-value evaluation of a program to (weak-head) normal form can always be simulated by a call-by-name evaluation. While the statement and intuition behind it are simple and clear, naive attempts at proof famously fail: the result is usually established as a consequence of the more complex standardisation theorem. In this work, we develop and formalise a novel and lightweight inductive approach to tackle the problem of simulation between two semantics for a single calculus, but with different evaluation orders. We exercise our method on the classic call-by-value and call-by-name example and report on methodological takeaways suggested by our approach, in particular what effect the flavour of semantics chosen has on the proof.
@article{BiernackiMS25,
title = {Call-by-value and call-by-name: A simple proof of a classic theorem},
author = {DARIUSZ BIERNACKI and JAMES MCKINNA and FILIP SIECZKOWSKI},
journal = {Journal of Functional Programming},
volume = {35},
year = {2025},
doi = {10.1017/s0956796825100038}
}