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

[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)

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

[lomeo.livejournal.com]

У тебя джаббер есть? мой lomeo.nuke на гмыле.

[deni-ok.livejournal.com]

Я плохо представляю, что это такое :))
Но на гмыле dmoskvin слева есть чат - это то что надо?

[lomeo.livejournal.com]

То, но достучаться не получается :(

[deni-ok.livejournal.com]

У меня тоже :(
Со всеми остальными я общаюсь, а ты?

[ro-che.livejournal.com]

Что-то типа (\x.f(xx))(\x.f(xx)), f -- любая инволюция (т.е. f . f = id)