No-Brainer CPS conversion (Functional pearl)

Abstract

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.