Лябда исчисление

[nbyte]

Здравствуйте.
Некак не выходит решить следующий пример
Есть терм, который вычисляет функцию $\[\neg x\]$
он равен

$$ \[\lambda {\rm{x}}{\rm{.((x0)1)}}\] $$

логические константы

$$\[\begin{array}{l} {\rm{0 = }}\lambda {\rm{x}}{\rm{.}}\lambda {\rm{y}}{\rm{.y}} \\ {\rm{1 = }}\lambda {\rm{x}}{\rm{.}}\lambda {\rm{y}}{\rm{.x}} \\ \end{array}\] $$

пробую вычислить с $x = 1$ и получить
так решаю

$$ \[\begin{array}{l} {\rm{(1) [}}\lambda {\rm{x}}{\rm{.((x0)1)](}}\lambda {\rm{x}}{\rm{.}}\lambda {\rm{y}}{\rm{.x)}} \\ {\rm{(2) (((}}\lambda {\rm{x}}{\rm{.}}\lambda {\rm{y}}{\rm{.x)(}}\lambda {\rm{x}}{\rm{.}}\lambda {\rm{y}}{\rm{.y))(}}\lambda {\rm{x}}{\rm{.}}\lambda {\rm{y}}{\rm{.x))}} \\ {\rm{(3) ((}}\lambda {\rm{y}}{\rm{.(}}\lambda {\rm{x}}{\rm{.}}\lambda {\rm{y}}{\rm{.y))(}}\lambda {\rm{x}}{\rm{.}}\lambda {\rm{y}}{\rm{.x)}} \\ {\rm{(4) }}\lambda {\rm{x}}{\rm{.}}\lambda {\rm{y}}{\rm{.(}}\lambda {\rm{x}}{\rm{.}}\lambda {\rm{y}}{\rm{.x)}} \\ \\ \end{array}\] $$

в этоге получаю не правильны ответ.
тоесть в ответе по идее должно быть
$\[{\rm{0 = }}\lambda {\rm{x}}{\rm{.}}\lambda {\rm{y}}{\rm{.y}}\]$
Помогите пожалуйста, кто-нибудь понять, где ошибка.

[Xaositect]

Четвертое из третьего не получается бета-редукцией.
Вы, видимо, путаетесь с переменными, переименуйте внутреннее $y$ во что-нибудь, если так удобнее.

[Circiter]

2nbyte
Как правильно заметил Xaositect, проблема в вычислении третьего правила. Здесь $1$ привязывается к $\lambda\rm y$ и больше нигде не используется, теряется. Остается $0$, что и требуется.

[nbyte]

Действительно.
Спасибо Вам!
Раньше до меня этот момент недоходил.

[Circiter]

2nbyte
Говоря более точно, во втором преобразовании кроме $\beta$-редукции выполняется $\alpha$-конверсия.