Y-комбинатор

Это вообще про что и к чему, и при чем тут Development? Может тебе на http://www.mathforum.ru/

Почему? лямбда-исчисление непосредственно соотноситься с программированием, является его теоретической основой. К тому же я сомневаюсь, что тамошние хомячки имеют об этом представление.

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

Кстати, всегда интересовало, каким боком Y-комбинатор к программированию? Рекурсия что ли на самом деле выполняется через Y-комбинатор?

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

Вот пример редукций из английской вики, более детально разжевано, но ни хрена не понятно:

Y g	= (λf . (λx . f (x x)) (λx . f (x x))) g; (by definition of Y)
	= (λx . g (x x)) (λx . g (x x))	; (β-reduction of λf: applied to g)
	= g ((λx . g (x x)) (λx . g (x x))); (β-reduction of λx: applied left function to right function)
	= g (Y g); (by second equality)

Посмотри Little Schemer, chapter 9

В смысле? Здесь вся суть как раз в бета-редукции по иксу.

Y g = (/f. (/x.(f(x x))) (/x.(f(x x))))
    = (/x.(g(x x))) (/x.(g(x x)))
    = g ((/x.(g(x x))) (/x.(g(x x))))
    = g (Y g) = g (g (Y g) = g (g (g (...))

Откуда там берется в начале строки g?

Ну так комбинатор к какой-то функции в конечном счёте применяется, вот тебе и расписывают детально что будет, если его к любой функции g применить.

Извините пожалуйста, но я не понял. На второй строчке заканчиваются вычисления, мы получаем невычисляемую аппликацию, ей негде взять свой x. Потом нам подставляют в начале g, к которй применялся Y. Допустим g - это /x.x. Он вернет все ту же невычислимую аппликацию. Как это порождает рекурсию?

Смотри, в первой строчке у нас функция одного аргумента f, на его место мы подставляем нашу функцию g, получаем вторую строчку, которая являет собой функцию одного аргумента x, на место которого мы подставляем ту же самую функцию одного аргумента x: (/x.(g(x x))), после подстановки получаем третью строчку, которая в силу второй строки тождественно равна g (Y g).

Ну так комбинатор к какой-то функции в конечном счёте применяется, вот тебе и расписывают детально что будет, если его к любой функции g применить.

Нет я ко 2 строке претензий не имею. Я про 3-ю. Применение Y к g должно редуцироваться в аппликацию (/x.(g(x x))) (/x.(g(x x))) - здесь все ясно. Но дальше ничего ведь вычислено быть не может. Откуда эта аппликация возьмет тсвой x?

То есть вся суть y-комбинатора в том, что мы в (/x.(g(x x))) на место икса подставляем саму (/x.(g(x x))) — это и даёт нам рекурсию.

получаем вторую строчку, которая являет собой функцию одного аргумента x

Почему она является функцией одного аргумента, если она является аппликацией 2 функций, которая не может быть вычислена?

Откуда эта аппликация возьмет тсвой x?

Он равен (/x.(g(x x))), т.е. безымянной функции одного аргумента (своего икса).

Почему она является функцией одного аргумента, если она является аппликацией 2 функций, которая не может быть вычислена?

Потому что аппликация только одна. У нас только λx и ничего больше, а дальнейший хвост идёт просто как параметр и раньше времени не вычисляется.

То есть вся суть y-комбинатора в том, что мы в (/x.(g(x x))) на место икса подставляем саму (/x.(g(x x))) — это и даёт нам рекурсию.

Тогда неверно скобки расставлены. должно быть /x.(g(x x)) (/x.(g(x x)))

должно быть /x.(g(x x)) (/x.(g(x x)))

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

Это одно и то же

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

зачем лепить лишние скобки

Просто для красоты, логически отделить одну часть от другой. В лямбда-исчислении всё сводится в аппликации, поэтому как мы напишем: Y(g) или (Y)g, или даже (Y)(g) не играет абсолютно никакой роли.

Y(g) или (Y)g, или даже (Y)(g) не играет абсолютно никакой роли.

Здесь да, а вот A(BC) или (AB)C - разница уже есть.

Ну здесь уже разумеется :3

В лямбда-исчислении всё сводится в аппликации

А как же лямбда абстракция?

Ну в конечном-то итоге.

У нас одному такому «молодому учёному» двойку на защите диплома поставили.
Подсказать, почему?

Очень интересно.

Ссылка на вики? :3

На самом деле, я когда учился, я ржал, когда преподы строили из себя умников, предираясь к подобным вещам. Эти безмозглые олени, по большей части, знания всю жизнь получали из книжечек, и в реальном производстве нули, но любители показать какие они умницы. Сама по себе ссылка на инет, или на каноническую (для них) литературу, ничего ни значит. Если препод знает свой предмет, а таких единицы, он и так способен оценить знания ученика. Если имеют место такие придирки, сразу можно на такого препода ставить клеймо.

До второй строчки все логично, дальше какая-то ересь. Откуда там берется в начале строки g?

Имеем:

 (λf . (λx . f (x x)) (λx . f (x x))) g

Производим бета-редукцию (подставляем g вместо аргумента переменной f внутри выражения). Можно представить это как вызов функции:

 ;; Scheme code
 (define (y f) ((lambda (x) (f (x x))) (lambda (x) (f (x x)))))
 (y g) => ((lambda (x) (g (x x))) (lambda (x) (g (x x)))) =>
          (g ((lambda (x) (g (x x))) (lambda (x) (g (x x))))) =>  
          (g (y g))

Последнее (g (y g)) происходит из того, что предыдущий результат у нас это вызов функции g с аргументом ((\x . g (x x)) (\x . g (x x))), что в свою очередь и есть определение Y комбинатора (см. (define (y f) ...)).

ТС - безмозглый олень, потому что хочет чему-то научиться из википедии

А ты, как я понял, ходишь на википедию чисто поржать...

(λx . g (x x)) (λx . g (x x))	= g ((λx . g (x x)) (λx . g (x x)));

Откуда там берется в начале строки g?

А как оно может НЕ взяться?

Смотри, как вообще бета-редукция устроена? (λx.e)y редуцируется к e, в котором КАЖДОЕ свободное вхождение x заменяется на y (возможно, с переименованием переменных, чтобы избежать их случайного захвата — нам об этом беспокоиться не нужно).

В данном случае у нас e — это g (x x), а y — это (λx . g (x x)). Соответственно, если мы в e заменим КАЖДОЕ свободное (а других у нас нет) вхождение x на (λx . g (x x)) — мы получим правую часть.

То есть, g берётся именно из-под первой лямбды.

Это одно и то же.

Нет, не одно и то же. Лямбда по правилам загребает под себя столько, сколько сможет. То есть,

λx . g (x x) (λx . g (x x)) = λx . (g (x x) (λx . g (x x)))

Лямбда по правилам загребает под себя столько, сколько сможет.

Да, кстати, ты прав.

А все же тут есть определеннная натяжка. Весь вопрос сводится к тому, можем ли мы считать результат редукции Y g (вторая строка) за сам Y g (запись, аппликацию - первая строка), что следует из заключения Y g = g (Y g). Если считать это тру равенством, необходима аксиома-определения равенства. Если считать результат редукции равным самой аппликации, догда да, справедливо. В этом случае мы должны, как бы полностью абстрагироваться от времени, но само понятие шага редукции этому противоречит. Поэтому не так уж тут все однозначно, больше похоже на демагогию.

Ну да, она и обычная арифмерика этим грешит: 4=2+2, типа, абстрагирования от времени. От времени то может мы и абстрагировались, а от числа редукций в программировании не можем. Возникает вопрос: а что будет делать 4 пока вычисляется 2+2? Вычисляться в себя? сколько раз. Мы это явно не указываем. А откуда машина об этом узнает? Ей не понятно сколько раз надо вычислить одно повыражение, сколько другое; когда остановиться. Вот она изнанка декларативности: создание видимости решения проблемы, вместо ее решения. Так что непонятно, зачем математику пытаются натянуть на программирование. Если ты натянул презерватив на член - это не значит, что он делает работу вместо члена.

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

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

Тут уже нужно переходить к семантике. Потому что лямбда-термы, пусть даже связанные редукцией, разумеется, не равны. Но, скажем, в семантике Скотта равенство уже появится.

Если считать результат редукции равным самой аппликации, догда да, справедливо. В этом случае мы должны, как бы полностью абстрагироваться от времени, но само понятие шага редукции этому противоречит.

Операционная семантика задает отношение эквивалентности. Никакого времени в нем и нет изначально - терм до редукции эквивалентен терму после редукции. И наоборот, конечно. Так что ничего ничему не противоречит.

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

Смотря что под равенством подразумевать. Если отношение эквивалентности, задаваемое семантикой - вполне равны.

Смотря что под равенством подразумевать.

«Подразумевать» тут нечего. Равенство есть равенство.

«Подразумевать» тут нечего. Равенство есть равенство.

Равенство - это некоторое отношение эквивалентности. И задать на термах его можно по-разному. Но если подразумевать некий дефолт - то тогда никакой семантики Скотта для равенства не нужно, как только задали редукции - сразу и равенство есть.