Как я могу объяснить, что такое Ubuntu тому, кто никогда не слышал об этом? [закрыто]

Как новичок в комбинаторах, я нашел статью Майка Ваньера (спасибо Николасу Манкузо) очень полезной. Я хотел бы написать резюме, помимо документирования моего понимания, если бы оно могло помочь некоторым другим, я был бы очень рад.

От Crappy до Less Crappy

Используя факториал в качестве примера, мы используем следующую функцию almost-factorial для вычисления факториала числа x:

def almost-factorial f x = if iszero x
                           then 1
                           else * x (f (- x 1))

В приведенном выше псевдокоде almost-factorial принимает функцию f и число x (almost-factorial каррируется, поэтому его можно рассматривать как принимающее функцию f и возвращающее 1-арная функция).

Когда almost-factorial вычисляет факториал для x, он делегирует вычисление факториала для x - 1 функции f и накапливает этот результат с x (в этом случае он умножает результат на (x - 1) с х).

Это можно увидеть как almost-factorial принимает в дрянную версию факториальной функции (которая может рассчитывать только до числа x - 1) и возвращает менее дрянную версию факториал (который вычисляет до числа x). Как в следующем виде:

almost-factorial crappy-f = less-crappy-f

Если мы несколько раз передадим менее дрянную версию факториала в almost-factorial, мы в итоге получим желаемую факториальную функцию f. Где это можно рассматривать как:

almost-factorial f = f

Фиксированная точка

Тот факт, что almost-factorial f = f означает f, является фиксированной точкой функции almost-factorial.

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

Три функции

Для обобщения мы имеем нерекурсивную функцию fn (например, наше почти факториальное), у нас есть функция с фиксированной точкой fr (как и у нашего f), тогда что Y делает, когда вы даете Y fn, Y возвращает функция фиксированной точки из fn.

Итак, в итоге (упрощается, если предположить, что fr принимает только один параметр; x вырождается в x - 1, x - 2 ... в рекурсии):

• Определим вычисления ядра как fn : def fn fr x = ...accumulate x with result from (fr (- x 1)), это почти полезная функция - хотя мы не можем использовать fn напрямую на x, это будет полезно очень скоро. Этот нерекурсивный fn использует функцию fr для вычисления своего результата
• fn fr = fr, fr является точкой фиксации fn, fr является полезная функция , мы можем использовать fr в x, чтобы получить наш результат
• Y fn = fr, Y возвращает точка фиксации функции Y превращает нашу почти полезную функцию fn в полезную fr

Вывод Y (не включен)

Я пропущу вывод из Y и пойду к пониманию Y. В сообщении Майка Вайнера много деталей.

Форма Y

Y определяется как (в формате лямбда-исчисления ):

Y f = λs.(f (s s)) λs.(f (s s))

Если мы заменим переменную s слева от функций мы получаем

Y f = λs.(f (s s)) λs.(f (s s))
=> f (λs.(f (s s)) λs.(f (s s)))
=> f (Y f)

Так что действительно, результат (Y f) является точкой фиксации f.

Почему (Y f) работает?

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

def fn fr x = accumulate x (fr (- x 1))

начиная с fn fr = fr, мы продолжаем

=> accumulate x (fn fr (- x 1))
=> accumulate x (accumulate (- x 1) (fr (- x 2)))
=> accumulate x (accumulate (- x 1) (accumulate (- x 2) ... (fn fr 1)))

рекурсивное вычисление заканчивается, когда самый внутренний (fn fr 1) является базовым случаем, а fn не использует fr в расчет.

Снова глядя на Y:

fr = Y fn = λs.(fn (s s)) λs.(fn (s s))
=> fn (λs.(fn (s s)) λs.(fn (s s)))

Итак,

fr x = Y fn x = fn (λs.(fn (s s)) λs.(fn (s s))) x

Для меня магическими частями этой установки являются:

• fn и fr взаимозависимы друг от друга: fr «оборачивает» fn внутри, каждый раз, когда fr используется для вычисления x, он «порождает» («поднимает»?) An fn и делегирует вычисление этому fn (передавая само по себе fr и x); с другой стороны, fn зависит от fr и использует fr для вычисления результата меньшей задачи x-1.
• В то время, когда fr используется для определения fn (когда fn использует fr в своих операциях), реальное fr еще не определено.
• Именно fn определяет реальную бизнес-логику. Основываясь на fn, Y создает fr - вспомогательную функцию в определенной форме - для облегчения вычисления для fn рекурсивным способом .

Это помогло мне понять Y таким образом на данный момент, надеюсь, это поможет.

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