Вызов по значению в исчислении лямбда

Я прокладываю себе путь через Типы и языки программирования, а Пирс - для стратегии снижения стоимости вызова, дает пример term id (id (λz. id z)). Внутреннее redex id (λz. id z) сначала сводится к λz. id z, давая id (λz. id z) в результате первой редукции до того, как внешнее redex приводится к нормальной форме λz. id z.

Но вызов по порядку значений определяется как "только внешние удаленные редексы уменьшены", а "redex уменьшается только тогда, когда его правая сторона уже сведена к значению". В примере id (λz. id z) появляется в правой части внешнего redex и уменьшается. Как это связано с правилом, которое уменьшает только самые внешние редексы?

Является ли ответ, что "внешний" и "самый внутренний" относится только к лямбда-абстракциям? Итак, для термина t в λz. t, t не может быть уменьшено, но в redex s t, t сводится к значению v, если это возможно, а затем s v сокращается?

Ответ 1

Короткий ответ: да. Вы никогда не сможете уменьшить внутри лямбда-термина, вы можете сократить время снаружи, начиная с права.

Набор контекстов оценки в лямбда-исчислении по значению определяется следующим образом:

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

E - это то, что вы можете оценить.

Например, в лямбда-исчислении по названию контекст оценки:

E = [ ] | Et | fE

поскольку вы можете уменьшить приложение, даже если термин не является значением. Например, (λx.x)(z λx.x) застревает в вызове по значению, но в вызове по имени он уменьшается до (z λx.x), что является нормальной формой.
В контексте грамматика f является нормальной формой (в вызове по имени), определенной как:

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

Вы можете увидеть другое определение контекстов в главе 19.5.3 Пирса.

Ответ 2

Является ли ответ, что "внешний" и "самый внутренний" относится только к лямбда-абстракциям? Итак, для члена t в λz. t, t не может быть уменьшено, но в redex s t t сводится к значению v, если это возможно, а затем s v сокращается?

Да, это точно.