lambda 演算中的按值调用
我正在研究类型和编程语言，以及 Pierce，用于按值缩减策略调用，给出术语id(id(λz.id z))的示例。内部 redex id (λz.id z) 被简化为 λz.id z。首先，将 。id (λz.id z) 作为第一次归约的结果，然后将外部 redex 归约到正常形式 λz.id z。 id z
但是按值顺序调用被定义为“仅减少最外层的 Redex”，并且“仅当 Redex 的右侧已减少为某个值时才减少 Redex”。在示例中，id (λz.id z) 出现在最外层 Redex 的右侧，并被缩减。这与仅减少最外层氧化还原的规则有何关系？
答案是“最外层”和“最内层”仅指 lambda 抽象吗？因此对于λz 中的项、t。 tt 无法减少，但在 redex s t 中，t 会减少为值 v 如果这是可能的，那么 s v 会减少吗？
I'm working my way through Types and Programming Languages, and Pierce, for the call by value reduction strategy, gives the example of the term id (id (λz. id z)). The inner redex id (λz. id z) is reduced to λz. id z first, giving id (λz. id z) as the result of the first reduction, before the outer redex is reduced to the normal form λz. id z.
But call by value order is defined as 'only outermost redexes are reduced', and 'a redex is reduced only when its right-hand side has already been reduced to a value'. In the example id (λz. id z) appears on the right-hand side of the outermost redex, and is reduced. How is this squared with the rule that only outermost redexes are reduced?
Is the answer that 'outermost' and 'innermost' only refers to lambda abstractions? So for a term t in λz. t, t can't be reduced, but in a redex s t, t is reduced to a value v if this is possible, and then s v is reduced?
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（2）
简短的回答：是的。你永远不能减少 lambda 项的内部，你只能减少外部的项，从右边开始。
按值 lambda 演算中的求值上下文集定义如下：
E 是您可以计算的值。
例如，在按名称 lambda 演算中，求值上下文是：
即使术语不是值，您也可以减少应用程序。
例如，
(λx.x)(z λx.x)被困在按值调用中，但在按名称调用中它会减少为(z λx.x)，即正常形式。在上下文语法中，
f是一种范式（按名称调用），定义为：您可以在 Pierce 的第 19.5.3 章中看到上下文的另一个定义。
Short answer: yes. You can never reduce inside a lambda-term you can only reduce term outside, starting by right.
The set of evaluation contexts in lambda-calculus by value is defined as follow:
E is what you can value..
For example in lambda calculus by name the evaluation context is :
as you can reduce an application even if a term is not a value.
For example
(λx.x)(z λx.x)is stuck in call by value but in call by name it reduce to(z λx.x), which is a normal form.In the context grammar
fis a normal form (in call by name) defined as:You can see another definition of contexts at chapter 19.5.3 of the Pierce.
是的，完全正确。
Yes, that's exactly right.