The Church-Rosser Theorem

闲扯

最近写的尽是些有的没的,完全没有干货。怎么说,最近考虑在思考人生,价值观在改变,简而言之就是又退化到科学>>技术的中二阶段。一方面看到现阶段所谓“技术产物”的各种各样的问题,另一方面由于自身智力,能力,精力的限制,没有办法对其进行改进和提升,只能采取粗暴的、眼不见为净的鸵鸟政策。其实我知道自己是躲不掉的(当然我说的是找工作),但是还是想在不得不面对之前关心些别的,或者说补救些别的,能补多少是多少吧。年轻的时候有大把时间,却不想念书,现在老了,想念书了,却没有多少时间了(有时间也架不住嗜睡)。

Anyway, 我接下来准备翻译大段的关于无类型lambda-calculus中Church-Rosser定理的证明,为什么要做这么无聊的事情?因为我觉得有趣…为什么不先完善下之前对STLC的证明?1.不求甚解是我的一贯毛(feng)病(ge);2.这个定理在它的证明中会有一丢丢的作用,Normalization证明的补充会在之后进行。

beta-eta-reduction

  • $\beta-reduction$ 就不赘述了
  • $\beta-equivalence$ 为其自反,对称,传递闭包,记作 $=_{\beta}$,描述的是这样的二元关系:两个表达式可以通过若干步正向或者反向的beta归约相互转化。
  • $\eta-reduction$ 规定如果两个表达式作用在任意相同的表达式上,得到的结果相同,则可以认为两个表达式相同,即函数相同的定义。于是有$\lambda x.Mx \rightarrow_{\eta} M, where\ x \notin FV(M)$
  • $\beta\eta-reduction$ 就是两者的结合,记作 $\rightarrow_{\beta\eta}$
  • 结合后的多步操作,即其自反,传递闭包记作 $\twoheadrightarrow_{\beta\eta}$,equivalence, normal form的概念也有相应的扩充

Statement of Church-Rosser Theorem

  • 用双箭头表示 $\twoheadrightarrow_{\beta}$ 或者 $\twoheadrightarrow_{\beta\eta}$

如果某M, N, P满足 $M \twoheadrightarrow N \land M \twoheadrightarrow P$,则存在某个Z,使得 $N \twoheadrightarrow Z \land P \twoheadrightarrow Z$。
就是说,不论在beta或者是beta-eta的操作语义下,如果N和P对于M都是多步可达的,那么它们必定共享某个可达的表达式Z,如下图:

cr

What does that theorem imply?

Corollary 1 : 如果 $M =_{\beta} N$,则存在某表达式Z,使得$M,N \twoheadrightarrow_{\beta} Z$,对beta-eta有同样结论。

Proof : 前提条件等价于如下描述:存在一个有限的表达式序列$M_0, M_1, …, M_n$,其中相邻的两个表达式满足关系$\leftarrow_{\beta}$或者$\rightarrow_{\beta}$,且头和尾分别是M和N。

对n进行归纳,当n为0时,M与N恒等,结论显然。若n-1时成立,归纳假设,存在Z’使得$M \twoheadrightarrow_{\beta} Z’ \land M_{n-1} \twoheadrightarrow_{\beta} Z’$。
N和$M_n$之间的关系有两种情况:

  1. $N \rightarrow_{\beta} M_{n-1}$ : 于是有 $N \twoheadrightarrow_{\beta} Z’$,于是Z’即满足
  2. $N \leftarrow_{\beta} M_{n-1}$ : 我们将Church-Rosser定理作用于$M_{n-1}, Z’, N$,于是存在Z使得 $Z’ \twoheadrightarrow_{\beta} Z \land N \twoheadrightarrow_{\beta} Z$,于是 $M \twoheadrightarrow_{\beta} Z’ \twoheadrightarrow_{\beta} Z$,得证。

对于beta-eta有类似证明。

Corollary 2 : 如果N是一个normal form(无法继续归约),$N =_{\beta} M$,则 $M \twoheadrightarrow_{\beta} N$, beta-eta类似。

Proof : 1的简单推论,Z只能是N

Corollary 3 : 如果$M =_{\beta} N$,则其中一者的normal form也是另一者的normal form, beta-eta类似。

Proof : 不妨设M有normal form Z,于是有$M =_{\beta} Z =_{\beta} N$,于是根据2有 $N \twoheadrightarrow_{\beta} Z$,得证。

可以看出3是一个很有意义的推论,有助于后续性质的推导。

Why is that hard to proof?

对下图中的a, b, c作与该定理的描述相似的解读。

cr-abc

  • a等价于Church-Rosser定理
  • 容易证明c蕴含a,但是$\beta\eta-reduction$不满足c(又叫Diamond property)
  • a蕴含b,反之不然(反例见下图),于是我们无法通过证明b来证明a

cr-ba

定理的证明过程通过寻找一个满足如下性质的归约关系 $\triangleright$ 来克服上述困难:

  • $\triangleright$ 满足c
  • 其自反,传递闭包即为$\twoheadrightarrow_{\beta\eta}$

假设能够找到这样的关系,那么根据其c性质推出其a性质,又在a中,其多步的闭包与beta-eta相同,便能证明beta-eta满足a性质

Proof of the Theorem

$\triangleright$ 定义如下:

  1. $\overline{M \triangleright M}$
  2. $\dfrac{P \triangleright P’ \ \ N \triangleright N’}{PN \triangleright P’N’}$
  3. $\dfrac{N \triangleright N’}{\lambda x.N \triangleright \lambda x.N’}$
  4. $\dfrac{Q \triangleright Q’ \ \ N \triangleright N’}{(\lambda x.Q)N \triangleright Q’[N’/x]}$
  5. $\dfrac{P \triangleright P’, where\ x \notin FV(P)}{\lambda x.Px \triangleright P’}$

Lemma1

Lemma1 :

  1. 如果$M \rightarrow_{\beta} M’$ 则 $M \triangleright M’$
  2. 如果$M \triangleright M’$ 则 $M \twoheadrightarrow_{\beta\eta} M’$
  3. $\twoheadrightarrow_{\triangleright} = \twoheadrightarrow_{\beta\eta}$

Proof :

1和2类似,通过对前提中的关系进行归纳便容易得证,这里就不展开冗长的过程了。事实上这个新的关系又叫作parallel one-step reduction,它的每步归约可以比beta-eta多做一些事情,相当于把多步并作一步进行(也可以不选择并行,根据1),这么理解之后1和2的结论便是显然成立的。

至于3,根据1可得,若beta-eta多步归约可达,则parallel one-step多步归约可达,即$\twoheadrightarrow_{\triangleright} \subseteq \twoheadrightarrow_{\beta\eta}$;根据2,反之,即$\twoheadrightarrow_{\beta\eta} \subseteq \twoheadrightarrow_{\triangleright}$。

Lemma2

至此,我们只需证明parallel one-step满足性质c。为此,我们还需要若干引理。

Lemma2 : 若 $M \triangleright M’ \land U \triangleright U’$,则 $M[U/y] \triangleright M’[U’/y]$

Proof : 对 $M \triangleright M’$ 进行归纳,共5种情况,对于标号1, 2, 3, 5的情况,结论显然,不再赘述,针对4:

  • 有$M = (\lambda x.Q)N \land M’ = Q’[N’/x] \land Q \triangleright Q’ \land N \triangleright N’$
  • 归纳假设,有$Q[U/y] \triangleright Q’[U’/y] \land N[U/y] \triangleright N’[U’/y]$
  • 根据规则4,有$(\lambda x.Q[U/y]) N[U/y] \triangleright Q’[U’/y][N’[U’/y]/x] = Q’[N’/x][U’/y]$ 即 $M[U/y] \triangleright M’[U’/y]$,得证

Lemma3

引入最终形态(maximal parallel one-step reduct)M*的概念,形式化定义如下:

  1. $x^* = x$, for variable x
  2. $(PN)^* = P^*N^*$, if PN is not a $\beta-redex$
  3. $(\lambda x.N)^* = \lambda x.N^*$, if $\lambda x.N$ is not a $\eta-redex$
  4. $((\lambda x.Q) N)^* = Q^*[N^*/x]$
  5. $(\lambda x.P x)^* = P^*$, if $x \notin FV(P)$

Lemma3 : 若 $M \triangleright M’$,则 $M’ \triangleright M^*$

Proof : 对M的大小进行归纳,首先,按照惯例,将前提分成5种情况:

  1. M = M’ = x, 又 M* = x, 成立
  2. M = PN,M’ = P’N’, $P \triangleright P’ \land N \triangleright N’$. 归纳假设,得到 $P’ \triangleright P^* \land N’ \triangleright N^*$,再分为两种情况:
    1. PN不是个beta可约式,根据终极形态的定义2,$M’ = P’ N’ \triangleright P^*N^* = M^*$,得证
    2. PN beta可约,则P为一个lambda函数,设$P = \lambda x.Q$,则根据终极心态定义4 $M^* = Q^*[N^*/x]$,对$P \triangleright P’$再分情况,只能是1, 3, 5:
      1. 若为1,$M’ = PN’ = Q[N’/x]$,由于Q为M的一部分,大小小于M,归纳假设,有$Q \triangleright Q \triangleright Q^*$,于是根据Lemma2, $M’ = Q[N’/x] \triangleright Q^*[N^*/x] = M^*$
      2. 若为3,$P’ = \lambda x.Q’ \land Q \triangleright Q’$,同理,Q的大小小于M,归纳假设有$Q’ \triangleright Q^*$,于是根据归约条件4,$M’ = (\lambda x.Q’)N’ \triangleright Q^*[N^*/x] = M^*$
      3. 若为5,$P = \lambda x.R’x \land P’ = R’ \land R \triangleright R’$ 且x不是P’的自由变量,Rx是M的子式,归纳假设,$Rx \triangleright R’x \triangleright (Rx)^*$,根据Lemma2,有$M’ = R’N’ = (R’x)[N’/x] \triangleright (Rx)^*[N^*/x] = M^*$
  3. $M = \lambda x.N \land M’ = \lambda x.N’ \land N \triangleright N’$,分两种情况
    1. M eta不可约,则根据终极形态定义3,$M^* = \lambda x.N^*$,根据归约定义3,$M’ = \lambda x.N’ \triangleright \lambda x.N^* = M^*$
    2. M eta可约,则$M = \lambda x.Px \land N=Px \land x \notin FV(P)$,根据终极形态定义5,M* = P*, 对$N \triangleright N’$再分情况,只能是1, 2, 4:
      1. 若为1,N=N’=Px, P为M的子式,归纳假设,根据归约条件5,$P \triangleright P \triangleright P^*, M’ = \lambda x.Px \triangleright P^* = M^*$
      2. 若为2,$N’ = P’x \land P \triangleright P’$,同理,归纳假设,根据归约条件5, $P’ \triangleright P^*, M’ = \lambda x.P’x \triangleright P^* = M^*$
      3. 若为4,$P = \lambda y.Q \land N’ = Q’[x/y] \land Q \triangleright Q’$,P为M子式,有$P \triangleright \lambda y.Q’ \triangleright P^*$,于是$M’ = \lambda x.Q’[x/y] = \lambda y.Q’ \triangleright P^*$,右边最后一个等号是因为x不是Q’的自由变量
  4. $M = (\lambda x.Q)N \land M’ = Q’[N’/x] \land Q \triangleright Q’ \land N \triangleright N’$,根据终极形态定义4,$M^* = Q^*[N^*/x]$,根据Lemma2,得证
  5. $M = \lambda x.Px \land M’=P’ \land P \triangleright P’$,同上,归纳假设,$M’ = P’ \triangleright P^* = M^*$

Q.E.D

Diamond Property

终于,可以通过Lemma3来证明parallel one-step满足c属性,i.e. Diamond Property了。

回忆下c属性的描述: 若$M \triangleright N \land M \triangleright P$,则存在Z满足 $N \triangleright Z \land P \triangleright Z$。

这里只需要使 Z = M* ,根据Lemma3,结论显然。至此,结合前文的铺垫,Church-Rosser定理便得到了证明。

对于beta-reduction,只需要调整构造,将对应的规则5都删去即可。

叹为观止

如此神奇的证明,我虽然能理解它是有道理的,但是完全无法想象出这样奇妙的证明是怎么构造出来的,尤其是其中parallel one-step和maximal reduct的构造。
相比与糟糕的应用,糟糕的工具,糟糕的OS(尤其是IOS),糟糕的服务,糟糕的设备……数学是如此的美好~~

References