Cosa sono le "semantiche di riduzione"? Si prega di spiegare l'uso di PLT Redex in termini profani

Question

Qualcuno può spiegare l'uso della semantica di riduzione e il PLT Redex in un linguaggio più semplice.

Grazie.

Answer 1

semantica riduzione è una tecnica di calcolo, che prevede la sostituzione un'espressione con un equivalente (e auspicabilmente più piccolo) espressione fino a eliminare sostituzione è possibile. Se una lingua è completa da Turing, ci sono espressioni che non smettono mai di essere sostituite.

riduzione è di solito notata da una freccia a destra, ed è meglio spiegato con l'esempio:

(3 + 7) + 5 --> 10 + 5 --> 15 

Questo dimostra la semantica standard di riduzione per le espressioni aritmetiche. L'espressione 15 non può essere ulteriormente ridotta.

Spero che questo aiuti.

Answer 2

La semantica di riduzione è simile (se non uguale?) Alla semantica contestuale. Qualsiasi espressione può essere suddivisa in un contesto e redex.

Fondamenti pratici di Robert Harper per i linguaggi di programmazione (bozza PDF disponibile here) sezione 9.3 La Semantica contestuale fa un lavoro decente nel spiegarli.

Un esempio:

print 5+4 
**context: print [], redex: 5+4 
**evaluate redex: 9 
**plug back into context 

print 9 
**context: [], redex: print 9 
**evaluate redex: nil ==> 9 
**plug back into context 

nil 

Si puo 'bastone' la Redex di nuovo nel 'buco' di contesto per ottenere: stampa 5 + 4. La valutazione avviene al redex. Rompi un'espressione in un contesto + redex, valuta il redex per ottenere una nuova espressione, ricollegala nel contesto, risciacqua e ripeti.

Ecco un esempio leggermente più complicato che richiede la conoscenza di una macchina astratta che valuta il lambda calcolo:

(lambda x.x+1) 5 
**context: [] 5, redex: (lambda x.x+1) 
**evaluate redex: <(lambda x.x+1), {environment}> <- create a closure 
**plug back into context 

<(lambda x.x+1), {}> 5 
**context: [], redex: <(lambda x.x+1), {}> 5 
**evaluate redex: x+1 where x:=5 
**plug back into context 

x+1 where x:=5 
**context: []+1, redex: x 
**evaluate redex: 5 (since x:=5 in our environment) 
*plug back into context 

5+1... 
6 

EDIT: La parte difficile è riconoscere dove rompere un'espressione in un contesto & Redex. Richiede la conoscenza della semantica operativa della lingua (che 'pezzo' di un'espressione è necessario valutare successivamente).