lambda-calculus - 在 lambda 演算中按值调用

Question

我正在努力解决 Types and Programming Languages和皮尔斯，对于减值策略的调用，给出了术语 id (id (λz. id z)) 的例子。 .内部 redex id (λz. id z)减少到 λz. id z首先，给id (λz. id z)作为第一次减少的结果，在外部 redex 减少到正常形式之前 λz. id z .

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

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

Answer 1

简短的回答:是的。你永远不能在 lambda 项内减少，你只能在外部减少项，从右边开始。

lambda 演算中的一组求值上下文按值定义如下:

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 章中看到上下文的另一个定义。