我正在研究Types and Programming Languages，而 Pierce 对于按值减少策略的调用，给出了 term 的例子id (id (λz. id z))。内部 redexid (λz. id z)被归约为λz. id zfirst，id (λz. id z)作为第一次归约的结果，在外部 redex 归约为正常形式之前λz. id z。
但是按值顺序调用被定义为“仅减少最外层的redex”，并且“仅当redex 的右侧已经减少为一个值时才减少redex”。在示例id (λz. id z)中出现在最外层 redex 的右侧，并且被缩减。这与仅减少最外层redexes的规则有何关系？
“最外层”和“最里面”的答案是否仅指 lambda 抽象？所以对于 in 中的一个术语t，λz. t不能t减少，但是在 redexs t中，如果可能的话，t减少到一个值v，然后s v减少？
简短的回答：是的。你永远不能在 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 章看到上下文的另一个定义。
“最外层”和“最里面”的答案是否仅指 lambda 抽象？所以对于 λz 中的项 t。t, t 不能减少，但是在 redex st 中，如果可能的话，t 会减少到值 v，然后 sv 会减少？
是的，完全正确。