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

cs.stackexchange https://cs.stackexchange.com/questions/9604

Вопрос

ИСПРАВЛЕНИЕ комбинатора с фиксированной точкой (он же Y-комбинатор) в (нетипизированном) лямбда-исчислении ($ \ lambda $) определяется как:

ИСПРАВЬТЕ $ riangleq \lambda f.(\лямбда x.f~(\лямбда y.x~x~y))~(\лямбда x.f~(\лямбда y.x~x~y))$

Я понимаю его назначение и могу прекрасно отследить выполнение его приложения; Я хотел бы понять, как вывести ИСПРАВЛЕНИЕ из первых принципов.

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

  1. ИСПРАВЛЕНИЕ - это функция:ИСПРАВИТЬ $\ triangleq \lambda_\ldots$
  2. ИСПРАВЛЕНИЕ использует другую функцию, $ f $, чтобы сделать ее рекурсивной:ИСПРАВИТЬ $ riangleq \lambda f._\ldots$
  3. Первый аргумент функции $f$ - это "имя" функции, используемое там, где предполагается рекурсивное приложение.Следовательно, все появления первого аргумента в $ f $ должны быть заменены функцией, и эта функция должна ожидать остальные аргументы в $ f $ (давайте просто предположим, что $ f $ принимает один аргумент):ИСПРАВЬТЕ $ riangleq \lambda f._\ldots f~(\lambda y._\лдоты у)$

Вот тут-то я и не знаю, как "сделать шаг" в своих рассуждениях.Маленькие многоточия указывают, где в моем ИСПРАВЛЕНИИ чего-то не хватает (хотя я могу узнать это, только сравнив его с "реальным" ИСПРАВЛЕНИЕМ).

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

Это было полезно?

Решение

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

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

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

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

$$f = \нижняя скоба{(\лямбда r .(\ldots r \ldots r \ldots))}_{M} f$$

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

$$f = \нижняя скоба{(\лямбда r .(\ldots r \ldots r \ldots))}_{M} \нижняя скоба{(\лямбда r .(\ldots r \ldots r \ldots))}_{M}$$

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

$$f = \нижняя скоба{(\лямбда r .(\ldots (rr) \ldots (rr) \ldots))}_{M'} \нижняя скоба{(\лямбда r .(\ldots (rr) \ldots (rr) \ldots))}_{M'}$$

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

$$f = (\лямбда x.\нижняя скобка{(\лямбда 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(xx)) (\лямбда x.m(xx))$$

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

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

Другие советы

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

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

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

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

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

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

Я и есть логово.

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

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

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

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

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

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

$Mx = f(xx)$

Итак, $M$ - это $\лямбда x.f (xx)$ и мы имеем

$MM = (\лямбда x.f(xx))(\лямбда x.f(xx))$

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

$Y = \лямбда f.(ММ) = \лямбда f.((\лямбда x.f(xx))(\лямбда x.f(xx)))$

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

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

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 Назад.Теперь должно быть ясно, что если мы добавим 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 комбинатор - это, по сути,

  1. удвойте f
  2. сделайте первый f подпрыгнувший
  3. повторять

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

$$(\лямбда x.xx) (\лямбда x.xx) riangleright (\лямбда x.xx)(\лямбда x.xx)$$

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

$$\begin{array} {rr} & (\лямбда x.R(xx))(\лямбда x.R(xx)) ~\\ riangleright & R(~ (\лямбда x.R(xx))(\лямбда x.R(xx))~) \\ riangleright & R(R(~ (\лямбда x.R(xx))(\лямбда x.R(xx))~)) \\ riangleright & \точки \end{массив} \тег{A}$$

(А) это способ написания общих рекурсивных уравнений в лямбда-исчислении (помимо примитивно-рекурсивного).Итак, как вы решаете уравнение $ Yf = f (Yf) $ ?Подключите $ f $ к $ R $ в приведенном выше уравнении, чтобы получить:

$$Yf = (\лямбда x.f(xx))(\лямбда x.f(xx))$$ $$Y = \лямбда f.(\лямбда x.f(xx))(\лямбда x.f(xx))$$

Лицензировано под: CC-BY-SA с атрибуция
Не связан с cs.stackexchange
scroll top