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

I think I found my answer.

Assuming the input program is not fully CPS, at least one procedure return point will have to be converted into a continuation by the CPS conversion. So this continuation is both introduced by the conversion and necessary. Because it is necessary, you would always need to do this, also when converting by hand for example. Therefore, administrative redexes are only those lambdas introduced by the CPS conversion that aren't really necessary (my second definition).

I found a paper that explains it like this (emphasis mine):

The naîve λ-encoding into CPS, however, generates a quite impressive inflation of lambdas, most of which form administrative redexes that can be safely reduced. Administrative reductions yield CPS terms corresponding to what one could write by hand. It has therefore become a challenge to eliminate as many administrative redexes as possible, at CPS-transformation time.

Still, any remarks or suggestions welcome of course.

Answer 2

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.