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

[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 - любая лямбда

Не ошибся?

[lomeo.livejournal.com]

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

[ro-che.livejournal.com]

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