Глупые вопросы по основам лямбда-исчисления

[xz121]

Читаю "Типы в языках программирования" Пирса, на стр. 61 русского издания:


Тут два места, которые я не могу понять:

1. Последний переход (выделенный красным). Если вдруг терм $v$ содержит переменную $f$ как свободную, то разве мы не должны при бета-редукции подставить вместо нее терм $w$ и получить, вообще говоря, терм, отличный от $v$?

2. Не проще ли определить терм $test$ как $\lambda x.x$? Казалось бы, тогда мы в одну редукцию (вместо трех) придем к $tru\;v\;w$.

[arseniiv]

xz121 в сообщении #1427368 писал(а):

1. Последний переход (выделенный красным). Если вдруг терм $v$ содержит переменную $f$ как свободную, то разве мы не должны при бета-редукции подставить вместо нее терм $w$ и получить, вообще говоря, терм, отличный от $v$?

Я думаю, там выше должно было быть написано, что мы воспринимаем термы с точностью до α-конверсии и что мы заменяем переменные, если вдруг при подстановке они бы замкнулись. Здесь ровно такой случай: если в $v$ свободна $f$, подстановка $(\lambda f. t)[t\mapsto v]$ в строгом смысле запрещена, но если мы заменим $f$ на свежую переменную — или заранее выбрали её аккуратно — то мы сможем заменить и получить терм $\lambda f.v$, где в $v$ обязательно нет свободных вхождений $f$. Потому дальше всё норм.

xz121 в сообщении #1427368 писал(а):

2. Не проще ли определить терм $test$ как $\lambda x.x$? Казалось бы, тогда мы в одну редукцию (вместо трех) придем к $tru\;v\;w$.

Да, можно. Определение в тексте просто ради наглядности, ну и при некоторых стратегиях вычисления оно может быть предпочтительнее, чем просто $I$.

-- Сб ноя 23, 2019 22:27:14 --

Кстати Пирса вы хорошо выбрали. Там вроде есть и какие-то пояснения дальше, и если будет совсем плохо, откройте оригинал, и там может быть небольшая разница в словах (хотя перевод этого кусочка по-моему чистый).

[xz121]

arseniiv
Спасибо!
Как выяснилось, явно про альфа-конверсию написано на 10 страниц позже, а тут, видимо, подразумевалось как очевидное :)