Perchè ricorsivo "lasciamo" rendere lo spazio effciente?

Question

Ho trovato questa dichiarazione mentre studiava funzionale programmazione reattiva, da "Plugging a Space Leak with an Arrow" da Hai Liu e Paul Hudak (pagina 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 

La differenza qui sembra piccola, ma viene richiesto enormemente l'efficienza dello spazio. Perché e come succede? L'ipotesi migliore che ho fatto è quello di valutare loro mano:

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

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

Come sopra, avremo bisogno di creare infiniti nuovi thunk per queste ricorsione. Poi cerco di valutare il secondo:

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 

Nella seconda forma gli appare xs e possono essere condivisi tra tutti i luoghi che si verificano, quindi credo che sia il motivo per cui siamo in grado di richiedere solo O(1) spazi piuttosto che O(n). Ma non sono sicuro se ho ragione o no.

BTW: La parola chiave "condivisa" viene dalla stessa del giornale pagina 4:

Il problema qui è che le regole di valutazione standard di Call-by-necessità non sono in grado di riconoscere che la funzione:

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

è lo stesso:

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

l'ex definizione fi cause di lavoro per essere ripet ted nella chiamata ricorsiva a f, mentre in quest'ultimo caso il calcolo è condiviso.

Answer 1

E 'più facile da capire con le immagini:

• la prima versione

  repeat x = x : repeat x 
  

  crea una catena di costruttori (:) che termina con un thunk che si sostituirà con altri costruttori quando richiesto. Quindi, O (n) spazio.

  

• La seconda versione

  repeat x = let xs = x : xs in xs 
  

  utilizza let a "legare il nodo", creando un unico (:) costruttore che si riferisce a se stesso.

  

Answer 2

In parole semplici, le variabili sono condivise, ma le applicazioni di funzione no. In

repeat x = x : repeat x 

si tratta di una coincidenza (dal punto di vista del linguaggio) che il (co) chiamata ricorsiva a ripetere è con lo stesso argomento. Quindi, senza ulteriore ottimizzazione (che è chiamata trasformazione degli argomenti statici), la funzione verrà chiamata ancora e ancora.

Ma quando si scrive

repeat x = let xs = x : xs in xs 

non ci sono ricorsive funzione chiamate. Si prende un x e si costruisce un valore ciclico xs che lo utilizza. Tutta la condivisione è esplicita.

Se vuoi capirlo in modo più formale, devi familiarizzare con la semantica della valutazione lazy, come ad esempio A Natural Semantics for Lazy Evaluation.

Answer 3

L'intuizione su xs condivisa è corretta. Per ribadire l'esempio del dell'autore in termini di ripetizione, anziché integrale, quando si scrive:

repeat x = x : repeat x 

la lingua non riconosce che il repeat x sulla destra è lo stesso del valore prodotto dall'espressione x : repeat x.Mentre se si scrive

repeat x = let xs = x : xs in xs 

si sta creando in modo esplicito una struttura che quando valutato assomiglia a questo:

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