異曲同工 - Church-Rosser and Consistency of Evaluation

    在「解釋語言的語言」中提到，設計一個新的語言，僅僅是使用meta-language給出其描述是不夠的，咱們還須要去驗證一些性質。
    考慮一下咱們在「解釋語言的語言中」給出的求值關係\(r\) ，對於表達式\(( f . ( t . f ) )\), 表達式可以經過求值關係\(\rightarrow_{r}\)獲得\((f . (t . f) )\rightarrow_{r}(f . t)\)以及\((f . (t . f) )\rightarrow_{r}(t . f)\)，可是咱們的關注點在於經過求值關係\(\rightarrow_{r}\)獲得的不一樣表達式的最終結果是否相同。這上面的例子中\((t . f)\)與\((f . t)\)最終都會規約到\(t\)，可是單個例子顯然沒有說服力。這須要證實求值的一致性（Consistency of Evaluation）。
    回憶一下在上一節提到的不一樣擴展範圍的求值關係：

name	definition	intution
\(-\)	the base relation on members of an expression grammar	a single "reduction" step with no context
\(\rightarrow_{-}\)	the compatible clojure of - with respect to expression grammar	a single step within context
\(\twoheadrightarrow_{-}\)	the reflexive-transitive clojure of \(\rightarrow_{-}\)	multiple evaluation steps (zero or more)
\(=_{-}\)	the symmetric-transitive clojure of \(\twoheadrightarrow_{-}\)	equate expression that produce the same result
\(eval_{-}\)	\(=_{-}\)restricted to a range of results	complete evaluation

    接下來在這裏先給出3個定理

Theorem 1: \(eval_r(B_0)=R_1\) and \(eval_r(B_1)=R_2\), then \(R_1=R_2\)
Theorem 2(Church-Rosser Theorem ): If \(M=_{r}N\) , there exists expression \(L\) such that \(M \twoheadrightarrow_{r} L\) and \(N \twoheadrightarrow_{r} L\)
Theorem 3(Diamond property of \(\twoheadrightarrow_{r}\)): If \(L \twoheadrightarrow_{r} M\) and \(L \twoheadrightarrow_{r} N\), then there exists expression \(L'\) such that \(M \twoheadrightarrow_{r} L'\) and \(N \twoheadrightarrow_{r} L'\)

    定理1解釋圖：

    定理1描述的是一個表達式經過求值函數 \(eval_r(B_0)\)獲得的值的一致性。

    定理2解釋圖：

    定理2描述的是兩個經過求值關係 \(\twoheadrightarrow_{r}\)獲得的表達式最終規約結果的一致性。
    證實過程：

Base case: if \(M =_{r} N\), there exists an expression \(L\) such that \(M =_{r} L\) and \(L =_{r} N\)( transitive relation)
- Case \(M \twoheadrightarrow_{r} N\)
Let \(L=N\) , the claim holds
Inductive cases:
- Case \(M =_{r} N\) because \(N =_{r} M\)
By induction, \(L\) exists for \(N =_{r} M\), that is the \(L\) we want
- Case \(M \twoheadrightarrow_{r} N\) because \(M \twoheadrightarrow_{r} L_0\) and \(L_0 \twoheadrightarrow_{r} N\)
By induction, there exists an \(L_1\) such that \(M \twoheadrightarrow_{r} L_1\) and \(L_0 \twoheadrightarrow_{r} L_1\). Also by the induction, there exists an \(L_2\) such that \(N \twoheadrightarrow_{r} L_2\) and \(L_0 \twoheadrightarrow_{r} L_2\)
then by theorem 1 and induction, there exists an \(L_3\) such that \(L_1 \twoheadrightarrow_{r} L_3\) and \(L_2 \twoheadrightarrow_{r} L_3\), the claim holds.

    定理2證實圖：

    定理3解釋圖：

    定理3描述的是一個表達式的不一樣規約路徑，最終規約到一個結果的過程，因爲形狀是一個四邊形（可能中間也會有多箇中間表達式 \(L_n\)），所以稱其爲關係 \(\twoheadrightarrow_{r}\)的Diamond property。
    基於上述的定理，能夠獲得基於關係 \(\twoheadrightarrow_{r}\)拓展而來的求值關係求值一致性保證。可是在具體的語言描述中，仍是須要對咱們的語言描述進行驗證，但這老是一個好的開始。

參考文獻

    [1] Matthias Fellesisen, Matthew Flatt.Programming Languages And Lambda Calculi[M]. Utah:, 2006. 21-24.