|
A Higher-Order Colon Translation
Olivier Danvy
December 2000 |
Abstract:
A lambda-encoding such as the CPS transformation gives rise to
administrative redexes. In his seminal article ``Call-by-name, call-by-value
and the lambda-calculus'', 25 years ago, Plotkin tackled administrative
reductions using a so-called ``colon translation.'' 10 years ago, Danvy and
Filinski integrated administrative reductions in the CPS transformation,
making it operate in one pass. The technique applies to other
lambda-encodings (e.g., variants of CPS), but we do not see it used in
practice--instead, Plotkin's colon translation appears to be favored.
Therefore, in an attempt to link both techniques, we recast Plotkin's proof
of Indifference and Simulation to the higher-order specification of the
one-pass CPS transformation. To this end, we extend his colon translation
from first order to higher order
Available as PostScript, PDF, DVI. |