【Programming Languages And Lambda calculi】 1.5 ~ 1.7 上下文規約 賦值函式 符號摘要
技術標籤：programming language程式語言lambda
文章目錄
1.5 上下文中的賦值
如何減少表示式 ((f • t) • f) ？根據 r 關係或者 ↝↝r 關係，這個表示式並不能規約！
直觀上看，通過將第一個子表示式根據 (f • t) r t 的規則， ((f • t) • f) 應該被規約到 (t•f) 。但是在r關係的定義中，沒有一項是滿足 ((f • t) • f) 的。我們只能將類似於 (f • B) 或 (t • B) 格式的表示式規約。換句話說，在 •
現在我們將 r關係 用 -->r 擴張，從而支援子表示式的規約：
–>r 關係被稱為 r關係 的 相容閉合（compatible closure）譯者注：從這篇開始，我找到了一個更合適的詞“閉合”來翻譯closure，以及更合適的詞“規約”來翻譯reduction
和r一樣， -->r 是一個單步規約的關係，但是它允許任何一個子表示式自身規約。用r關係規約後的子表示式被稱為 redex ，包裹redex的文字被稱為上下文（context）。
–>r 關係包括 ((f • t) • f) -->r (t • f)
並且，繼續規約這個表示式，我們最終可以得到 t ：
最後，如果我們定義 ->->r 作為 –>r 的自反-傳遞閉合，我們可以得到 ((f • t) • f) ->->r t，因此，->->r 是由r生成的自然規約關係（natural reduction relation）。
總結：
單純的自反閉合 ≍r，等價閉合 ≈r，或是自反-傳遞閉合 ↝↝r 關係將是無趣的。相反，我們最近感興趣的將會是相容閉合 -->r 和它的自反-傳遞閉合 ->->r ， 因為他們對應了典型的賦值概念。另外，–>r 的等價閉合 =r 關聯了會產生相同結果的表示式，因此它也很有趣。
練習 1.3
請你解釋為什麼 (f • ((t • f) • f)) !↝↝r** r t** .
題解：
(f • ((t • f) • f)) r ((t • f) • f) 無法繼續規約。
練習 1.4
請你用 -->r 進行規約，證明 (f • ((t • f) • f)) →→r t
題解：
(f • ((t • f) • f)) -->r ((t • f) • f) -->r (t • f) -->r t
1.6 賦值函式
→→r 將我們與賦值的概念拉得更近了。由於 ((f • t) • f) →→r t，我們發現 ((f • t) • f)→→r (t • f) 以及 ((f • t) • f)→→r ((f • t) • f) 同樣成立。
在賦值中，我們感興趣的是 B表示式 到底是 f 還是 t ，任何其他的對映關係都是無關緊要的。為了捕捉到這種賦值的概念，我們將 evalr 關係定義如下：
這裡，我們使用了另一個符號來定義關係，這個特殊的符號是具有暗示性的函式的一種關係，即把每一個元素最多對映到一個元素的關係。我們使用函式表示法，因為 evalr 必須是一個函式，才能讓它作為一個求值器而有意義。
練習 1.5
在這些關係中：哪一個是函式？在非函式關係中，找到它關聯的兩個表示式。
題解：
r 和 evalr 是函式。
- ≍r 不是函式
(t • B1) ≍r B1
(t • B1) ≍r (t • B1)
- ≈r 不是函式
(t • B1) ≈r B1
(t • B1) ≈r (t • B1)
- ↝↝r 不是函式
(t • B1) ↝↝r (t • B1)
(t • B1) ↝↝r t
- →r 不是函式
((t • B1) • (t • B1)) →r (t • (t • B1))
((t • B1) • (t • B1)) →r ((t • B1) • t)
- →→r 不是函式
(t • B1) ↠r (t • B1)
(t • B1) ↠r t
- =r 不是函式
(t • B1) =r (t • B1)
(t • B1) =r t
1.7 符號摘要
| 名字 | 定義 | 直觀定義 |
|---|---|---|
| _ | 表示式語法成員的基礎關係 | 一個單步的沒有上下文的規約步驟 |
| →_ | _ 關係 關於表示式語法的相容閉合關係 | 上下文中的單步 |
| →→_ | →_關係 的自反-傳遞閉合 | 多數賦值步驟（0或多） |
| =_ | →→_關係 的對稱-傳遞閉合 | 產出相同結果的同等表示式 |
| eval_ | =_關係 嚴格限定結果的範圍 | 全面完整的賦值函式 |
第一章 完