Jak używać poprawki i jak to działa?

Byłem trochę zdezorientowany dokumentacją fix(chociaż myślę, że rozumiem teraz, co ma robić), więc spojrzałem na kod źródłowy. To mnie bardziej zdezorientowało:

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

Jak dokładnie zwraca to stały punkt?

Postanowiłem wypróbować to w linii poleceń:

Prelude Data.Function> fix id
...

I tam wisi. Aby być uczciwym, to jest na moim starym Macbooku, który jest trochę powolny. Jednak ta funkcja nie może być zbyt kosztowna obliczeniowo, ponieważ cokolwiek przekazane do id zwraca to samo (nie wspominając o tym, że nie pochłania czasu procesora). Co ja robię źle?

Nie robisz nic złego. fix idjest nieskończoną pętlą.

Kiedy mówimy, że fixzwraca najmniej ustalony punkt funkcji, mamy na myśli to w sensie teorii domeny . Więc fix (\x -> 2*x-1)się nie wróci 1, bo chociaż 1jest stałym punktem tej funkcji, to nie jest przynajmniej jeden w zamawiania domeny.

Nie mogę opisać kolejności domen w jednym lub dwóch akapitach, więc odsyłam do powyższego linku do teorii domen. Jest to doskonały samouczek, łatwy do odczytania i dość pouczający. Gorąco polecam.

W przypadku widoku z wysokości 10 000 stóp fixjest to funkcja wyższego rzędu, która koduje ideę rekursji . Jeśli masz wyrażenie:

let x = 1:x in x

Co daje nieskończoną listę [1,1..], możesz powiedzieć to samo, używając fix:

fix (\x -> 1:x)

(Lub po prostu fix (1:)), które mówi: znajdź mi stały punkt (1:)funkcji, IOW wartość xtaką, że x = 1:x... tak jak zdefiniowaliśmy powyżej. Jak widać z definicji, fixto nic innego jak ta idea - rekursja zamknięta w funkcji.

Jest to również prawdziwie ogólna koncepcja rekurencji - w ten sposób można napisać dowolną funkcję rekurencyjną, w tym funkcje wykorzystujące rekursję polimorficzną . Na przykład typowa funkcja Fibonacciego:

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

Można napisać w fixten sposób:

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

Ćwiczenie: rozwiń definicję, fixaby pokazać, że te dwie definicje fibsą równoważne.

Ale dla pełnego zrozumienia przeczytaj o teorii domeny. To naprawdę fajne rzeczy.

Nie twierdzę, że w ogóle to rozumiem, ale jeśli to komuś pomaga ...

Rozważ definicję fix. fix f = let x = f x in x. Zadziwiająca część xjest zdefiniowana jako f x. Ale pomyśl o tym przez chwilę.

x = f x

Ponieważ x = fx, możemy podstawić wartość xpo prawej stronie tego, prawda? Więc dlatego...

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.

Tak więc sztuczka polega na tym, że aby zakończyć, ftrzeba wygenerować jakąś strukturę, tak aby późniejszy fwzorzec mógł dopasować tę strukturę i zakończyć rekursję, bez faktycznego dbania o pełną "wartość" swojego parametru (?)

Chyba że, oczywiście, chcesz zrobić coś takiego, jak stworzenie nieskończonej listy, jak zilustrowano luqui.

Silnia wyjaśnienia TomMD jest dobra. Podpis typu poprawki to (a -> a) -> a. Innymi słowy, typ podpisu dla (\recurse d -> if d > 0 then d * (recurse (d-1)) else 1)to . Więc możemy tak powiedzieć . W ten sposób fix przyjmuje naszą funkcję, która jest lub naprawdę, i zwróci wynik typu , innymi słowy, inną funkcję!(b -> b) -> b -> b(b -> b) -> (b -> b)a = (b -> b)a -> a(b -> b) -> (b -> b)ab -> b

Czekaj, myślałem, że powinien zwrócić stały punkt ... a nie funkcję. Cóż, w pewnym sensie (ponieważ funkcje to dane). Możesz sobie wyobrazić, że dało nam to ostateczną funkcję znajdowania silni. Daliśmy mu funkcję, która nie wiedziała, jak się powtarzać (stąd jeden z jej parametrów jest funkcją używaną do rekurencji), i fixnauczyliśmy ją, jak się powtarzać.

Pamiętasz, jak powiedziałem, że fmusi wygenerować jakąś strukturę, aby później fmożna było dopasować wzorzec i zakończyć? Cóż, to chyba nie do końca w porządku. TomMD zilustrował, jak możemy rozszerzyć, xaby zastosować funkcję i przejść do przypadku podstawowego. Do swojej funkcji użył warunku if / then i to właśnie powoduje zakończenie. Po wielokrotnych zamianach inczęść całej definicji fixostatecznie przestaje być definiowana w kategoriach xi wtedy jest obliczalna i kompletna.

Potrzebujesz sposobu na zakończenie działania punktu stałego. Rozszerzając swój przykład, oczywiste jest, że się nie skończy:

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

Oto prawdziwy przykład użycia poprawki (uwaga, nie używam poprawki często i prawdopodobnie byłem zmęczony / nie martwiłem się o czytelny kod, kiedy to pisałem):

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

WTF, mówisz! Cóż, tak, ale jest tutaj kilka naprawdę przydatnych punktów. Po pierwsze, pierwszym fixargumentem powinna być zwykle funkcja, która jest przypadkiem „rekurencyjnym”, a drugim argumentem są dane, na których należy działać. Oto ten sam kod, co nazwana funkcja:

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

Jeśli nadal jesteś zdezorientowany, być może silnia będzie łatwiejszym przykładem:

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

Zwróć uwagę na ocenę:

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

Och, czy właśnie to widziałeś? Stało xsię to funkcją w naszym thenoddziale.

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 -->

W powyższym trzeba pamiętać x = f x, stąd dwa argumenty x 2na końcu zamiast po prostu 2.

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

I tu się zatrzymam!

Jak rozumiem, znajduje wartość dla funkcji, taką, że wyprowadza to samo, co mu podajesz. Haczyk polega na tym, że zawsze wybierze undefined (lub nieskończoną pętlę, w haskell, undefined i infinite loop są takie same) lub cokolwiek, co ma najwięcej niezdefiniowanych w sobie. Na przykład z id,

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

Jak widać, undefined jest punktem stałym, więc fixwybierzemy to. Jeśli zamiast tego zrobisz (\ x-> 1: x).

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

Więc fixnie można wybrać niezdefiniowanego. Aby był nieco bardziej połączony z nieskończonymi pętlami.

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

Znowu niewielka różnica. Więc jaki jest punkt stały? Spróbujmy 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

To jest to samo! Ponieważ jest to jedyny stały punkt, fixnależy się na nim ustalić. Przepraszamy fix, nie ma dla ciebie nieskończonych pętli lub niezdefiniowanych.