Вызов по значению в исчислении лямбда
Я прокладываю себе путь через Типы и языки программирования, а Пирс - для стратегии снижения стоимости вызова, дает пример 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 сокращается?
Да, это точно.
