In the context of Scheme and CPS conversion, I'm having a little trouble deciding what administrative redexes (lambdas) exactly are:
If possible, a good reference would be welcome.
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.
I think I found my answer. (Edit: I have accepted dimvar's answer instead, it's shorter and more correct.)
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.
© 2022 - 2024 — McMap. All rights reserved.
