技術標籤：programming language程式語言

1.4 有向賦值

“賦值”規則 ≈r 看上去並不特別像賦值。它允許我們證明某些表示式是相等的，但是它沒有確切地告訴我們如何從一個隨意的B集合元素到 t 或是 f 。

更加簡單的關係 r 事實上顯得更加有用。在r關係的定義中，兩個給定的條件都將一個表示式轉化成另一個更簡的表示式。並且，對於任何集合B的表示式中，B集合元素要麼是t或者f，要麼關係r將B集合元素與至多一個的其他表示式相關聯。作為結論來說，我們可以將 r 視為 單步減少（single-step reduction）行為，從而幫助我們理解一個直譯器可能會通過單步賦值的方式進行到最終值之前的工作。

我們可以定義 ~~r 為r關係的自反-傳遞封閉，這樣一來，我們會得到一個 多步減少 關係。多步減少關係 ~~r 會將一個表示式轉化（map）為許多其他的表示式。但是事實證明，多步減少關係最終會將表示式轉化為 要麼 t 要麼 f 。

通過定義 ~~r 為r關係“自反-傳遞封閉”已經足夠。另一種可用的定義方式為擴張r關係的規約。第三種方式為部分擴張規約，但是在定義之中使用r關係：

r 關係以及 ~~r 關係是有意不對稱的，以顯賦值過程中的有向性。比如，給定表示式 (f • (f • (t • f))) ，我們可以進行如下的減少：

左邊的空列是上一行右邊的表示式。每一行都是 (f • (f • (t • f))) ~~r t

練習1.2

用單步減少的r關係證明 (f • (f • (f • f))) ~~r f

題解

(f • (f • (f • f))) r (f • (f • f)))

​					  r (f • f)

​					  r f

所以，(f • (f • (f • f))) ~~r f