什麼是「還原語義」？請解釋PLT Redex在外行人員中的使用

Question

有人請以更簡單的語言解釋簡化語義和PLT Redex的用法。

謝謝。

Answer 1

簡化語義學是一種計算技術，它涉及到用等效（有希望更小）的表達式代替表達式，直到不再有可能的替換。如果一種語言是圖靈完備的，那麼表達式永遠不會停止替換。

還原通常是通過一個右箭頭記譜，並且它最好通過實例說明：

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

此示出了用於算術表達式標準還原語義。表達式15不能再減少。

希望這會有所幫助。

Answer 2

約簡語義與上下文語義相似（如果不是相同？）。任何表達式都可以分解爲一個上下文並進行redex。

羅伯特哈珀的編程語言實踐基礎（草案PDF可用here）第9.3節語境語義學做了一個體面的工作來解釋它們。

一個例子：

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 

你可以用「杖」的歸約回上下文的「洞」來獲得：打印5 + 4。評估發生在redex。您將表達式分解爲上下文+ redex，評估redex以獲取新表達式，將其插回到上下文中，然後再重複。

這裏的一個稍微複雜的實施例，需要一個抽象機，用於評估演算的知識：

(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 

編輯：棘手的部分是識別其中打破的表達到上下文&歸約式。它需要知道該語言的操作語義（下一步需要評估的表達式）。