Continuations are variously understood as representations of the current evaluation context and as representations of the rest of the computation, but these understandings contradict each other: plug ging an expression in a context yields a new expression whereas sending an intermediate result to a continuation yields the final an swer. We show that continuationsasevaluationcontexts are the defunctionalized representation of the continuation of a single step reduction function and that continuationsastherestofthe computation are the continuation of an evaluation function. Fur thermore, we show that defunctionalizing the continuation of an evaluator gives rise to the same evaluation contexts as in the single step reducer. The only difference is how these evaluation contexts are interpreted: a ‘plug’ interpretation yields onestep reduction, whereas a ‘refocus’ interpretation yields evaluation. We then present a constructive corollary of Reynolds’s histor ical warning about depending on the evaluation order of a meta language for an interpreter: The two bestknown abstract machines for the calculus, Krivine’s machine and Felleisen et al.’s CEK machine, are in fact the callbyname and callbyvalue counter parts of the same (evaluationorder dependent) interpreter for the
【 预 览 】
附件列表
Files
Size
Format
View
On Evaluation Contexts, Continuations, and the Rest of the Computation