Call by value in the lambda calculus

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

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

Относится ли ответ, согласно которому "крайний" и "внутренний" относятся только к лямбда абстракциям? То есть для термина t в λz. t, t не может быть уменьшен, но в редексе s t, t уменьшается до значения v, если это возможно, а затем s v уменьшается?