對稱元程式設計的元理論
此備註提供 原則性元程式設計 的簡化變體，並概述其健全性證明。此變體僅處理兩個階段之間的對話。程式可以有引號，其中可以包含拼接（可以包含引號，引號中可以包含拼接，依此類推）。或者，程式可以從包含嵌入式引號的拼接開始。必要的限制是：(1) 項可以包含頂層引號或頂層拼接，但不能同時包含，(2) 引號不能直接出現在引號內，拼接不能直接出現在拼接內。換句話說，宇宙僅限於兩個階段。
在此限制下，我們可以簡化類型規則，以便始終只有兩個環境，而不是一堆環境。這裡提供的變體與完整微積分不同的另一個原因是，我們用上下文類型規則取代評估環境。雖然這樣比較冗長，但可以更輕鬆地設定元理論。
語法
Terms t ::= x variable
(x: T) => t lambda
t t application
’t quote
~t splice
Simple terms u ::= x | (x: T) => u | u u
Values v ::= (x: T) => t lambda
’u quoted value
Types T ::= A base type
T -> T function type
’T quoted type
運算語意
評估
((x: T) => t) v --> [x := v]t
t1 --> t2
---------------
t1 t --> t2 t
t1 --> t2
---------------
v t1 --> v t2
t1 ==> t2
-------------
’t1 --> ’t2
拼接
~’u ==> u
t1 ==> t2
-------------------------------
(x: T) => t1 ==> (x: T) => t2
t1 ==> t2
---------------
t1 t ==> t2 t
t1 ==> t2
---------------
u t1 ==> u t2
t1 --> t2
-------------
~t1 ==> ~t2
類型規則
類型判斷的形式為 E1 * E2 |- t: T，其中 E1, E2 是環境，而 * 是 ~ 和 ’ 之一。
x: T in E2
---------------
E1 * E2 |- x: T
E1 * E2, x: T1 |- t: T2
--------------------------------
E1 * E2 |- (x: T1) => t: T -> T2
E1 * E2 |- t1: T2 -> T E1 * E2 |- t2: T2
-------------------------------------------
E1 * E2 |- t1 t2: T
E2 ’ E1 |- t: T
-----------------
E1 ~ E2 |- ’t: ’T
E2 ~ E1 |- t: ’T
----------------
E1 ’ E2 |- ~t: T
（奇怪的是，這看起來有點像聖誕樹）。
健全性
元理論通常需要對兩個判斷進行相互歸納。
進度定理
- 如果
E1 ~ |- t: T，則對於某個值v，t = v或對於某個項t2，t --> t2。 - 如果
’ E2 |- t: T，則對於某個簡單項u，t = u或對於某個項t2，t ==> t2。
通過項的結構歸納法證明。
證明 (1)
- 變數、lambda 和應用程式的案例與 STLC 中的案例相同。
- 如果
t = ’t2，則通過反演，我們對於某個類型T2，有’ E1 |- t2: T2。根據第二個 歸納假設 (I.H.)，我們有以下之一t2 = u，因此’t2是值，t2 ==> t3，因此’t2 --> ’t3。
- 情況
t = ~t2無法輸入。
證明 (2)
-
如果
t = x，則t是簡單項。 -
如果
t = (x: T) => t2，則t2是一個簡單項，在這種情況下t也是。或者根據第二個 I.H.t2 ==> t3，在這種情況下t ==> (x: T) => t3。 -
如果
t = t1 t2，則適用以下三種情況之一t1和t2是簡單項，則t也是簡單項。t1不是一個簡單的項。然後根據第二個 I.H.，t1 ==> t12，因此t ==> t12 t2。t1是個簡單的項，但t2不是。然後根據第二個 I.H.t2 ==> t22，因此t ==> t1 t22。
-
情況
t = ’t2無法打字。 -
如果
t = ~t2，則根據反演，我們有E2 ~ |- t2: ’T2，對於某些類型T2。根據第一個 I.H.，我們有一個t2 = v。由於t2: ’T2，我們必須有v = ’u，對於某些簡單項u，因此t = ~’u。根據引號拼接簡約，t ==> u。t2 --> t3。然後根據’t的上下文規則，t ==> ’t3。
替換引理
- 如果
E1 ~ E2 |- s: S且E1 ~ E2, x: S |- t: T，則E1 ~ E2 |- [x := s]t: T。 - 如果
E1 ~ E2 |- s: S且E2, x: S ’ E1 |- t: T，則E2 ’ E1 |- [x := s]t: T。
證明是根據 t 的打字推導進行歸納，類似於 STL 的證明（其中 (2) 比 (1) 簡單一些，因為我們不需要將 lambda 繫結與繫結變數 x 交換）。連結兩個假設的論點如下。
要證明 (1)，令 t = ’t1。然後 T = ’T1 對於某些類型 T1，最後一個打字規則是
E2, x: S ’ E1 |- t1: T1
-------------------------
E1 ~ E2, x: S |- ’t1: ’T1
根據第二個 I.H.，E2 ’ E1 |- [x := s]t1: ’T1。根據輸入，E1 ~ E2 |- ’[x := s]t1: ’T1。由於 [x := s]t = [x := s](’t1) = ’[x := s]t1，我們得到 [x := s]t: ’T1。
為了證明 (2)，令 t = ~t1。那麼最後的輸入規則是
E1 ~ E2, x: S |- t1: ’T
-----------------------
E2, x: S ’ E1 |- ~t1: T
根據第一個 I.H.，E1 ~ E2 |- [x := s]t1: ’T。根據輸入，E2 ’ E1 |- ~[x := s]t1: T。由於 [x := s]t = [x := s](~t1) = ~[x := s]t1，我們得到 [x := s]t: T。
保護定理
- 如果
E1 ~ E2 |- t1: T且t1 --> t2，則E1 ~ E2 |- t2: T。 - 如果
E1 ’ E2 |- t1: T且t1 ==> t2，則E1 ’ E2 |- t2: T。
證明方法是對評估推導進行結構歸納。證明 (1) 類似於 STL 的證明，使用替換引理作為 beta 歸約情況，並加上引號項目的歸約，如下所示
- 假設最後的規則是
t1 ==> t2 ------------- ’t1 --> ’t2根據輸入規則的反演，我們必須有
T = ’T1，其中T1是某種類型，使得t1: T1。根據第二個 I.H.，t2: T1，因此’t2:T1`。
證明 (2)
-
假設最後的規則是
~’u ==> u。~’u的輸入證明必須具有以下形式E1 ’ E2 |- u: T ----------------- E1 ~ E2 |- ’u: ’T ----------------- E1 ’ E2 |- ~’u: T因此，
E1 ’ E2 |- u: T。 -
假設最後的規則是
t1 ==> t2 ------------------------------- (x: S) => t1 ==> (x: T) => t2根據輸入反演，
E1 ' E2, x: S |- t1: T1，其中T1是某種類型，使得T = S -> T1。根據 I.H，t2: T1。根據 lambda 的輸入規則，結果如下。 -
應用程序的上下文規則同樣直接。
-
假設最後的規則是
t1 ==> t2 ------------- ~t1 ==> ~t2根據輸入規則的反演，我們必須有
t1: ’T。根據第一個 I.H.，t2: ’T，因此~t2: T。