What exactly are administrative redexes after CPS conversion?

Question

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.

Answer 1

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.