Задачка

[deniok]

Хорошая задачка из Herman Geuvers, Introduction to Type Theory (упражнение 3.17):

Построить лямбда-терм с типом ((α → β) → α) → (α → α → β) → β.

Ответы скринить не буду.

UPD: Имеется в виду просто типизированная лямбда. То есть fix и прочие Y-комбинаторы нам недоступны.

UPD2: Рекурсия ни в каком виде недоступна!

Comments

[vanja-y.livejournal.com]

Ничего лучше чем

\f g -> g(Y(f.g))

не придумывается.

[vanja-y.livejournal.com]

то есть

\f g -> g (Y(f.g)) (Y(f.g))

конечно.

[deni-ok.livejournal.com]

это уже близко к победе.
хинт: никто не запрещает вложенные лямбды (a без Y, наоборот, можно обойтись, поскольку выше уже показали, что это теорема минимальной логики высказываний :)

[anatoly borodin (from livejournal.com)]

Ну тогда и ((α → γ) → α) → (α → α → β) → β можно.

[ro-che.info (from livejournal.com)]

Ээ.. как?

[anatoly borodin (from livejournal.com)]

Никак, гоню.

[cadadr.livejournal.com]

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

[ro-che.info (from livejournal.com)]

Y не имеет типа, вот в чем проблема.
А если б имел, то можно было бы еще проще -- "Y I" :)