Calcolo lambda non tipizzato: Perché il valore call-by-value è rigoroso?

Question

Calcolo lambda non tipizzato: Perché il valore call-by-value è rigoroso?

#1 da (5 voti)

5

Attualmente sto leggendo "Tipi e linguaggi di programmazione" di Benjamin C. Pierce. Prima di entrare veramente nella teoria dei tipi, spiega il calcolo lambda e le strategie di valutazione.

Sono un po 'confuso dalla spiegazione di chiama per nome vs chiama per valore in questo contesto.

Le due strategie sono spiegate nel modo seguente:

chiama per nome

Come ordine normale in quanto sceglie prima il redex più a sinistra, più esterno, ma più restrittivo non consentendo riduzioni all'interno delle astrazioni. Un esempio:

  id (id (λz. id z))
→ id (λz. id z)
→ λz. id z

chiama per valore

Solo i redex più esterni vengono ridotti e un redex viene ridotto solo quando il suo lato destro è già stato ridotto a un valore, un termine che è terminato nell'elaborazione e non può essere ulteriormente ridotto. Un esempio:

  id (id (λz. id z))
→ id (λz. id z)
→ λz. id z

(identical to the call by name evaluation)

Ok, finora tutto bene. Ma questo è seguito dal seguente paragrafo:

The call-by-value strategy is strict, in the sense that the arguments to functions are always evaluated, whether or not they are used by the body of the function. In contrast, non-strict (or lazy) strategies such as call-by-name and call-by-need evaluate only the arguments that are actually used.

So che cosa significa call-by-value e call-by-name praticamente, dall'aver usato (tra gli altri) C e Haskell, ma non riesco a capire perché la strategia di valutazione spiegata sopra porti a questo nel calcolo lambda. Si tratta di una regola aggiuntiva che accompagna sempre call-by-value o se segue la strategia di riduzione sopra descritta?

Specialmente dal momento che i passaggi di riduzione negli esempi sono identici, non riesco a vedere la differenza tra le due strategie e mi piacerebbe se qualcuno potesse aiutarmi a ottenere qualche intuito.

lambda

posta beta 27.05.2013 - 18:23

fonte

1 risposta

Leggi altre domande sui tag lambda

Quando si progetta una struttura di directory, i nomi dei file dovrebbero includere i nomi delle cartelle? Cosa significa per un algoritmo convergere?

score 5 · Accepted Answer

Sì, la strategia di valutazione come descritta porta a una semantica rigorosa, e gli esempi sono scelti in modo spettacolare per nascondere la differenza tra le due semantiche. Penso che vada qualcosa del genere:

id (id (λz. id z))  # strict means we evaluate the right hand side
→ id (λz. id z)     # RHS has been reduced (id (λz. id z)) → (λz. id z) by inner id 
→ λz. id z          # now we have called the outer id to obtain the final value

id (id (λz. id z))  # normal form means we call the outer id and pass RHS as a closure
→ id (λz. id z)     # outer id just returned its argument unevaluated → id (λz. id z) 
→ λz. id z          # now same thing is repeated with inner id

Quindi i passaggi di derivazione sembrano sintatticamente gli stessi, ma stanno accadendo cose diverse. Sotto lo schema di valutazione pigro, id in realtà non forza la valutazione del suo argomento: restituisce semplicemente quell'argomento stesso. Quindi non solo id x e x producono lo stesso valore, ma sono in realtà equivalenti: id x produce realmente x stesso, e quindi x restituisce il suo valore più tardi quando effettivamente necessario. Allo stesso modo, id (id (λz. id z)) restituisce semplicemente il lato destro non valutato di (id (λz. id z)) .

Ciò che è confuso nell'esempio è che si basa sulla nidificazione della stessa funzione, che è solo id , in modo tale che due diverse riduzioni generino entrambi id (λz. id z) . In uno questo è solo una copia dell'espressione interna id , e nell'altro, è il valore dell'espressione interna, passato un argomento al% esterno% co_de.