deniok

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

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)

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

From:

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

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

From:

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

Пусть имеется терм 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,...])

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

From:

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

From:

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

From:

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

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

From:

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

From:

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

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

From:

на icfpc2007

From:

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

From:

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

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.

From:

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

From:

Ну 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

From:

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

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

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

F(YF)=YF

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

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

From:

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

From:

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

From:

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

From:

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

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

From:

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

From:

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

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

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

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

From:

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

From:

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

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

From:

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

From: (Anonymous)

Почему?

From:

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

я тут пишу-таки работу про визуальный конструктор лямбда-выражений
и построил в нем ваш терм 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

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

From:

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

From:

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

From:

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

http://deniok.narod.ru/

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

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

From:

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

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

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

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

From:

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

From:

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

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

From:

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

From: