CPS 转换后的管理 redexe 到底是什么?
在Scheme和CPS转换的背景下,我在决定什么方面遇到了一些麻烦管理redexes(lambda)正是:
- 所有由 CPS 转换引入
- 仅由 CPS 转换引入的 lambda 表达式,但如果您“手动”或通过更智能的 CPS 转换器进行转换,则您不会编写
如果可能的话,欢迎提供良好的参考。
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.
如果你对这篇内容有疑问,欢迎到本站社区发帖提问 参与讨论,获取更多帮助,或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱,如果其他用户或者作者回复了您的评论,将不能在第一时间通知您!
发布评论
评论(2)
Redex 代表“可约表达式”,它是一个不是值的表达式。因此,lambda 不是 redex,而是调用。
在 CPS 中,管理 Redex 是其运算符为延续 lambda 的 Redex。这样的 redexes 可以立即减少,因为你知道你正在调用哪个函数。
例如,
((lambda (u) ...) foo)
是管理性 Redex,但(k foo)
不是。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.我想我找到了答案。
(编辑:我已经接受了 dimvar 的答案,它更短、更正确。)
假设输入程序不完全是 CPS,则至少有一个过程返回点必须由 CPS 转换为延续转换。因此,这个延续是通过必要的转换和引入的。因为这是必要的,所以您总是需要这样做,例如在手动转换时也是如此。因此,管理 redexe 只是 CPS 转换引入的那些并非真正必要的 lambda(我的第二个定义)。
我找到了一篇 论文 解释如下(强调我的):
不过,当然欢迎任何评论或建议。
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):
Still, any remarks or suggestions welcome of course.