Как использовать исправление и как оно работает?

87

Меня немного смутила документация для fix(хотя я думаю, что понимаю, что она должна делать сейчас), поэтому я посмотрела исходный код. Это сбило меня с толку:

fix :: (a -> a) -> a
fix f = let x = f x in x

Как именно это возвращает фиксированную точку?

Решил опробовать в командной строке:

Prelude Data.Function> fix id
...

И он там висит. Честно говоря, это мой старый macbook, который работает медленно. Однако эта функция не может быть слишком затратной с точки зрения вычислений, поскольку все, что передается в id, возвращает то же самое (не говоря уже о том, что это не потребляет процессорного времени). Что я делаю не так?

Джейсон Бейкер
источник
68
Ответ на шутку звучит так: «Исправление бесполезно, оно просто есть, чтобы вы могли ввести fix errorghci и почувствовать себя хорошо».
Thomas M. DuBuisson
3
@TomMD - Забавно. Я запомню это, если кто-нибудь когда-нибудь спросит меня, что делает fix, и я почувствую себя озлобленным. :-)
Джейсон Бейкер
2
Я обычно пишу fixкак fix f = f (fix f). Коротко, просто, работает и идентично математическому определению.
newacct
20
@newacct, да, я тоже так думаю. Но тот, что здесь, может привести к более эффективным структурам. Вы можете увидеть разницу , если оценивать, скажем, fix (1:) !! (10^8). Оригинал делает это в постоянной памяти, ваша - в линейной (что тоже немного медленнее). То есть использование let «связывает более тесный узел» и позволяет создавать круговую структуру данных, тогда как ваша - нет.
luqui
22
Вы тоже могли бы изобрести заново fix! помогли мне понять fixмногое.
fredoverflow

Ответы:

90

Вы не делаете ничего плохого. fix idэто бесконечный цикл.

Когда мы говорим, что fixвозвращает наименьшую фиксированную точку функции, мы имеем в виду это в смысле теории предметной области . Так fix (\x -> 2*x-1)что не вернется 1, потому что, хотя и 1является фиксированной точкой этой функции, она не последняя в упорядочивании доменов.

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

Для обзора с высоты 10 000 футов fix- это функция высшего порядка, которая кодирует идею рекурсии . Если у вас есть выражение:

let x = 1:x in x

В результате получается бесконечный список [1,1..], вы можете сказать то же самое, используя fix:

fix (\x -> 1:x)

(Или просто fix (1:)), который говорит, что найдите мне фиксированную точку (1:)функции, IOW значение, xтакое, что x = 1:x... точно так же, как мы определили выше. Как видно из определения, fixэто не более чем идея - рекурсия, инкапсулированная в функцию.

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

fib n = if n < 2 then n else fib (n-1) + fib (n-2)

Можно записать fixтак:

fib = fix (\f -> \n -> if n < 2 then n else f (n-1) + f (n-2))

Упражнение: расширьте определение, fixчтобы показать, что эти два определения fibэквивалентны.

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

Луки
источник
32
Вот похожий способ подумать fix id: fixпринимает функцию типа a -> aи возвращает значение типа a. Поскольку idявляется полиморфным для любого a, fix idбудет иметь свой тип a, т.е. любое возможное значение. В Haskell единственным значением, которое может быть любого типа, является bottom, ⊥, и оно неотличимо от непрерывного вычисления. Таким образом fix idвыдает именно то, что должно, нижнее значение. Опасность fixсостоит в том, что если ⊥ - фиксированная точка вашей функции, то она по определению является наименее фиксированной точкой, поэтому fixне завершится.
John L
4
@JohnL в Haskell undefinedтакже является значением любого типа. Вы можете определить , fixкак: fix f = foldr (\_ -> f) undefined (repeat undefined).
didest
1
@Diego ваш код эквивалентен _Y f = f (_Y f).
Will Ness
25

Я вообще не утверждаю, что понимаю это, но если это кому-то поможет ... тогда ура.

Рассмотрим определение fix. fix f = let x = f x in x. Ошеломляющая часть - это то, что xопределяется как f x. Но подумайте об этом на минуту.

x = f x

Поскольку x = fx, то мы можем подставить значение xв правую часть этого, верно? И поэтому...

x = f . f $ x -- or x = f (f x)
x = f . f . f $ x -- or x = f (f (f x))
x = f . f . f . f . f . f . f . f . f . f . f $ x -- etc.

Таким образом, трюк состоит в том, что для завершения fнеобходимо сгенерировать какую-то структуру, чтобы более поздний fвариант мог сопоставить эту структуру с шаблоном и завершить рекурсию, фактически не заботясь о полном «значении» его параметра (?)

Если, конечно, вы не хотите создать бесконечный список, как проиллюстрировал Луки.

Факториальное объяснение TomMD хорошее. Подпись типа исправления (a -> a) -> a. Тип подписи для (\recurse d -> if d > 0 then d * (recurse (d-1)) else 1)это (b -> b) -> b -> b, другими словами, (b -> b) -> (b -> b). Так что мы можем так сказать a = (b -> b). Таким образом, fix принимает нашу функцию, которая есть a -> aили действительно, (b -> b) -> (b -> b)и возвращает результат типа a, другими словами, b -> bдругими словами, другую функцию!

Подождите, я думал, он должен возвращать фиксированную точку ... а не функцию. Ну, вроде как (поскольку функции - это данные). Вы можете представить, что это дало нам окончательную функцию для нахождения факториала. Мы дали ему функцию, которая не знает, как выполнять рекурсию (следовательно, одним из параметров для нее является функция, используемая для рекурсии), и fixнаучили ее, как выполнять рекурсию.

Помните, как я сказал, что fэто должно создать какую-то структуру, чтобы более поздняя fверсия могла соответствовать шаблону и завершаться? Думаю, это не совсем так. TomMD проиллюстрировал, как мы можем расширить, xчтобы применить функцию и перейти к базовому случаю. Для своей функции он использовал if / then, что и вызывает завершение. После повторных замен inчасть всего определения в fixконечном итоге перестает определяться в терминах, xи именно тогда она становится вычислимой и полной.

Дэн Бертон
источник
Спасибо. Это очень полезное и практичное объяснение.
kizzx2 04
17

Вам нужен способ отключения фиксированной точки. Расширяя ваш пример, очевидно, что он не закончится:

fix id
--> let x = id x in x
--> id x
--> id (id x)
--> id (id (id x))
--> ...

Вот реальный пример того, как я использую исправление (обратите внимание, я не часто использую исправление и, вероятно, устал / не беспокоился о читаемом коде, когда писал это):

(fix (\f h -> if (pred h) then f (mutate h) else h)) q

Ты говоришь, черт возьми! Что ж, да, но здесь есть несколько действительно полезных моментов. Прежде всего, вашим первым fixаргументом обычно должна быть функция, которая является «рекурсивным» случаем, а второй аргумент - это данные, с которыми нужно действовать. Вот тот же код, что и названная функция:

getQ h
      | pred h = getQ (mutate h)
      | otherwise = h

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

fix (\recurse d -> if d > 0 then d * (recurse (d-1)) else 1) 5 -->* 120

Обратите внимание на оценку:

fix (\recurse d -> if d > 0 then d * (recurse (d-1)) else 1) 3 -->
let x = (\recurse d -> if d > 0 then d * (recurse (d-1)) else 1) x in x 3 -->
let x = ... in (\recurse d -> if d > 0 then d * (recurse (d-1)) else 1) x 3 -->
let x = ... in (\d -> if d > 0 then d * (x (d-1)) else 1) 3

О, вы только что это видели? Это xстало функцией внутри нашей thenветки.

let x = ... in if 3 > 0 then 3 * (x (3 - 1)) else 1) -->
let x = ... in 3 * x 2 -->
let x = ... in 3 * (\recurse d -> if d > 0 then d * (recurse (d-1)) else 1) x 2 -->

Вышеупомянутое вам необходимо запомнить x = f x, поэтому два аргумента x 2в конце вместо просто 2.

let x = ... in 3 * (\d -> if d > 0 then d * (x (d-1)) else 1) 2 -->

И я остановлюсь здесь!

Томас М. ДюБюиссон
источник
Ваш ответ действительно fixимел для меня смысл. Мой ответ во многом зависит от того, что вы уже сказали.
Дэн Бертон
@Thomas, обе ваши редукционные последовательности неверны. :) id xпросто сокращается до x(которое затем снова сокращается до id x). - Затем, во 2-м примере ( fact), когда xпреобразователь запускается впервые, полученное значение запоминается и повторно используется. Пересчет (\recurse ...) xпроизойдет с определением отсутствия совместного использованияy g = g (y g) , а не с этим определением совместного использованияfix . - Я сделал пробную правку здесь - вы можете ее использовать, или я могу внести правку, если вы одобряете.
Will Ness
на самом деле, когда fix idсокращается, let x = id x in xтакже заставляет значение приложения id xвнутри letкадра (преобразователя), поэтому оно сокращается до let x = x in x, и this зацикливается. Похоже на то.
Will Ness
Верный. Мой ответ - это рассуждение по уравнениям. Отображение редукции а-ля Haskell, которая занимается порядком вычисления, только сбивает пример с толку без какой-либо реальной выгоды.
Thomas M. DuBuisson
1
Вопрос помечен как haskell, так и letrec (то есть рекурсивным let с разделением). В Haskell различие между fixи Y очень четкое и важное. Я не вижу, что хорошего в том, чтобы показать неправильный порядок сокращения, когда правильный еще короче, намного яснее и легче отслеживается и правильно отражает то, что на самом деле происходит.
Уилл Несс
3

Насколько я понимаю, он находит такое значение для функции, что выводит то же самое, что и вы. Загвоздка в том, что он всегда будет выбирать undefined (или бесконечный цикл, в haskell, undefined и бесконечные циклы одинаковы) или что-то, что содержит больше всего неопределенных значений. Например, с идентификатором

λ <*Main Data.Function>: id undefined
*** Exception: Prelude.undefined

Как видите, undefined - это фиксированная точка, поэтому fixвыберем ее. Если вы вместо этого сделаете (\ x-> 1: x).

λ <*Main Data.Function>: undefined
*** Exception: Prelude.undefined
λ <*Main Data.Function>: (\x->1:x) undefined
[1*** Exception: Prelude.undefined

Так что fixне могу выбрать undefined. Чтобы сделать его более связанным с бесконечными циклами.

λ <*Main Data.Function>: let y=y in y
^CInterrupted.
λ <*Main Data.Function>: (\x->1:x) (let y=y in y)
[1^CInterrupted.

Опять же небольшая разница. Так что же такое фиксированная точка? Давайте попробуем repeat 1.

λ <*Main Data.Function>: repeat 1
[1,1,1,1,1,1, and so on
λ <*Main Data.Function>: (\x->1:x) $ repeat 1
[1,1,1,1,1,1, and so on

Это то же самое! Поскольку это единственная фиксированная точка, fixнеобходимо на ней остановиться. Извините fix, для вас нет бесконечных циклов или undefined.

PyRulez
источник