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{paperbot3321,
  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}
}