LISP and Symbolic Computation, 6(3/4)289-360
Reasoning about Programs in Continuation-Passing StyleAmr Sabry, Department of Computer Science, Rice University, Houston, TX 77251-1892
Matthias Felleisen, Department of Computer Science, Rice University, Houston, TX 77251-1892
|
Abstract: Plotkin's lambda-v-calculus for call-by-value
programs is weaker than the lambda-beta-eta-calculus for the same
programs in continuation-passing style (CPS). To identify the
call-by-value axioms that correspond to beta-eta on CPS terms, we
define a new CPS transformation and an inverse mapping, both of which
are interesting in their own right. Using the new CPS transformation,
we determine the precise language of CPS terms closed under
beta-eta-transformations, as well as the call-by-value axioms that
correspond to the so-called administrative beta-eta-reductions on CPS
terms. Using the inverse mapping, we map the remaining beta and eta
equalities on CPS terms to axioms on call-by-value terms. On the pure
(constant free) set of 3-terms, the resulting set of axioms is
equivalent to Moggi's computational lambda-calculus. If the
call-by-value language includes the control operators abort and
call-with-current-continuation, the axioms are equivalent to an
extension of Felleisen et al.'s lambda-v-C-calculus and to the
equational subtheory of Talcott's logic IOCC. Keywords: lambda-calculus, lambda-v-calculus, continuation-passing style, CPS transformations, inverse CPS transformations, lambda-v-C-calculus, IOCC |
[local copy]