在lambda演算中按值调用 [英] Call by value in the lambda calculus

问题描述

我正在通过类型和编程语言以及皮尔斯(Pierce)对于按值减少策略进行调用，给出了术语id (id (λz. id z))的示例.首先将内部redex id (λz. id z)还原为λz. id z，作为第一次还原的结果为id (λz. id z)，然后将外部redex还原为正常形式λz. id z.

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.

但是按值顺序调用被定义为仅减少最外面的redex"，和仅当其右手侧已减小为值时才减少redex".在示例中，id (λz. id z)出现在最外面的redex的右侧，并被缩小.这与仅减少最外部的redex的规则如何平方?

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?

答案是最外层"和最内层"仅是指lambda抽象吗?因此，对于λz. t中的术语t，不能将t还原，但是在redex s t中，如果可能，将t还原为值v，然后再将s v减少了?

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?

推荐答案

简短的回答:是的.您永远不能在lambda项之内减少，而只能在正确的地方减少外部的项.

Short answer: yes. You can never reduce inside a lambda-term you can only reduce term outside, starting by right.

lambda演算中按值定义的评估上下文的集合定义如下:

The set of evaluation contexts in lambda-calculus by value is defined as follow:

E = [ ] | (λ.t)E | Et

E是您可以重视的.

例如，按名称命名为lambda演算，评估上下文为:

For example in lambda calculus by name the evaluation context is :

E = [ ] | Et | fE

因为您可以简化应用程序，即使术语不是值. 例如，(λx.x)(z λx.x)卡在按值调用中，但按名称调用时，它减少为(z λx.x)，这是正常形式.
在上下文中，语法f是一种普通形式(按名称调用)，定义为:

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 f is a normal form (in call by name) defined as:

f = λx.t | L  
L = x | L f

您可以在Pierce的第19.5.3章中看到上下文的另一种定义.

You can see another definition of contexts at chapter 19.5.3 of the Pierce.

这篇关于在lambda演算中按值调用的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！