Thunks and the tex2html_wrap_inline31-Calculus (Extended Version)

John Hatcliff
Olivier Danvy

March 1997


Plotkin, in his seminal article Call-by-name, call-by-value and the tex2html_wrap_inline31-calculus, formalized evaluation strategies and simulations using operational semantics and continuations. In particular, he showed how call-by-name evaluation could be simulated under call-by-value evaluation and vice versa. Since Algol 60, however, call-by-name is both implemented and simulated with thunks rather than with continuations. We recast this folk theorem in Plotkin's setting, and show that thunks, even though they are simpler than continuations, are sufficient for establishing all the correctness properties of Plotkin's call-by-name simulation.

Furthermore, we establish a new relationship between Plotkin's two continuation-based simulations tex2html_wrap_inline35 and tex2html_wrap_inline37, by deriving tex2html_wrap_inline35 as the composition of our thunk-based simulation tex2html_wrap_inline41 and of tex2html_wrap_inline43 -- an extension of tex2html_wrap_inline37 handling thunks. Almost all of the correctness properties of tex2html_wrap_inline35 follow from the properties of tex2html_wrap_inline41 and tex2html_wrap_inline37. This simplifies reasoning about call-by-name continuation-passing style.

We also give several applications involving factoring continuation-based transformations using thunks

Available as PostScript, PDF, DVI.


Last modified: 2003-06-08 by webmaster.