Was sind "Reduktionssemantik"? Bitte erläutern Sie die Verwendung von PLT Redex in Laien-Begriff

Question

Jemand bitte erklären Sie die Verwendung der Reduktionssemantik und der PLT Redex in einfacher Sprache.

Danke.

Answer 1

Die Reduktionssemantik ist eine Berechnungstechnik, bei der einen Ausdruck durch einen äquivalenten (und hoffentlich kleineren) Ausdruck ersetzt, bis kein Ersatz mehr möglich ist. Wenn eine Sprache Turing abgeschlossen ist, gibt es Ausdrücke, die niemals aufhören zu ersetzen.

Die Reduktion wird in der Regel durch einen Pfeil nach rechts notiert, und es ist am besten durch Beispiel erklärt:

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

Damit wird die Standard-Reduktions Semantik für arithmetischen Ausdrücke zeigt. Der Ausdruck 15 kann nicht weiter reduziert werden.

Hoffe, das hilft.

Answer 2

Die Reduktionssemantik ist der kontextuellen Semantik ähnlich (wenn nicht identisch?). Jeder Ausdruck kann in einen Kontext und Redex aufgeteilt werden.

Robert Harpers praktische Grundlagen für Programmiersprachen (PDF-Version verfügbar here) Abschnitt 9.3 Kontext-Semantik macht eine anständige Aufgabe, sie zu erklären.

Ein Beispiel:

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 

Sie können 'Stock' die redex zurück in das 'Loch' des Kontextes zu erhalten: print 5 + 4. Die Auswertung erfolgt beim Redex. Sie brechen einen Ausdruck in einen Kontext + Redex, bewerten den Redex, um einen neuen Ausdruck zu erhalten, stecken ihn wieder in den Kontext, spülen und wiederholen.

Hier ist ein etwas komplizierteres Beispiel, das Wissen einer abstrakten Maschine erfordert, die das Lambda-Kalkül auswertet:

(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: Der schwierige Teil, wo erkennt einen Ausdruck in einen Kontext & redex zu brechen. Es erfordert Kenntnisse der operativen Semantik der Sprache (welches "Stück" eines Ausdrucks als nächstes zu bewerten ist).