Call-By-Name Is Just Call-By-Value with Delimited Control

Delimited control operator shift0 exhibits versatile capabilities: it can express layered monadic effects, or equivalently, algebraic effects. Little did we know it can express lambda calculus too! We present ${\mathrm{\Lambda }}_{\mathrm{\$}}$, a call-by-value lambda calculus extended with shift0 and control delimiter $\mathrm{\$}$ with carefully crafted reduction theory, such that the lambda calculus with beta and eta reductions can be isomorphically embedded into ${\mathrm{\Lambda }}_{\mathrm{\$}}$ via a right inverse of a continuation-passing style translation. While call-by-name reductions of lambda calculus can trivially simulate its call-by-value version, we show that addition of shift0 and $\mathrm{\$}$ is the golden mean of expressive power that suffices to simulate beta and eta reductions while still admitting a simulation back. As a corollary, calculi $\mathrm{\Lambda }{\mu }_v$, ${\lambda }_{\mathrm{\$}}$, ${\mathrm{\Lambda }}_{\mathrm{\$}}$ and $\lambda$ all correspond equationally.