Задачка

[deniok]

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

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

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

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

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

Comments

Re: Как и следовало ожидать

[deni-ok.livejournal.com]

хорошо хоть, что пока ещё большинство пользующихся пруф ассистантами понимают как они работают :)

Re: Как и следовало ожидать

[perikov.livejournal.com]

цивилизация - эо постоянное нарастание количества вещей, которыми можно пользоваться, не понимая, как они устроены :)

Re: Как и следовало ожидать

[deni-ok.livejournal.com]

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