开发者

What exactly are administrative redexes after CPS conversion?

开发者 https://www.devze.com 2022-12-17 17:11 出处:网络
In the context of Scheme and CPS conversion, I\'m having a little trouble deciding what administrative redexes (lambdas) exactly are:

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开发者_JAVA技巧

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.

0

精彩评论

暂无评论...
验证码 换一张
取 消