一句话：提出线性时间 CPS 转换算法，不引入行政归约项，输出在 no-brainer 归约系统下即为范式。
传统上将直接风格（direct-style）λ-calculus 项转换为 continuation-passing style（CPS）的算法通常会引入“行政归约项”（administrative redexes），必须再经过一趟清理。本文提出一个简单且线性的时间 CPS 转换算法，完全不引入行政归约项。其输出项在一个更广的归约系统中已处于范式；该系统把行政归约项推广为“no-brainer redexes”，即归约后项的大小会缩小的归约项。作者陈述了刻画该算法理想性质的一系列定理，并给出完整证明的思路。作为 functional pearl，工作侧重算法与理论证明，而非实验评估。
Algorithms that convert direct-style λ-calculus terms to their equivalent terms in continuation-passing style (CPS) typically introduce so-called “administrative redexes:” useless artifacts of the conversion that must be cleaned up by a subsequent pass over the result to reduce them away. We present a simple, linear-time algorithm for CPS conversion that introduces no administrative redexes. In fact, the output term is a normal form in a reduction system that generalizes the notion of “administrative redexes” to what we call “no-brainer redexes,” that is, redexes whose reduction shrinks the size of the term. We state the theorems which establish the algorithm's desireable properties, along with sketches of the full proofs.
@article{DavisMS17,
title = {No-brainer CPS conversion (functional pearl)},
author = {Milo Davis and William Meehan and Olin Shivers},
journal = {Proceedings of the ACM on Programming Languages},
volume = {1},
number = {ICFP},
year = {2017},
doi = {10.1145/3110267}
}