Ненормализуемая вертушка

[deniok]

Придумал задачку по лямбда исчислению.

Общеизвестен лямбда-терм, не имеющий нормальной формы

(\x.xx)(\x.xx)

Этот терм обладает следующим свойством: он воспроизводит сам себя при каждой бета-редукции, ведя себя по отношению к ней как экспонента по отношению к дифференцированию.

А теперь задача: написать не имеющий нормальной формы терм, который бы вел себя как e^(-x). То есть при первой бета-редукции он должен превращаться во что-то другое, а при следующей возвращаться к исходному виду. Моя версия такого терма (flipflop) под катом белым цветом

flip = \xyz.xyzz
flop = \xyz.yxxz

flipflop = flip flop flop flip ~> -- первая редукция
flop flop flip flip            ~> -- вторая редукция
flip flop flop flip            = flipflop

Может кто придумает попроще?

UPD: Эх, а у меня-то решение неправильное :) (Потому что у меня аж шесть шагов) Правильное - у lomeo в комментах.

Comments

[lomeo.livejournal.com]

Первое, что пришло в голову

(\xy.yxy)T(\xy.yxy)

T - любая лямбда

Не ошибся?

[deni-ok.livejournal.com]

Направление то же, что и у меня было. Все хорошо, но при первой бета-редукции он должен превращаться во что-то другое, а превращается сам в себя :)

[lomeo.livejournal.com]

У меня при первой редукции он превращается в (\y.yTy)(\xy.yxy) - разве это исходный терм?

[deni-ok.livejournal.com]

Черт, да, ты прав. Я за шаг что-то принял аппликацию "лямбды двух переменных" :(

[deni-ok.livejournal.com]

Проапдейтил пост.
Кстати, а трехходовку можно сделать?

[lomeo.livejournal.com]

Аналогично :)

(\xyz.zxyz)AB(\xyz.zxyz)

Четырёхходовку дать? ;)