On inter-deriving small-step and big-step semantics: A case study for storeless call-by-need evaluation
Venue
Theoretical Computer Science, vol. 435 (2012), pp. 21-42
Publication Year
2012
Authors
Olivier Danvy, Kevin Millikin, Johan Munk, Ian Zerny
BibTeX
Abstract
Starting from the standard call-by-need reduction for the λ-calculus that is common
to Ariola, Felleisen, Maraist, Odersky, and Wadler, we inter-derive a series of
hygienic semantic artifacts: a reduction-free storeless abstract machine, a
continuation-passing evaluation function, and what appears to be the first heapless
natural semantics for call-by-need evaluation. Furthermore we observe that the
evaluation function implementing this natural semantics is in defunctionalized
form. The refunctionalized counterpart of this evaluation function implements an
extended direct semantics in the sense of Cartwright and Felleisen. Overall, the
semantic artifacts presented here are simpler than many other such artifacts that
have been independently worked out, and which require ingenuity, skill, and
independent soundness proofs on a case-by-case basis. They are also simpler to
inter-derive because the inter-derivational tools (e.g., refocusing and
defunctionalization) already exist.
