deniok | Задачка

Entry tags:

Задачка

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

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

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

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

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

Flat | Top-Level Comments Only

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

Гы-гы-гы!

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

(no subject)

deni-ok.livejournal.com - 2010-09-21 21:04 (UTC) - Expand

(no subject)

zelych.livejournal.com - 2010-09-22 07:16 (UTC) - Expand

Знаю, да

cadadr.livejournal.com - 2010-09-22 11:18 (UTC) - Expand

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

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

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

то есть

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

конечно.

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

(no subject)

anatoly borodin - 2010-09-21 20:37 (UTC) - Expand

(no subject)

ro-che.info - 2010-09-21 20:44 (UTC) - Expand

(no subject)

anatoly borodin - 2010-09-21 21:47 (UTC) - Expand

(no subject)

cadadr.livejournal.com - 2010-09-21 21:04 (UTC) - Expand

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

Можно ещё

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

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

наверное всё-таки

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

Но это тоже с Y...

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

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

Правильно! У меня решение другое

Prelude> :t \f g -> g (f (\x -> g x x)) (f (\x -> g x x))
\f g -> g (f (\x -> g x x)) (f (\x -> g x x))
  :: ((t1 -> t) -> t1) -> (t1 -> t1 -> t) -> t

но я использовал хинт из первоисточника.

Оно не другое, я тоже сначала к такому пришел, просто потом "разложил на множители". Вот этот последний шаг мне особенно понравился :)

(no subject)

deni-ok.livejournal.com - 2010-09-21 20:58 (UTC) - Expand

\ f g -> g (f (\ x -> g x x)) (f (\ x -> g x x))

cadadr.livejournal.com - 2010-09-21 20:57 (UTC) - Expand

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

ну да, все эти тавтологии пропозициональной логики, они такие, двухкопеечные

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

mr-aleph.livejournal.com - 2010-09-22 10:35 (UTC) - Expand

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

Рекурсия в where!
Просто типизированная лямбда негодуе!11

(no subject)

zelych.livejournal.com - 2010-09-22 07:47 (UTC) - Expand

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

Если поменять местами, то:

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

(no subject)

deni-ok.livejournal.com - 2010-09-22 14:03 (UTC) - Expand

(no subject)

asviraspossible.livejournal.com - 2010-09-22 15:56 (UTC) - Expand

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

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