Лямбда, которую мы потеряли

[deniok]

Пара задачек по лямбда-исчислению.

(1) Сконструируйте лямбда-терм F, такой что для любого терма M выполнялось бы

FM = MF

(2) Сконструируйте лямбда-терм G, такой что для любых термов M и N выполнялось бы

GMN = NG(NMG)

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

Comments

[lomeo.livejournal.com]

Первая. Во первых, берём форму

FM=(YG)M,

так как очевидно, что F - рекурсивна. Итак,

FM=(YG)M=G(YG)M
G(YG)M=MF=M(YG)
G = \a b . b a
F = Y(\a b . b a)

Вторая сложнее, сейчас подумаю.

[lomeo.livejournal.com]

Ну, аналогичными преобразованиями

G = Y (\f m n. n f (n m f))

[deni-ok.livejournal.com]

Браво! Ты, как обычно, лучший! На самом деле это теорема

Пусть имеется терм C=C[f,m,n,k,...] содержащий (возможно) указанные свободные переменные. Тогда для произвольных термов M, N, K, ... существует терм F, такой что

F M N K ... = C[f:=F][m:=M][n:=N][k:=K]...

Доказательство - конструктивное, конструируется

F = Y(\fmnk... -> C[f,m,n,k,...])

и доказывается, что это то, что надо :)

[lomeo.livejournal.com]

Спасибо! Я уже, когда выложил второе решение только заметил, что там всё просто конструируется.

[nealar.livejournal.com]

Первая F = GG
G = \g m . m g g
Шо-то такое у нас летом было.

[deni-ok.livejournal.com]

Что-то мне эта версия непонятна. Скобочек по-моему не хватает в одном месте...

А что летом у вас было?

[nealar.livejournal.com]

Там были алгоритмы Маркова на самом деле, но поскольку я о них кроме названия ничего не знаю, то делали лямбда-исчисление :)
А откуда у тебя в журнале реклама? От неё фокс глючит.

[deni-ok.livejournal.com]

Там - это где? Я не в курсе совершенно...

Реклама у меня из-за улучшенного аккаунта, а он из-за желания иногда картинок выложить. Я бы и платный оплатил - только лень и не знаю как :)

[nealar.livejournal.com]

на icfpc2007

[nealar.livejournal.com]

F = (\g. \m. m g g) (\g'. \m'. m' g' g')
Так?

[deni-ok.livejournal.com]

Ну это-то альфа-конверсия, она и так подразумевается где надо; а в конце всё равно не получается:

FM = (\g. \m. m g g) (\g'. \m'. m' g' g') M 
   = M (\g'. \m'. m' g' g') (\g'. \m'. m' g' g')
   фиг а не = M F, аппликация левоассоциативна

На самом деле чтобы сошлось надо

F = GG
G = \g m . m (g g)

но лучше не изобретать Y-подобный велосипед, а сразу им (Y) пользоваться, как lomeo.

[nealar.livejournal.com]

Дык, это если Y уже есть. То есть, совет невеждам не подходит. :)

[deni-ok.livejournal.com]

Ну Y это средоточие всех тайн и загадок. Держи:

Теорема 1. Для любого терма F существует терм X, такой что

FX = X

Этот X мудрецы зовут неподвижной точкой.
Доказательство: Введём

G = \x.F(xx)

тогда искомая неподвижная точка

X = GG

Воистину, это так

X = GG 
  = (\x.F(xx))(\x.F(xx)) 
  = F((\x.F(xx))(\x.F(xx))) 
  = F(GG)
  = FX

[deni-ok.livejournal.com]

Теорема 2 Существует комбинатор неподвижной точки Y,

Y=\f.(\x.f(xx))(\x.f(xx))

такой что для любого F

F(YF)=YF

Доказательство: Из предыдущей теоремы замечаем, что

YF = (\x.F(xx))(\x.F(xx)) 
   = GG
   = X

[kernelring.livejournal.com]

Как полный чайник, который интересуется ЛИ и функциональным программированием, не могу найти ответы на следующие вопросы:
А дальше что? Зачем нужны все эти неподвижные точки и Y-ки? Почему все так носятся с ними? Что пытаются доказать или выразить?

[deni-ok.livejournal.com]

Ну, если вы интересуетесь ЛИ, то непонятно, в чём вопрос. Как только мы ввели основные понятия (лямбда-терм с абстракцией и аппликацией) и задали схему бета-редукции, тут же Y и вылезает. Без него ЛИ не полное по Тьюрингу - арифметику, например, не задашь.

[kernelring.livejournal.com]

Вопрос в том, что хочется видеть конечную цель. Без такого видения очень сложно отделять главное от шелухи. Вот задали арифметику, а потом что? Ради чего её задавали? Может быть есть какой-нибудь мануал, где бы уделялось место не вопросу "как", а "зачем"? Или без мощного математического бэкграунда в эту область лучше не соваться?

[deni-ok.livejournal.com]

Конечная цель - это очень индивидуально, нес па?

Для меня ЛИ - это база, на основе которой скорее всего родится разумная универсальная нотация для записи вычислительных алгоритмов. Потому что современные массовые прикладные языки программирования - это, конечно, что-то типа римских цифр до изобретения арабских. По степени стройности общей концепции :-)

[kernelring.livejournal.com]

Полностью с вами согласен насчёт индивидуальности цели. На что, по вашему мнению, мне стоит обратить особое внимание при изучени ФП, если я преследую цель повышения продуктивности и выразительности труда программиста? Не является ли утопией моя задумка иметь конвертор (Haskell, например) -> (C, например)?

[deni-ok.livejournal.com]

>На что, по вашему мнению, мне стоит обратить особое внимание при изучени ФП, если я преследую цель повышения продуктивности и выразительности труда программиста?

По-моему так задачек побольше решать надо: SICP, YAHT стоит прочесть и упражнения прорешать (ну второе, конечно, не такое заслуженно именитое как первое). Первое, кстати, многие люди делают не только на Схеме, но и, параллельно, на Хаскелле.

>Не является ли утопией моя задумка иметь конвертор (Haskell, например) -> (C, например)?

Не очень понятно, зачем. Компилятор GHC сам по себе и есть почти что такой конвертер. И потом Хаскелл всё-таки ленивый язык, ему сишная модель исполнения не очень подходит.

[kernelring.livejournal.com]

Спасибо за советы.
>Не очень понятно, зачем
В данном случае просто интересно провернуть такую комбинацию:
исходник на Haskell->конвертор->исходник на С->целевое окружение, для которого ещё нет (и скорее всего не будет в ближайшее время) поддержки Haskell runtime.
А эту ленивость можно обойти? Не пользоваться ей, например? Или без ленивости получится как в С без указателей? :-)

[deni-ok.livejournal.com]

>А эту ленивость можно обойти?

Обойти-то всё можно, только зачем тогда Хаскелл?

[lomeo.livejournal.com]

Не надо про лето! :)

[(Anonymous)]

Почему?

[bntr.livejournal.com]

Приветствую!

я тут пишу-таки работу про визуальный конструктор лямбда-выражений
и построил в нем ваш терм FM, где F=(\gm.m(gg))(\gm.m(gg)) а M - свободная переменная:



здесь анимация (200kb) построения этого терма и его редукции сначала до M((\gm.m(gg))(\gm.m(gg)))
а потом дальше до M((\m.m(\m.m(\m.m((\gm.m(gg))(\gm.m(gg)))))))

тут основа используемого синтаксиса

если вас заинтересует конструктор, то здесь можно его скачать.
он пишется на питоне и требует
python 2.5 http://www.python.org/download/
и pygame 1.8 http://www.pygame.org/download.shtml

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

[deni-ok.livejournal.com]

Супер!
А чтобы редукции в классической лямбде отображались где-нибудь внизу/сбоку?

[bntr.livejournal.com]

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

[deni-ok.livejournal.com]

Просто работать с чисто визуальными и динамическими образами очень трудно. А автору это не всегда понятно ;-) Я в своё время с кубиком Рубика столкнулся с похожими проблемами:

http://deniok.narod.ru/

Без предварительных стрелочек юзерам совсем тяжело было. Да и потом все ругались, что тяжело алгоритм читать с экрана.

Чтобы это хозяйство было удобно многим, очевидно стоит регулировать скорость, либо сделать удобный пошаговый интерфейс.

[bntr.livejournal.com]

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

надеюсь, достаточно вывода на консоль выбранного суб-терма и всего терма после редукции

регулировку скорости да, добавлю, спасибо.

интерфейс кажется довольно пошаговый: одно нажатие Enter - одна редукция. плюс возможность шагов назад.

[deni-ok.livejournal.com]

А в движке при раскраске используется классическая лямбда с альфа-конверсией или индексы de Bruijn?

[bntr.livejournal.com]

можно сказать что третий вариант: каждой новой лямбде (и связанным с ней переменным) просто назначается новый цвет из пространства цветов.

еще (но это не строго) цвета в закрытом под-терме (под-терм без свободных переменных) объединены одним тоном (hue) и отличаются только яркостью.

[lomeo.livejournal.com]

Вау! Я видел пару картинок (http://bntr.livejournal.com/13102.html) - это было круто, но то, во что это выросло сейчас, гораздо гораздее! Мне нравится, здОрово!

[bntr.livejournal.com]

да тут было решил попробовать летом защитить это как диплом..

а в тех старых гифах был немного другой синтаксис: "f x y" и "f (g x)" были наоборот ("f x y" был вряд). но буквально на выходных руководитель меня просветил как лучше.

может еще можно что-то улучшить?

[thesz.livejournal.com]

Завораживает. ;)

[asviraspossible.livejournal.com]

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

1)

F M = M F
F = \x . x F = (\f x. x f) F = Y (\f x. x f) = (\f. (\x. f (x x))(\x. f (x x))) (\f x. x f)
= (\x. (\a b. b a) (x x)) (\x. (\a b. b a) (x x)) =
= (\x b. b (x x)) (\x b. b (x x))

2)

G = \m n.n G (n m G) = (\g m n. n g (n m g)) G =
(\f. (\x. f (x x))(\x. f (x x))) (\g m n. n g (n m g)) =
= (\x. (\g m n. n g (n m g)) (x x))(\x. (\g m n. n g (n m g)) (x x))
= (\x m n. n (x x) (n m (x x))) (\x m n. n (x x) (n m (x x)))

[deni-ok.livejournal.com]

Ага, замечательно!

[antilamer.livejournal.com]

Я чего-то не понимаю, или это правильный ответ?
F = Y (\GM . M G)
G = Y (\FMN . N F (N M F))

Осталось только упростить. Или в этом и будет загвоздка?

[antilamer.livejournal.com]

Прочитал комменты; видимо, загвоздки не будет и я тоже крутой ;)

[deni-ok.livejournal.com]

Крутой, крутой :-)