Dlaczego rekursywne `let` make space effcient?

Question

znalazłem to oświadczenie podczas studiów funkcyjną reagującą Programowanie, z "Plugging a Space Leak with an Arrow" przez Hai Liu i Pawła Hudák (strona 5):

Suppose we wish to define a function that repeats its argument indefinitely: 

    repeat x = x : repeat x 

or, in lambdas: 

    repeat = λx → x : repeat x 

This requires O(n) space. But we can achieve O(1) space by writing instead: 

    repeat = λx → let xs = x : xs 
        in xs 

Różnica tutaj wydaje się niewielka, ale niezwykle skłania efektywności przestrzeni. Dlaczego i jak to się dzieje? Najlepszym przypuszczenie Zrobiłem to ocenić je ręcznie:

r = \x -> x: r x 
    r 3 

    -> 3: r 3 
    -> 3: 3: 3: ........ 
    -> [3,3,3,......] 

Jak wyżej, musimy tworzyć nieskończone nowe łącznikami dla tych rekursji. Wtedy staram się ocenić drugi:

r = \x -> let xs = x:xs in xs 
    r 3 

    -> let xs = 3:xs in xs 
    -> xs, according to the definition above: 
    -> 3:xs, where xs = 3:xs 
    -> 3:xs:xs, where xs = 3:xs 

W drugiej postaci wyświetleniu xs i mogą być dzielone pomiędzy każdymi miejscach występujących, więc myślę, że dlatego możemy wymagać tylko O(1) spacji zamiast O(n). Ale nie jestem pewien, czy mam rację, czy nie.

BTW: słowo kluczowe „shared” pochodzi z tej samej gazety Strona 4:

Problem polega na tym, że standardowe call-by-potrzebie zasady oceny są w stanie rozpoznać, że funkcja:

f = λdt → integralC (1 + dt) (f dt) 

jest taka sama, jak:

f = λdt → let x = integralC (1 + dt) x in x 

były definicja de fi przyczyny pracować, aby być repea w rekurencyjnym wywołaniu do f, podczas gdy w tym drugim przypadku obliczenia są udostępniane.

Answer 1

To najłatwiejszy do zrozumienia ze zdjęciami:

• Pierwsza wersja

  repeat x = x : repeat x 
  

  tworzy łańcuch konstruktorów (:) kończących się thunk, który zastąpi się większą liczbą konstruktorów, gdy ich zażądasz. Tak więc przestrzeń O (n).

  

• Druga wersja

  repeat x = let xs = x : xs in xs 
  

  wykorzystuje let do "wiązania węzła", tworząc pojedynczy (:) konstruktora, który odnosi się do siebie.

  

Answer 2

Mówiąc prościej, zmienne są udostępniane, ale aplikacje funkcyjne nimi nie są. W

repeat x = x : repeat x 

jest to przypadek (z perspektywy języku), że (ko) rekurencyjne wywołanie powtórzyć to z tym samym argumentem. Tak więc, bez dodatkowej optymalizacji (która nazywa się statyczną transformacją argumentów), funkcja będzie ponownie wywoływana.

Ale kiedy piszesz

repeat x = let xs = x : xs in xs 

nie ma rekurencyjne funkcyjne połączeń. Bierzesz numer x i używasz wartości cyklicznej xs. Wszystkie udostępnianie jest jawne.

Jeśli chcesz zrozumieć to bardziej formalnie, musisz zapoznać się z semantyką leniwego oceniania, taką jak A Natural Semantics for Lazy Evaluation.

Answer 3

Twoja intuicja o współdzieleniu xs jest poprawna. Przekształcania przykład autora pod względem powtórzenia, zamiast integralną, gdy piszesz:

repeat x = x : repeat x 

język nie uznają, że repeat x po prawej stronie jest taka sama jak wartość wytwarzanego przez wyrażenie x : repeat x.Natomiast jeśli piszesz

repeat x = let xs = x : xs in xs 

jesteś jawnie tworzyć strukturę, która gdy oceniano wygląda następująco:

{hd: x, tl:|} 
^   | 
\________/