对称元编程的元理论
本笔记介绍了 原则性元编程 的简化变体，并概述了其健全性证明。该变体仅处理两个阶段之间的对话。程序可以包含引号，引号中可以包含拼接（拼接中可以包含引号，引号中可以包含拼接，等等）。或者程序可以从包含嵌入引号的拼接开始。本质上的限制是 (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，则要么t = v，其中v是某个值，要么t --> t2，其中t2是某个项。 - 如果
’ E2 |- t: T，则要么t = u，其中u是某个简单项，要么t ==> t2，其中t2是某个项。
通过对项进行结构归纳证明。
为了证明 (1)
- 变量、lambda 和应用的情况与 STLC 中的情况相同。
- 如果
t = ’t2，则根据反演，我们有’ E1 |- t2: 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
根据第二个归纳假设，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
根据第一个归纳假设，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。根据第二个归纳假设，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。根据归纳假设，t2: T1。根据 lambda 表达式的类型规则，结果成立。 -
应用的上下文规则同样简单明了。
-
假设最后一个规则是
t1 ==> t2 ------------- ~t1 ==> ~t2根据类型规则的反演，我们必须有
t1: ’T。根据第一个归纳假设，t2: ’T，因此~t2: T。