在 lambda 演算中按值调用

Posted 2023-05-08

【中文标题】在 lambda 演算中按值调用

【英文标题】：Call by value in the lambda calculus

【发布时间】：2011-09-04 08:24:26

【问题描述】：

我正在研究Types and Programming Languages，而 Pierce，对于按价值减少策略的调用，给出了术语 id (id (λz. id z)) 的示例。内部 redex id (λz. id z) 首先减少到 λz. id z，在外部 redex 减少到正常形式 λz. id z 之前，第一次减少的结果是 id (λz. id z)。

但是按值顺序调用被定义为“仅减少最外层的redex”，并且“仅当redex 的右侧已经减少为一个值时才减少redex”。在示例中，id (λz. id z) 出现在最外层 redex 的右侧，并且被缩小。这与仅减少最外层redexes 的规则有何关系？

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

【参考方案1】：

简短的回答：是的。你永远不能在 lambda 项内归约，你只能在外面归约，从右开始。

lambda-calculus by value 中的评估上下文集定义如下：

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

E 是你能看重的。

例如，在 lambda 演算中，计算上下文是：

E = [ ] | Et | fE

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

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

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

【讨论】：

一个更简单的例子是 (λx.x)(x)，因为右侧无法进一步评估，所以它被卡在按值调用中。

【参考方案2】：

“最外层”和“最内层”的答案是否仅指 lambda 抽象？所以对于 λz 中的项 t。 t, t 不能减少，但是在 redex s t 中，如果可能的话，t 减少到一个值 v，然后 s v 减少？

是的，完全正确。