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

[deniok]

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

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

FM = MF

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

GMN = NG(NMG)

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

Comments

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

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