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

Question

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

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

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

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

Prelude Data.Function> fix id 
... 

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

Answer 1

Вы ничего не делаете неправильно. fix id - бесконечный цикл.

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

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

Для просмотра с 4400 по 30 000, fix является функцией более высокого порядка, которая кодирует идею рекурсии. Если у вас есть выражение:

let x = 1:x in x 

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

fix (\x -> 1:x) 

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

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

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 эквивалентны.

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

Answer 2

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

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 

WTF, вы говорите! Ну, да, но здесь есть несколько действительно полезных моментов. Прежде всего, ваш первый аргумент 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 --> 

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

Answer 3

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

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

x = f x 

Так как X = F х, то мы можем подставить значение 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 может сопрягать образец, структура и прекращает рекурсию, фактически не заботясь о полное «значение» его параметра (?)

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

Факторное объяснение TomMD хорошее. Подпись типа Fix - (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). Таким образом, исправление принимает нашу функцию, которая равна a -> a, или действительно, (b -> b) -> (b -> b), и вернет результат типа a, другими словами, b -> b, другими словами, еще одна функция!

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

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

Answer 4

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

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

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

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

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

λ <*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, никаких бесконечных циклов или неопределенных для вас.

Answer 5

Одно ясно определение You could have re-invented fix too!