Call-by-value and call-by-name: A simple proof of a classic theorem

Abstract

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.