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

Question

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

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

Является ли ответ, что «самые внешние» и «самые внутренние» относятся только к лямбда-абстракциям?Таким образом, для члена t в λz. t значение t не может быть уменьшено, но при переопределении s t значение t уменьшается до значения v, если это возможно, а затем s vуменьшается?

Answer 1

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

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

E = [ ] | Et | fE

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

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

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

Answer 2

Является ли ответ, что «самые внешние» и «самые внутренние» относятся только к лямбда-абстракциям? Таким образом, для члена t в λz. t, t не может быть уменьшено, но в переопределении s t, t уменьшается до значения v, если это возможно, и затем s v уменьшается?

Да, именно так.