Haskell: Wspólna Corecursive Fallacies

Question

Więc myślałem o algorytm odległość wykres dzisiaj, i wpadł na ten podczas Jechałem w samochodzie:

module GraphDistance where 
import Data.Map 

distance :: (Ord a) => a -> Map a [a] -> Map a Int 
distance a m = m' 
    where m' = mapWithKey d m 
     d a' as = if a == a' then 0 else 1 + minimum (Prelude.map (m'!) as) 

Początkowo byłem dość dumny z siebie, ponieważ wydawało się takie eleganckie. Ale wtedy zdałem sobie sprawę, że to nie zadziała - corecursion może utknąć w pętli.

musiałem kodować go do siebie przekonać:

ghci> distance 1 $ fromList [(0,[1]),(1,[0,2]),(2,[1,3]),(3,[2])] 
fromList [(0,1),(1,0),(2,^CInterrupted. 

Ale teraz myślę, że dość dużo Przemyślałem to.

Czy istnieje lista typowych błędów i wzorców zapobiegawczych podczas radzenia sobie z danymi corecursive, które mogę przeczytać, , więc mogę wyszkolić mój mózg, by myśleć corecursively? Doświadczenie nauczyło mnie dość dobrze do przemyślenia nie-corecursive danych, ale chciałbym uczyć się od innych błędów, jeśli mogę.

Answer 1

Cóż, w przypadku danych corecursive istnieje naprawdę tylko jeden podstawowy błąd, a to bezużyteczne stosowanie rekursji!

Corecursion oznacza, że ​​dane są generowane przyrostowo w pewnym sensie. Funkcja wykresu odległości jest tu pouczająca, ponieważ wydaje się, że powinna działać powinna być, więc pomyśl o tym, gdzie powinna być część przyrostowa: Punktem początkowym jest odległość 0 od węzła do siebie, w przeciwnym razie większa od minimalnej odległości między własnych bezpośrednich sąsiadów. Tak więc, oczekiwalibyśmy, że każda wartość odległości będzie przyrostowa, co oznacza, że ​​potrzebujemy ich odpowiednio do rdzenia.

rekursji sporne, wówczas występuje ze względu na połączenie (+) i minimum: po znalezieniu minimum, 1 zawsze będzie mniej niż 1 + n, bez potrzeby martwić się o to, co n jest ... ale nie ma mowy porównać Int s bez obliczania całej wartości.

W skrócie, algorytm oczekuje, że będzie w stanie porównać, ile razy (1 +) został zastosowany do 0 tylko w razie potrzeby; to znaczy, chce, aby leniwe liczby naturalne były definiowane za pomocą "zera" i "następcy".

Oto:

data Nat = Z | S Nat 

natToInt :: Nat -> Int 
natToInt Z = 0 
natToInt (S n) = 1 + natToInt n 

instance Show Nat where show = show . natToInt 

instance Eq Nat where 
    Z == Z = True 
    (S n1) == (S n2) = n1 == n2 
    _ == _ = False 

    Z /= Z = False 
    (S n1) /= (S n2) = n1 /= n2 
    _ /= _ = True 


instance Ord Nat where 
    compare Z Z = EQ 
    compare Z (S _) = LT 
    compare (S _) Z = GT 
    compare (S n1) (S n2) = compare n1 n2 

A potem w GHCi:

> distance 1 $ fromList [(0,[1]),(1,[0,2]),(2,[1,3]),(3,[2])] 
fromList [(0,1),(1,0),(2,1),(3,2)] 

Dowód, że algorytm działa ^[0]; Twoja implementacja była po prostu niepoprawna.

---

Teraz, jako nieznaczną zmianę, niech zastosować algorytm do innego wykresu:

> distance 1 $ fromList [(0,[1]),(1,[0]),(2,[3]),(3,[2])] 

... czego oczekujemy to zrobić? Jaka jest odległość od węzła 1 dla węzłów 2 lub 3?

Running go w GHCi ma oczywisty wynik:

fromList [(0,1),(1,0),(2,^CInterrupted. 

Niemniej algorytm działa poprawnie na tym wykresie. Czy widzisz problem? Dlaczego zawiesił się w GHCi?

---

Podsumowując, należy wyraźnie rozróżnić dwie formy, które nie mogą być dowolnie mieszane:

• leniwy, ewentualnie nieskończonych danych, generowane corecursively
• danych skończony, spożywane rekurencyjnie

Obie formy można przekształcać w sposób niezależny od struktury (np. map działa na listach skończonych i nieskończonych). Codata może być konsumowana przyrostowo, dzięki algorytmowi corecursive; dane mogą być generowane rekurencyjnie, ograniczone przez algorytm rekursywny.

To, co nie może zrobić, to spożywać rekursywnie kodaty (np. Lewe fałdowanie nieskończonej listy) lub generować dane corecursively (rzadko w Haskell, z powodu lenistwa).

[0]: W przypadku niektórych danych wejściowych (np. Niektóre rozłączone wykresy) nie uda się, ale to inna sprawa.