求值顺序与CPS

最近在读小林直树写的Model checking higher-order programs时发现了一个错误。在把 call-by-name的

$$x$$

转换成call-by-value的

$$\lambda k. k\ x$$

时，他把式子写成了$\lambda x.k\ x$。要说我是怎么发现这个错误的，这其实是因为一开始我完全没有看懂什么叫做可以把call-by-value的程序转换成顶层全是unit类型的call-by-name程序。于是我就去查了Plotkin的原始文献，发现了上面的错误。

正确来说，用于转换的公式有以下四个（用unary算符$\overline{\cdot}$表示转换）

1. $\overline{a} = \lambda k.k\ a$，其中$a$是常量
2. $\overline{x} = \lambda k.k\ x$，其中$x$是变量
3. $\overline{\lambda x.M} = \lambda k. k\ (\lambda x. \overline{M})$
4. $\overline{MN} = \lambda k. (\overline{M} (\lambda f \overline{N} (\lambda a. f\ a\ k)))$

话说Plotkin居然会把$\kappa$和$x$混起来用，在论文的样式下这两个字符简直一模一样。1975年的文献还只有影印版，真是视力毁灭者。也难怪小林直树会把这两个字符搞混了。

Call-by-value, Call-by-name和$\lambda$演算

在讨论一些更深入的事情之前，有必要解释一下$\lambda$ calculus里的cbv和cbn。粗略地讲，在程序语言中，call-by-value指在进行函数参数传递时所有参数会被首先求值，最后把值传进函数；而call-by-name则会把表达式直接传进去，直到完全传透为止不进行表达式的求值。

在$\lambda$演算中的call-by-value和call-by-name则按照如下方式定义，注意下面值指的是非application的表达式（即常量，变量和抽象）

1. call-by-value：仅允许值进行代入；
2. call-by-name：从最外层最左侧的表达式开始求值（代入）。

我们知道，根据Church-Rossar定理，一个$\lambda$表达式的最简式和它的代入顺序无关（当然，如果“不恰当地”选择顺序，式子可能无法化到最简）。因此无论是cbv还是cbn，对于同一个$\lambda$表达式，最终的结果总是一样的。但是这个结论不总是成立。其一，存在上述的规约顺序的问题，这会影响规约最终是否能够终止；其二，如果$\lambda$演算允许副作用存在，则可能出现不同的结果。一个程序例子如下

let x := 0 in
let f a := a + a in
f (x := !x + 1; !x)

在这个例子里，call-by-value的最终结果是2，而call-by-name的最终结果是3。一般而言， call-by-name会获得更好的终止性，而call-by-value则更符合机器执行逻辑。一个只在 call-by-name的情况下可以终止规约的$\lambda$表达式如下：

$$(\lambda x.y)((\lambda x.x\ x)(\lambda x.x\ x)) \rightarrow_V (\lambda x.y)((\lambda x.x\ x)(\lambda x.x\ x))$$ $$(\lambda x.y)((\lambda x.x\ x)(\lambda x.x\ x)) \rightarrow_N y$$

转换

在小林直树的文章里，他使用了并不非常正式的表述“转换”。严格来说，在被转换之前和之后，程序始终是$\lambda$表达式，转换并不足以表达前后的某种等价关系。在原始文献中，有更加严密的表达。

Our object here is to show that call-by-value can be simulated by call-by-name, and vise versa.

作者使用了“模拟”。也就是说，用call-by-name的方式对转换后的程序进行规约时，能够得到和用call-by-value方式对转换前程序进行规约时的同样行为。作者用三个定理描述了这个性质。

1. $\mathbf{Theorem1}.\ (\text{Indifference}).\ Eval_N(\overline{M}(\lambda x.x)) = Eval_V(\overline{M}(\lambda x.x))$
2. $\mathbf{Theorem2}.\ (\text{Simulation}).\ \Psi(Eval_V(M)) = Eval_N(\overline{M}(\lambda x.x))$
3. $\mathbf{Theorem3}.\ (\text{Translation}).$ If $\lambda_V^{\mathcal{L}}\vdash M=N$ then $\lambda_V^{\mathcal{L''}}\vdash \overline{M}=\overline{N}$ and then $\lambda_N\vdash \overline{M}=\overline{N}$ . The second but not the first implication is reversible.

其中$\mathcal{L}$指call-by-value的原语言，$\mathcal{L'}$指call-by-name的语言，$\mathcal{L''}$指call-by-value的语言，但是其常量，变量，变量列表和$Constapply$使用了call-by-name的版本。其中$Constapply$是一个应用primitive函数的语法糖，其中$Constapply(a,b)$指把primitive$a$应用到$b$上，若无法把$a$应用到$b$上，或$a$不是primitive，则$Constapply(a,b)$没有定义，有以下定义

$$Constapply_N(a,b) = \overline{Constapply_V(a,b)}$$

$\Psi(x)$定义为

$$\Psi(a) = a,\ \Psi(x) = x,\ \Psi(\lambda x.M) = \lambda x.\overline{M}.$$

即保存所有抽象，值和变量，只改变应用。

不过在深入讨论（并证明）这三个定理之前，我们先来非正式地思考一下$\lambda$式规约结果的等价性。让我们回到最开头的转换公式上。

1. $\overline{a} = \lambda k.k\ a$，其中$a$是常量
2. $\overline{x} = \lambda k.k\ x$，其中$x$是变量
3. $\overline{\lambda x.M} = \lambda k. k\ (\lambda x. \overline{M})$
4. $\overline{MN} = \lambda k. (\overline{M} (\lambda f. \overline{N} (\lambda a. f\ a\ k)))$

可以观察到，从构成上来说，前三个公式用了一样的转换方式：接受一个$k$，然后对$k$应用原式。这里用到的是(CPS, continuation-passing style)的思路。$k$是被显式编码的continuation计算，即“执行完a之后会执行的控制流”。在直觉上令人有些迷惑的是，原式被放在了continuation后面，这看起来像是“先执行continuation，然后再执行原式”，例如

$$(\lambda k.k\ x)K \rightarrow K\ x$$

关于$K$，一般地，如果表达式处于顶层，我们会把这个$K$定义成恒等的$\lambda x.x$。这样，表达式才能够被真正执行，例如

$$(\lambda k.k\ x)(\lambda x.x) \rightarrow (\lambda x.x)x \rightarrow x$$

而对于非顶层的表达式，在转换到call-by-name（$\mathcal{L'}$）后，$K$也一定在开头携带一个抽象，这部分会把后面的$x$翻到前面去。

对于第四个转换公式，可以注意到它获取了3个continuation。第一个continuation $k$作为整体表达式的$K$，被放在了最后一个$\lambda$抽象的最后的位置，成为了$f\ a$的continuation。然而$f,a$似乎又与上面得出的反转直觉相反---它们又不反转了。这是因为$\overline{M}$和$\overline{N}$一定存在把它们各自的continuation翻到前面的$\lambda$抽象。例如

$$M = \lambda k.k\ Y,\ N = \lambda k.k \ Z,$$ $$MNK=(\lambda k.k\ Y)(\lambda k.k\ Z)K \rightarrow ((\lambda k.k\ Z)Y)K\rightarrow Y\ Z\ K$$ $$\overline{MNK}=\overline{M}(\lambda f.\overline{N}(\lambda a.f\ a\ K))= (\lambda k.k\ Y)(\lambda f.\overline{N}(\lambda a.f\ a\ K)) \\\rightarrow (\lambda f.\overline{N}(\lambda a.f\ a\ K))Y = (\lambda f.(\lambda k. k\ Z)(\lambda a.f\ a\ K))Y\rightarrow (\lambda f.(\lambda a.f\ a\ K)Z)Y \rightarrow Y\ Z\ K$$

定理的证明

Plotkin用4个引理证明了这3个定理。让我们从引理一开始。

引理一

$$\mathbf{Lemma\ 1}.\ [\Psi(N)/x]\overline{M} = \overline{[N/x]M},\text{ if } N\text{ is a value and }x\not\in \{k, a, b\}.$$

这个引理相对比较好证明，只需对$M$进行结构性归纳即可。

1. 若$M$是常量$a$，则有 $$[\Psi(N)/x]\overline{a} = [\Psi(N)/x](\lambda k.k\ a) = (\lambda k.k\ a) = \overline{[N/x]a}$$
2. 若$M$是变量，则有
   • 当$M$是$y$时，显然。
   • 当$M$是$x$时，
   $$[\Psi(N)/x]\overline{x} = [\Psi(N)/x](\lambda k.k\ x) = \lambda k.k\ \Psi(N)\ (k\not\in FV(N)) \\= \overline{N} = \overline{[N/x]x}$$
3. 若$M$是抽象$\lambda y.M_1$，则有
   • 当$y = x$时，显然。
   • 否则，
   $$\begin{align*} [\Psi(N)/x]\overline{\lambda y.M_1} &= [\Psi(N)/x](\lambda k.k\ (\lambda y.\overline{M_1}))\\ &= \lambda k.k\ (\lambda z.([\Psi(N)/x][z/y]\overline{M_1}))\\ &(x\not=k,\ k\not\in FV(N),\text{ and with the usual condition on z})\\ &= \lambda k.k\ (\lambda z.([\Psi(N)/x]\overline{[z/y]M_1}))\quad (\text{by induction hypothesis})\\ &= \lambda k.k\ (\lambda z.(\overline{[N/x][z/y]M_1}))\quad (\text{by induction hypothesis})\\ &= \overline{\lambda z.([N/x][z/y]M_1)}\\ &= \overline{[N/x]\lambda y.M_1} \end{align*}$$

这里有一步可能会造成困扰。第二个等号引入了新的抽象$z$。从表面上看，好像更简单的写法是$\lambda k.k\ (\lambda y.([\Psi(N)/x]\overline{M_1})),\quad y\not\in FV(\Psi(N)).$不这么写是因为，由于$M$中本身就出现了$y$，$FV(\Psi(N))$可能真的会有$y$，使得这种写法不一定总是成立。

4. 若$M$是应用$M_1M_2$，则有 $$\begin{align*} \overline{M_1M_2} &= [\Psi(N)/x](\lambda k.\overline{M_1}(\lambda f.\overline{M_2}(\lambda a.f\ a\ k)))\\ &= \lambda k.[\Psi(N)/x]\overline{M_1}(\lambda f.[\Psi(N)/x]\overline{M_2}(\lambda a.f\ a\ k))\\ &(\text{as }x\not\in \{k,f,a\}\text{ and }f,a\not\in FV(\Psi(N)))\\ &= \lambda k.\overline{[N/x]M_1}(\lambda f.\overline{[N/x]M_2}(\lambda a.f\ a\ k))\quad (\text{by induction hypothesis})\\ &= \overline{[N/x]M_1[N/x]M_2}\\ &= R.S. \end{align*}$$

引理二

在介绍引理二之前，Plotkin引入了一个新的算符“$:$”。它定义在$\mathcal{L}\times\mathcal{L'}\rightarrow \mathcal{L'}$上，具体如下

$$\begin{align*} &N:K=K\Psi(N)\quad &(N\text{ is a closed value})\\ &MN:K=M:(\lambda f.\overline{N}(\lambda a.f\ a\ K))\quad &(M\text{ is not a value})\\ &MN:K=N:(\lambda a.\Psi(M)\ a\ K)\quad &(M, \text{ but not } N,\text{ is a value})\\ &MN:K=\Psi(M)\Psi(N)K\quad &(M \text{ and } N \text{ are values}) \end{align*}$$

在此基础上，我们有引理2

$$\mathbf{Lemma\ 2}.\ \text{If }K\text{ is a closed value then }\overline{M}K\overset{+}{\rightarrow}M:K,\text{ for any term }M,(f,a,k\not\in FV(K)).$$

其中$\overset{+}{\rightarrow}$表示一步及以上但有限的规约。引理二也通过结构性归纳证明。

1. 若$M$是值（即不是应用），那么 $$\overline{M}K = (\lambda k.k\Psi(M))K \rightarrow K\Psi(M) = M:K$$
2. 若$M$是应用$(M_1M_2)$，那么
   • subcase 1：若$M_1$不是值，那么根据“$:$”的定义有 $$(M_1M_2):K=M_1:(\lambda f.\overline{M_2}(\lambda a.f\ a\ K))$$ 而 $$\begin{align*} \overline{M}K = \overline{M_1M_2}K &= (\lambda k.\overline{M_1}(\lambda f.\overline{M_2}(\lambda a.f\ a\ k)))K \rightarrow \overline{M_1}(\lambda f.\overline{M_2}(\lambda a.f\ a\ K))\\ &\overset{+}{\rightarrow} M_1:(\lambda f.\overline{M_2}(\lambda a.f\ a\ K))\quad (\text{by induction hypothesis})\\ &=M:K \end{align*}$$
   • subcase 2：若$M_1$是值，但$M_2$不是值，那么有 $$(M_1M_2):K = M_2:(\lambda a.\Psi(M_1)\ a\ K)$$ 而 $$\begin{align*} \overline{M}K &\overset{+}{\rightarrow}M_1:(\lambda f.\overline{M_2}(\lambda a.f\ a\ K))\quad (\text{by induction step in subcase 1})\\ &=(\lambda f.\overline{M_2}(\lambda a.f\ a\ K))\Psi(M_1)\rightarrow \overline{M_2}(\lambda a.\Psi(M_1)\ a\ K)\\ &\overset{+}{\rightarrow} M_2:(\lambda a.\Psi(M_1)\ a\ K)\quad (\text{by induction hypothesis})\\ &=M:K \end{align*}$$
   • subcase 3：若$M_1$和$M_2$都是值，那么 $$(M_1M_2):K = \Psi(M_1)\Psi(M_2)K$$ 而 $$\begin{align*} \overline{M}K &\overset{+}{\rightarrow}M_2:(\lambda a.\Psi(M_1)\ a\ K)\quad (\text{as in subcase 2})\\ &\rightarrow (\lambda a.\Psi(M_1)\ a\ K)\Psi(M_2)\\ &\rightarrow \Psi(M_2)\Psi(M_1)K \end{align*}$$

这样就完成了这个引理的证明。原始文献里有些跳步让它变得难读，上面做了一些修正。

引理三

引理三如下

$$\mathbf{Lemma\ 3}.\ \text{If }M\underset{V}{\rightarrow}N\text{ then }M:K\overset{+}{\rightarrow}N:K\ (\text{ If }K\text{ is a closed value and }M\text{ and }N\text{ are terms}).$$

同样地，我们使用结构性归纳。这里我们按照$M$及规约后的$N$的类型进行分类。注意$M$一定是某种应用。

1. subcase 1：$M$是常量应用$ab$，此时$N$立即地是$Constapply_V(a,b)$，有 $$\begin{align*} M:K &= abK\rightarrow Constapply_N(a,b)K = \overline{N}K\\ &\overset{+}{\rightarrow}N:K\quad (\text{by Lemma 2}) \end{align*}$$
2. subcase 2：$M$是抽象应用$(\lambda x.M_1)M_2$且$M_2$是值（即不是应用），因此$N$是$[M_2/x]M_1$，有 $$\begin{align*} M:K &= \Psi(\lambda x.M_1)\Psi(M_2)K\quad (\text{by }:\text{'s definition})\\ &= (\lambda x.\overline{M_1})\Psi(M_2)K \rightarrow [\Psi(M_2)/x]\overline{M_1}K\\ &= \overline{[M_2/x]M_1}K\quad (M_2\text{ is a value, hence by Lemma 1})\\ &= \overline{N}K\\ &\overset{+}{\rightarrow}N:K\quad (\text{by Lemma 2}) \end{align*}$$
3. subcase 3：$M$是一般应用$M_1M_2$，且$M_1$是值，$M_2$有规约$M_2\underset{V}{\rightarrow}N_2$，此时可得$N = M_1N_2$，有 $$\begin{align*} M:K &= M_2:(\lambda a.\Psi(M_1)\ a\ K)\quad (\text{by }:\text{'s definition})\\ &\overset{+}{\rightarrow}N_2:(\lambda a.\Psi(M_1)\ a\ K)\quad (\text{by induction hypothesis})\\ &= L, \end{align*}$$
   • 若$N_2$是值，首先 $$N:K = (M_1N_2):K = \Psi(M_1)\Psi(N_2)K$$ 而根据$:$的定义，可得 $$L = (\lambda a.\Psi(M_1)\ a\ K)\Psi(N_2) \rightarrow \Psi(M_1)\Psi(N_2)K = N:K$$
   • 若$N_2$不是值，根据$:$的定义 $$N:K = (M_1N_2):K = N_2:(\lambda a.\Psi(M_1)\ a\ K)$$ 直接得到了$L$。
4. subcase 4：$M$是一般应用$M_1M_2$，且$M_1$有规约$M_1\underset{V}{\rightarrow}N_1$，此时可得$N = N_1M_2$，那么 $$\begin{align*} M:K &= (M_1M_2):K\\ &= M_1:(\lambda f.\overline{M_2}(\lambda a.f\ a\ K))\quad (\text{by }:\text{'s definition})\\ &\overset{+}{\rightarrow} N_1:(\lambda f.\overline{M_2}(\lambda a.f\ a\ K))\quad (\text{by induction hypothesis})\\ &= L, \end{align*}$$
   • 若$N_1$是值，根据$:$的定义，有 $$\begin{align*} L &= (\lambda f.\overline{M_2}(\lambda a.f\ a\ K))\Psi(N_1)\\ &\rightarrow \overline{M_2}(\lambda a.\Psi(N_1)\ a\ K)\\ &\overset{+}{\rightarrow} M_2:(\lambda a.\Psi(N_1)\ a\ K)\quad (\text{by Lemma 2})\\ &= L' \end{align*}$$
     • 此时考虑$M_2$，若$M_2$是值，根据“$:$”的定义有 $$N:K = N_1M_2:K = \Psi(N_1)\Psi(M_2)K$$ 且 $$L' = (\lambda a.\Psi(N_1)\ a\ K)\Psi(M_2) \rightarrow \Psi(N_1)\Psi(M_2)K = N:K$$
     • 而若此时$M_2$不是值，根据“$:$”的定义有 $$N:K = N_1M_2:K = M_2:(\lambda a.\Psi(N_1)\ a\ K)$$ 直接得到了$L'$。
   • 若$N_1$不是值，根据$:$的定义有 $$N:K = N_1M_2:K = N_1(\lambda f.\overline{M_2}(\lambda a.f\ a\ K))$$ 直接得到了$L$。

这样就完成了证明。不得不说原始证明写得真是烂透了。

引理四

在引理四的开头，作者首先定义了$Sticks_*$。一个很重要但是作者却没有明说的直觉是，$Sticks_*$指在$*$的求值策略下最终会卡住而无法进一步化简的表达式。$Sticks_V$定义如下

1. 常量应用：若$Constapply_V(a,b)$没有定义（即$a$不是可以应用于$b$的primitive），则$ab\in Sticks_V$
2. 常量-抽象应用：对于任意项$N$，$a(\lambda x.N)\in Sticks_V$
3. 抽象应用：若$N\in Sticks_V$，那么对于任意项$M$，有$(\lambda x.M)N\in Sticks_V$
4. 一般应用：若$M\in Sticks_V$，那么对于任意项$N$，有$MN\in Sticks_V$

作者只分了四类令人有些意外。按照作者的定义，一个项可以是常量，变量，抽象和应用。即使顶层是变量$x$没有意义，

而$Sticks_N$定义如下

1. 常量应用：若$Constapply_N(a,b)$没有定义（即$a$不是可以应用于$b$的primitive），则$ab\in Sticks_N$
2. 常量-抽象应用：对于任意项$N$，$a(\lambda x.N)\in Sticks_N$
3. 一般应用：若$M\in Sticks_N$，那么对于任意项$N$，有$MN\in Sticks_N$
4. 常量-一般应用：若$N\in Sticks_N$，那么$aN\in Sticks_N$

在此基础上，有

1. 若$M\underset{V}{\overset{+}{\rightarrow}}N$，且$M$和$N$都不是值（都是应用），且$M$内没有自由变量，那么$M\in Sticks_V$
2. 若$M\underset{N}{\overset{+}{\rightarrow}}N$，且$M$和$N$都不是值，且$M$内没有自由变量，那么$M\in Sticks_N$

作者指出显然$Sticks_V\subseteq Sticks_N$。