Понятный, интуитивно понятный вывод комбинатора с фиксированной точкой (Y комбинатор)?

28

Комбинатор FIX с фиксированной запятой (он же Y-комбинатор) в (нетипизированном) лямбда-исчислении ( $\lambda$ ) определяется как:

FIX $\triangleq \lambda f.(\lambda x. f~(\lambda y. x~x~y))~(\lambda x. f~(\lambda y. x~x~y))$

Я понимаю его назначение и прекрасно отслеживаю выполнение его приложения; Я хотел бы понять, как вывести FIX из первых принципов .

Вот, насколько я понимаю, когда я пытаюсь получить это сам:

FIX - это функция: FIX $\triangleq \lambda_\ldots$
FIX использует другую функцию, , чтобы сделать ее рекурсивной: FIX $f$ $\triangleq \lambda f._\ldots$
Первый аргумент функции - это «имя» функции, используемое там, где предназначено рекурсивное приложение. Поэтому все появления первого аргумента для должны быть заменены функцией, и эта функция должна ожидать остальных аргументов (давайте просто предположим, что принимает один аргумент): FIX $f$ $f$ $f$ $f$ $\triangleq \lambda f._\ldots f~(\lambda y. _\ldots y)$

Это где я не знаю, как «сделать шаг» в моих рассуждениях. Маленькие эллипсы указывают, где в моем FIX чего-то не хватает (хотя я могу узнать это только по сравнению с «настоящим» FIX).

Я уже прочитал « Типы и языки программирования» , который не пытается вывести его напрямую, а вместо этого отсылает читателя к «Маленькому интригану» за выводом. Я тоже это читал, и его «вывод» не был таким уж полезным. Более того, речь идет не о прямом выводе, а об использовании очень специфического примера и о специальной попытке написать подходящую рекурсивную функцию в . $\lambda$

computability logic programming-languages lambda-calculus combinatory-logic BlueBomber
источник

1

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

Xodarap

2

Существует несколько различных комбинаторов с фиксированной точкой. Возможно, люди просто играли с комбинаторами, пока не наткнулись на них.

Юваль Фильмус

@YuvalFilmus, это то, что мое исследование и ответ на этот вопрос начинают заставлять меня задуматься. Но я все еще думаю, что было бы поучительно «увидеть», как комбинатор (ы) логически формируются, что особенно полезно при, например, попытке создать новый комбинатор.

BlueBomber

Прочитайте главу 9 в «Маленьком Лиспере» Даниэля П. Фридмана (или «Маленький интриган»)

user18199

2

ОП, кажется, указывает, что они уже прочитали это.

Рафаэль

29

Я нигде не читал это, но вот как я полагаю, мог быть получен: $Y$

Давайте иметь рекурсивную функцию , возможно, факториал или что-то еще в этом роде. Неформально мы определяем как псевдо-лямбда-термин, где встречается в его собственном определении: $f$ $f$ $f$

f = \dots f \dots f \dots

$f = \ldots f \ldots f \ldots$

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

f = \underset{M}{\underset{⏟}{(λ r . (\dots r \dots r \dots))}} f

$f = \underbrace{(\lambda r . (\ldots r \ldots r \ldots))}_{M} f$

Теперь мы могли бы определить если бы у нас был только способ передать его в качестве аргумента самому себе. Это невозможно, конечно, потому что у нас нет под рукой. То , что мы имеем под рукой . Поскольку содержит все, что нам нужно для определения , мы можем попытаться передать в качестве аргумента вместо и попытаться восстановить из него позже внутри. Наша первая попытка выглядит так: $f$ $f$ $M$ $M$ $f$ $M$ $f$ $f$

f = \underset{M}{\underset{⏟}{(λ r . (\dots r \dots r \dots))}} \underset{M}{\underset{⏟}{(λ r . (\dots r \dots r \dots))}}

$f = \underbrace{(\lambda r . (\ldots r \ldots r \ldots))}_{M} \underbrace{(\lambda r . (\ldots r \ldots r \ldots))}_{M}$

Однако это не совсем правильно. Перед тем , получили заменить внутри . Но теперь мы проходим вместо. Мы должны как - то исправить все места , где мы используем , чтобы они реконструкции от . На самом деле, это совсем не сложно: теперь, когда мы знаем, что , везде, где мы используем мы просто заменяем его на . $f$ $r$ $M$ $M$ $r$ $f$ $M$ $f = M M$ $r$ $(r r)$

f = \underset{M^{'}}{\underset{⏟}{(λ r . (\dots (r r) \dots (r r) \dots))}} \underset{M^{'}}{\underset{⏟}{(λ r . (\dots (r r) \dots (r r) \dots))}}

$f = \underbrace{(\lambda r . (\ldots (rr) \ldots (rr) \ldots))}_{M'} \underbrace{(\lambda r . (\ldots (rr) \ldots (rr) \ldots))}_{M'}$

Это решение хорошо, но нам пришлось изменить внутри. Это не очень удобно. Мы можем сделать это более элегантно, не изменяя , введя другой который посылает свой аргумент, примененный к самому себе: выражая как мы получаем $M$ $M$ $\lambda$ $M$ $M'$ $\lambda x.M(xx)$

f = (λ x . \underset{M}{\underset{⏟}{(λ r . (\dots r \dots r \dots))}} (x x)) (λ x . \underset{M}{\underset{⏟}{(λ r . (\dots r \dots r \dots))}} (x x))

$f = (\lambda x.\underbrace{(\lambda r . (\ldots r \ldots r \ldots))}_{M}(xx)) (\lambda x.\underbrace{(\lambda r . (\ldots r \ldots r \ldots))}_{M}(xx))$

Таким образом, когда заменяется на , заменяется на , который по определению равен . Это дает нам нерекурсивное определение , выраженное как действительный лямбда-член $M$ $x$ $MM$ $r$ $f$ $f$

Переход на теперь легкий. Мы можем взять произвольный лямбда-член вместо и выполнить эту процедуру для него. Таким образом, мы можем выделить и определить $Y$ $M$ $M$

Y = λ m . (λ x . m (x x)) (λ x . m (x x))

$Y = \lambda m . (\lambda x. m(xx)) (\lambda x.m(xx))$

Действительно, сводится к как мы его определили. $Y M$ $f$

Примечание: я получил как это определено в литературе. Комбинатор вы описали это вариант для вызова по значению языков, иногда также называют . Смотрите эту статью в Википедии . $Y$ $Y$ $Z$

Петр Пудлак
источник

1

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

для некоторого

. Затем, когда мы создаем

, мы используем это утверждение, что

определяется как приложение чего-то к себе внутри

, например, применяя

к

в вашем ответе, который по определению равен

. Захватывающий!

f = X (X)

$f = X (X)$

X

$X$

X

$X$

f

$f$

X

$X$

x

$x$

x

$x$

f

$f$

BlueBomber

11

Как отметил Ювал, не существует только одного оператора с фиксированной запятой. Их много. Другими словами, уравнение для теоремы о неподвижной точке не имеет единственного ответа. Таким образом, вы не можете извлечь оператора из них.

Это все равно что спрашивать, как люди выводят как решение для . Они не! Уравнение не имеет единственного решения. $(x,y)=(0,0)$ $x=y$

На тот случай, если вы хотите узнать, как была открыта первая теорема о неподвижной точке. Позвольте мне сказать, что я также задавался вопросом о том, как они придумали теоремы о фиксированной точке / рекурсии, когда я впервые увидел их. Это кажется таким гениальным. Особенно в форме теории вычислимости. В отличие от того, что говорит Ювал, это не тот случай, когда люди играют, пока не найдут что-то. Вот что я нашел:

Насколько я помню, теорема изначально принадлежит С. К. Клини. Клини предложила оригинальную теорему о фиксированной точке, спасая доказательство несостоятельности первоначального лямбда-исчисления Чёрча. Первоначальное лямбда-исчисление церкви пострадало от парадокса типа Рассела. Модифицированное лямбда-исчисление позволило избежать этой проблемы. Клини изучил доказательство несоответствия, вероятно, чтобы увидеть, как модифицированное лямбда-исчисление будет страдать от аналогичной проблемы, и превратил доказательство несоответствия в полезную теорему модифицированного лямбда-исчисления. Благодаря своей работе по эквивалентности исчисления лямбад с другими моделями вычислений (машинами Тьюринга, рекурсивными функциями и т. Д.) Он перенес его в другие модели вычислений.

Как вывести оператора вы можете спросить? Вот как я это запомнил. Теорема о неподвижной точке об удалении самоссылки.

Все знают парадокс лжеца:

Я логово.

Или в более лингвистической форме:

Это предложение неверно.

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

Если вы напишите следующую цитату дважды, во второй раз внутри кавычек, полученное предложение будет ложным: «Если вы напишите следующую цитату дважды, во второй раз внутри кавычек, полученное предложение будет ложным:»

Нет ссылки на себя, у нас есть инструкции о том, как создать предложение, а затем что-то с ним сделать. И построенное предложение равно инструкции. Обратите внимание, что в калькуляции нам не нужны кавычки, потому что нет различия между данными и инструкциями. $\lambda$

Теперь, если мы проанализируем это, у нас есть где - это инструкции, чтобы построить и что-то с ним сделать. $MM$ $Mx$ $xx$

$Mx = f(xx)$

Итак, есть и мы имеем $M$ $\lambda x. f(xx)$

$MM = (\lambda x. f(xx))(\lambda x. f(xx))$

Это для фиксированного . Если вы хотите сделать это оператором, мы просто добавим и получим : $f$ $\lambda f$ $Y$

$Y = \lambda f. (MM) = \lambda f.((\lambda x. f(xx))(\lambda x. f(xx)))$

Так что я просто иметь в виду , парадокс без самоссылки , и это помогает мне понять , что о. $Y$

Кава
источник

3

Таким образом, вам нужно определить комбинатор с фиксированной точкой

fix f = f (fix f)
      = f (f (fix f))
      = f (f (f ... ))

но без явной рекурсии. Начнем с самого простого неприводимого комбинатора

omega = (\x. x x) (\x. x x)
      = (\x. x x) (\x. x x)
      = ...

В xпервой лямбде многократно подставляется вторая лямбда. Простое альфа-преобразование делает этот процесс более понятным:

omega =  (\x. x x) (\x. x x)
      =α (\x. x x) (\y. y y)
      =β (\y. y y) (\y. y y)
      =α (\y. y y) (\z. z z)
      =β (\z. z z) (\z. z z)

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

(\x. f (x x)) (\y. y y)

fбудет всплывать

f ((\y. y y) (\y. y y))

Мы получили нашу omegaспину. Теперь должно быть ясно, что, если мы добавим a fко второй лямбде, то fпоявится в первой лямбде, а затем она подпрыгнет:

Y f = (\x. x x)     (\x. f (x x))
      (\x. f (x x)) (\x. f (x x)) -- the classical definition of Y

поскольку

(\x. s t) z = s ((\x. t) z), if `x' doesn't occur free in `s'

мы можем переписать выражение как

f ((\x. x x) (\x. f (x x))

который просто

f (Y f)

и мы получили наше уравнение Y f = f (Y f). Таким образом, Yкомбинатор по существу

удвоить f
сделать первый fподпрыгнул
повторение

user3237465
источник

2

Возможно, вы видели классический пример уравнения без нормальной формы:

(λ Икс, Икс Икс) (λ Икс, Икс Икс) ▹ (λ Икс, Икс Икс) (λ Икс, Икс Икс)

$(\lambda x.xx)(\lambda x.xx) \triangleright (\lambda x.xx)(\lambda x.xx)$

Аналогичное уравнение предлагается для общей рекурсии:

\begin{matrix} (A) & \begin{array}{rr} (λ x . R (x x)) (λ x . R (x x)) \\ ▹ & R ((λ x . R (x x)) (λ x . R (x x))) \\ ▹ & R (R ((λ x . R (x x)) (λ x . R (x x)))) \\ ▹ & \dots \end{array} \end{matrix}

$\begin{array} {rr} & (\lambda x.R(xx))(\lambda x.R(xx)) ~\\ \triangleright & R(~ (\lambda x.R(xx))(\lambda x.R(xx))~) \\ \triangleright & R(R(~ (\lambda x.R(xx))(\lambda x.R(xx))~)) \\ \triangleright & \dots \end{array} \tag{A}$

$Yf = f(Yf)$ $f$ $R$

Y f = (λ x . f (x x)) (λ x . f (x x))

$Yf = (\lambda x.f(xx))(\lambda x.f(xx))$

Y = λ f . (λ x . f (x x)) (λ x . f (x x))

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

DanielV
источник

Понятный, интуитивно понятный вывод комбинатора с фиксированной точкой (Y комбинатор)?

Ответы: