Задачка

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

[vanja-y.livejournal.com]

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

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

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

[vanja-y.livejournal.com]

Можно ещё

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

но я не уверен, что такое счастье будет работать.

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

Красиво, мне понравилось :)

Prelude> :t \x y -> (\s -> s (x s)) (\s -> y s s)
\x y -> (\s -> s (x s)) (\s -> y s s)
  :: ((t -> t1) -> t) -> (t -> t -> t1) -> t1

просто же как две копейки

[mr-aleph.livejournal.com]

Prelude> :t (\x y -> (\x' -> y x' x') (x (\x' -> y x' x'))) 
(\x y -> (\x' -> y x' x') (x (\x' -> y x' x')))
  :: ((t1 -> t) -> t1) -> (t1 -> t1 -> t) -> t

[zelych.livejournal.com]

а я вот так придумал: z f g = ab a where (ab, a) = (g a, f ab)

[asviraspossible.livejournal.com]

f :: ((a -> b) -> a) -> (a -> (a -> b)) -> b
f a b = x (a x)
where x = fix (b . a)

[kodt-rsdn.livejournal.com]

Гаскель-шмаскель

term :: ((a->b)->a) -> (a->(a->b)) -> b

term f g = b where
  a  = f ab -- чтобы не плодить сущности, оставим единственное значение типа a
  ab = g a
  b  = ab a
  -- или
  a = (f.g) a
  b = g a a

Поскольку здесь возникает неподвижная точка, - любители могут зафигачить туда Y и сделать нерекурсивный терм.

Примеры

-- самое простое: неподвижная точка константной функции
foo ab   = "hello"              -- a :: String
goo a a' = length a + length a' -- b :: Int
t = term foo goo -- t=10

-- чуть-чуть заковыристее
foo ab = map ab [[1], [1,2], [1,2,3], [1,2,3,4]] -- a :: [Int]
goo a a' = length a + length a'                  -- b :: Int
t = term foo goo -- t=8

[migmit.livejournal.com]

Думал секунд 30:

\g b -> (\d -> d (g d)) (\a -> b a a)

С днем варения!

[kitya.livejournal.com]

Отанжоби омедето гозаимас! Ну и троекратное ура!

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

[perikov.livejournal.com]

все закончилось сокрушительной победой пруф ассистантов :) Coq, Agda, djinn рисуют такие вещи нараз:)