CPS 转换后的管理 redexe 到底是什么?

发布于 2024-08-18 21:22:09 字数 378 浏览 16 评论 0原文

在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 技术交流群。

扫码二维码加入Web技术交流群

发布评论

需要 登录 才能够评论, 你可以免费 注册 一个本站的账号。

评论(2

临风闻羌笛 2024-08-25 21:22:09

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.

ぺ禁宫浮华殁 2024-08-25 21:22:09

我想我找到了答案。
编辑:我已经接受了 dimvar 的答案,它更短、更正确。)

假设输入程序不完全是 CPS,则至少有一个过程返回点必须由 CPS 转换为延续转换。因此,这个延续是通过必要的转换引入的。因为这是必要的,所以您总是需要这样做,例如在手动转换时也是如此。因此,管理 redexe 只是 CPS 转换引入的那些并非真正必要的 lambda(我的第二个定义)。

我找到了一篇 论文 解释如下(强调我的):

将简单的 λ 编码到 CPS 中,
然而,产生了一个相当令人印象深刻的
lambda 的膨胀,其中大部分
形成管理 Redex,可以
可以安全地减少。行政
减少产量 CPS 条款
对应于一个人可以写的内容
手工。因此它成为了一个
挑战消除尽可能多的
尽可能进行行政复述,
CPS-转换时间。

不过,当然欢迎任何评论或建议。

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.

~没有更多了~
我们使用 Cookies 和其他技术来定制您的体验包括您的登录状态等。通过阅读我们的 隐私政策 了解更多相关信息。 单击 接受 或继续使用网站,即表示您同意使用 Cookies 和您的相关数据。
原文