Search code examples
schemecontinuationslanguage-theorycontinuation-passing

What exactly are administrative redexes after CPS conversion?

In the context of Scheme and CPS conversion, I'm having a little trouble deciding what administrative redexes (lambdas) exactly are:

  • all the lambda expressions that are introduced by the CPS conversion
  • only the lambda expressions that are introduced by the CPS conversion but you wouldn't have written if you did the conversion "by hand" or through a smarter CPS-converter

If possible, a good reference would be welcome.

Solution

  • Redex stands for "reducible expression", which is an expression that isn't a value. Therefore, a lambda is not a redex, but a call is.
    In CPS, an administrative redex is a redex whose operator is a continuation lambda. Such redexes can be reduced immediately because you know which function you are calling.
    For example, ((lambda (u) ...) foo) is an administrative redex, but (k foo) isn't.