Задачка

[deniok]

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

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

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

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

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

Comments

[cadadr.livejournal.com]

Coq < Theorem cheat : forall A B : Prop, ((A -> B) -> A) -> (A -> A -> B) -> B.
1 subgoal
  
  ============================
   forall A B : Prop, ((A -> B) -> A) -> (A -> A -> B) -> B

cheat < auto.
Proof completed.
...

[deni-ok.livejournal.com]

Гы-гы-гы!

[cadadr.livejournal.com]

Ну, конкретно это можно и ручками выписать.

[deni-ok.livejournal.com]

я как раз и запостил её с этой целью

и ждал читеров с джином, а не с COQ :)

[zelych.livejournal.com]

а зачем ручками-то?
Если поменять Prop на Set, можно extract сделать:

Coq> Extraction cheat.

let cheat h h0 =
  h0 (h (fun h1 -> h0 h1 h1)) (h (fun h1 -> h0 h1 h1))

Знаю, да

[cadadr.livejournal.com]

Ручками --- в смысле, для тренировки ума.