Church-Rosser(CR)性质

等价关系,一步归约

设 $R$ 是集合 $\Lambda$ 上的一个二元关系,则 $R$ 中包含 $\Lambda$ 中的一些有序对 $R=\{(X,Y)|X,Y\in \Lambda\land X,Y\text{ satisfy }…\}$
归纳定义二元关系 $\rightarrow_R$ 如下:

  1. 对于任何 $M,N\in\Lambda$ ,若 $(M,N)\in R$ 则 $M\rightarrow_R N$
  2. $\rightarrow_R$ 是合拍的,即若 $M\rightarrow_R N$ 则

若 $M \rightarrow_R N$ ,则称 $M$ 一步 $R-$ 归约到(one step R-reduces to) $N$

归约,转换

归纳定义二元关系($R-$ 归约) $\twoheadrightarrow_R$ 如下:

  1. 对于任何 $M,N\in\Lambda$ ,若 $M\rightarrow_R N$ 则 $M\twoheadrightarrow_R N$
  2. $\twoheadrightarrow_R$ 是自反的和传递的,即

可以这样理解 $\twoheadrightarrow_R$ 就是经过任意次数的 $\rightarrow_R$ (包括零次,一次,许多次)
归纳定义二元关系($R-$ 转换) $=_R$ 如下:

  1. 对于任何 $M,N\in \Lambda$ 若 $M\twoheadrightarrow_R N$ 则 $M=_R N$
  2. $=_R$ 是等价关系,即

即在 $=_R$ 下,经过 $\rightarrow_R$ 归约的链条只要是无向联通的,它们就是等价的
显然 $\rightarrow_R,\twoheadrightarrow_R,=_R$ 都是合拍关系,且 $\twoheadrightarrow_R$ 是归约关系(即 $\twoheadrightarrow_R$ 是合拍的,自反的,转递的), $=_R$ 是同余关系(即 $=_R$ 是合拍的等价关系)


三条公理 ($\alpha,\beta,\eta$)

显然,我们有对应的 $\rightarrow_{\alpha(\beta,\eta)}$ (一步归约), $\twoheadrightarrow_{\alpha(\beta,\eta)}$ (归约), $=_{\alpha(\beta,\eta)}$ (转换)

设 $\beta\eta\equiv \beta\cup\eta$

则 $\rightarrow_{\beta\eta},\twoheadrightarrow_{\beta\eta},=_{\beta\eta}$ 也分别是一步归约,归约和转换

Diamond Property ($\diamond$ 性质,CR性质)

设 $\twoheadrightarrow$ 是一个传递关系,如果满足对 $\forall P,M,N$

则称 $\twoheadrightarrow$ 关系具有 Church-Rosser 性质
为什么叫 C-R 关系 $\diamond$ 关系,这其实很形象,如图
Diamond-Property

CR性质对于 $\twoheadrightarrow_{\beta},\twoheadrightarrow_{\eta},\twoheadrightarrow_{\beta\eta}$ 均成立,这里我们介绍 $\twoheadrightarrow_{\beta}$ 的证明,剩下的两个类似

准备工作

剩余

设 $R,S$ 为 $\lambda -$ 项 $P$ 的可约式,当 $R$ 被收缩时,将 $P$ 变为 $P’$ ,记作 $P\xrightarrow[R]{}_{\beta} P’$, $S$ 相对于 $R$ 的剩余是 $P’$ 中的可约式,且满足:

  • 情况1: $R$ 与 $S$ 在 $P$ 中无重叠,从而 $P\xrightarrow[R]{}_{\beta} P’$ 不改变 $S$,在 $P’$ 中不变的 $S$ 称为 $S$ 在 $P’$ 中的剩余
  • 情况2: $R\equiv S$ ,从而收缩 $R$ 就是收缩 $S$,此时 $S$ 在 $P’$ 中无剩余
  • 情况3: $R$ 为 $S$ 的部分且 $R\not\equiv S$, 从而 $S$ 呈形 $(\lambda x.M)N$ ,而 $R$ 在 $M$ 或 $N$ 中 ,收缩 $R$ 使得 $M\xrightarrow[R]{}_{\beta} M’$ 或者 $N\xrightarrow[R]{}_{\beta} N’$ , 从而 $S\xrightarrow[R]{}_{\beta} (\lambda x.M’)N$ 或者 $S\xrightarrow[R]{}_{\beta} (\lambda x.M)N’$ ,$(\lambda x.M’)N$ 或者 $(\lambda x.M)N’$ 就是 $S$ 的剩余
  • 情况4: $S$ 为 $R$ 的部分且 $R\not\equiv S$ ,设 $R$ 呈形 $(\lambda x.M)N$ ,收缩 $R$ 得到
    • 情形4.1: $S$ 在 $M$ 中,则在收缩 $R $ 以后,若 $x\in FV(S)$ ,则 $S$ 变为 $S\lbrack x:=N\rbrack$ 否则 $S$ 保持不变,因此 $S\lbrack x:=N\rbrack$ 或者 $S$ 就是 $S$ 在 $P’$ 中的剩余
    • 情形4.2: $S$ 在 $N$ 中,则在做代入 $M\lbrack x:=N\rbrack$ 时,每代入一次 $N$ 就得到一个 $S$ 的出现,这些皆为 $S$ 在 $P’$ 中的剩余

MCD

极小可约式

设 $R_1,\cdots,R_n$ 为 $\lambda-$ 项 $P$ 中的可约式, $R_i$ 是极小可约式是指 $R_i$ 不真包含其他 $R_j$

Minimal Complete Development

设 $P\in\Lambda,R_1,R_2,\cdots,R_n$ 是 $P$ 中的可约式,设 $P$ 通过依次收缩 $R_1,R_2,\cdots,R_n$ 的剩余得到 $Q$ ,若对于每一个 $i=1,2,\cdots,n,R_i$ 是 $R_i,R_{i+1},\cdots,R_n$ 中的极小可约式,则称 $P$ 归约到 $Q$ 的过程是一个 Minial complete development(MCD),记作 $P\rhd_{mcd}Q$

例子

过程 $(\lambda x.xt)((\lambda y.y)z)\rightarrow_{\beta}(\lambda x.xt)z\rightarrow_{\beta} zt$ 是 MCD
过程 $(\lambda x.xt)((\lambda y.y)z)\rightarrow_{\beta}(\lambda y.y)zt\rightarrow_{\beta} zt$ 不是 MCD

过程 $(\lambda x.xx)((\lambda x.x)y)\rightarrow_{\beta}((\lambda x.x)y)((\lambda x.x)y)\rightarrow_{\beta} y((\lambda x.x)y)$ 不是 MCD
令 $R_1\equiv(\lambda x.xx)((\lambda x.x)y),R_2\equiv ((\lambda x.x)y)$
这里先收缩了 $R_2$ ,再收缩的是收缩 $R_1$ 后产生的 $R_2$ 的剩余,因为 $R_1$ 不是 $\{R_1,R_2\}$ 中的极小可约式,所以该过程不是 MCD 过程
事实是不存在从 $(\lambda x.xx)((\lambda x.x)y)$ 到 $y((\lambda x.x)y)$ 的 MCD 归约

命题

  1. $n>0$ 时 $R_1,\cdots,R_n$ 中一定有极小者
  2. 当 $n=0$ 时 $P\rhd_{mcd} Q$ 就是 $P\equiv Q$
  3. 若 $P\rightarrow_{\beta} Q$ 则显然有 $P\rhd_{mcd} Q$
  4. $\rhd_{mcd}$ 没有传递性
  5. $P\rhd_{mcd} Q\Rightarrow P\twoheadrightarrow_{\beta}Q$ 反之则不成立,例如但是没有从 $(\lambda x.xy)(\lambda z.z)$ 到 $y$ 的 MCD 归约
  6. 给定 $P$ 与可约式的集合 $\{R_1,\cdots,R_n\}$, 若 $p\rhd_{mcd}Q$ 则 $Q$ 是唯一的

引理

引理1:
若 $M\rhd_{mcd}M’$ 且 $N\rhd_{mcd}N’$ ,则 $MN\rhd_{mcd} M’N’$

证明:
假设 $M$ 的收缩过程是 $R_1,R_2,\cdots,R_p$ , $N$ 的收缩过程是 $T_1,T_2,\cdots,T_q$
则一定可以把两者混合,使得新的收缩序列依旧满足 MCD 条件,因为:
首先保证在混合序列中 $R,J$ 依旧是按顺序排列的
若某个 $R_i$ 真包含 $T_j$ ,则在混合序列里把 $T_j$ 安排到 $R_i$ 前
对于 $T_j$ 真包含 $R_i$ 的同理


引理2:
若 $M\rhd_{mcd}M’$ 且 $N\rhd_{mcd}N’$ ,则 $M\lbrack x:=N\rbrack\rhd_{mcd} M’\lbrack x:=N’\rbrack$

证明:
按照变元约定,可设 $FV(xN)$ 不在 $M$ 中受约束,设 $M\rhd_{mcd}M’$ 依次收缩了 $R_1,\cdots,R_n$ 的剩余,以下对 $M$ 的结构作归纳证明 $M\lbrack x:=N\rbrack\rhd_{mcd}M’\lbrack x:=N’\rbrack$

  • 情况1: $M\equiv x$ ,从而 $n=0$ 且 $M’\equiv x$ 于是
  • 情况2: $x\not\in FV(M)$ ,从而 $x\not\in FV(M’)$ ,于是
  • 情况3: $M\equiv \lambda y.M_1$ ,即 $M$ 的可约式都在 $M_1$ 中,于是 $M’$ 呈形 $\lambda y.M_1’$ ,其中 $M_1\rhd_{mcd} M_1’$ ,因此
  • 情况4: $M=M_1M_2$ 且 $M$ 本身并非可约式,或者 $M$ 是可约式但在 $M\rhd_{mcd}M’$ 的过程中没有涉及收缩 $M$ 的剩余,因此 $M\rhd_{mcd} M’$ 过程中收缩的任何可约式皆在 $M_1$ 或者 $M_2$ 中,从而 $M’$ 呈形 $M_1’M_2’$ ,其中 $M_1\rhd_{mcd}M_1’$ 且 $M_2\rhd_{mcd}M_2’$ ,因此
  • 情况5: $M\equiv (\lambda y.L)Q$ ,且 $M$ 的剩余在 $M\rhd_{mcd} M’$ 的归纳过程中被收缩,其余被收缩的可约式均是 $L$ 或者 $Q$ 中可约式的剩余,因为 $M$ 包含了其他所有的可约式,根据 MCD 的定义, $M$ 的剩余必在归约的最后一步被收缩,故 $M\rhd_{mcd} M’$ 呈形其中 $L\rhd_{mcd}L’,Q\rhd_{mcd}Q’$ 根据归纳假设得因此

引理3:
若 $P\rhd_{mcd} A$ 且 $P\rhd_{mcd} B$ ,则存在 $T$ 使得 $A\rhd_{mcd} T$ 且 $B\rhd_{mcd} T$ ,如图所示
CR1

证明:
对 $P$ 的结构作归纳:

  • 情况1: $P\equiv x$, 则 $A\equiv B\equiv P$ ,取 $T\equiv P$ 即可
  • 情况2: $P\equiv \lambda x.P_1$ 从而所有的可约式皆在 $P_1$ 中,且 $A,B$ 分别呈形 $\lambda x.A_1,\lambda x.B_1$ ,其中 $P_1\rhd_{mcd} A_1$ 且 $P_1\rhd_{mcd }B_1$ 根据归纳假设知存在 $T_1$ 使得 $A_1\rhd_{mcd} T_1$ 且 $B_1\rhd_{mcd} T_1$ ,因此取 $T\equiv \lambda x.T_1$ 即可
  • 情况3: $P=P_1P_2$ 且 $P$ 本身非可约式,或 $P$ 本身为可约式但在 $P\rhd_{mcd} A$ 和 $P\rhd_{mcd} B$ 的过程中均未收缩 $P$ 的剩余,从而 $A$ 呈形 $A\equiv A_1A_2$ ,其中$B$ 呈形 $B\equiv B_1B_2$ ,其中 于是根据归纳假设,存在 $T_1,T_2$ 满足下图
    CR2
    取 $T=T_1T_2$ ,根据引理1可知定理成立
  • 情况4: $P\equiv (\lambda x.M)N$ 且在 $P\rhd_{mcd} A$ 和 $P\rhd_{mcd} B$ 的过程中仅有一个涉及收缩 $P$ 的剩余,不失一般性,可设 $P\rhd_{mcd} A$ 收缩了 $P$ 的剩余,从而 $P\rhd_{mcd} A$ 呈形其中 $M\rhd_{mcd} M’,N\rhd_{mcd}N’$ ,而 $P\rhd_{mcd} B$ 呈形其中 $M\rhd_{mcd} M’’,N\rhd_{mcd}N’’$ ,根据归纳假设可知对于 $M,N$ 存在 $M^+,N^+$ 使得满足下图
    CR3
    取 $T\equiv M^+\lbrack x:=N^+\rbrack$ 因为 $A\equiv M’\lbrack x:=N’\rbrack$ 由引理2知 $A\rhd_{mcd} T$ ,又因为所以 $B\rhd_{mcd} T$
  • 情况5: $P\equiv (\lambda x.M)N$ 且 $P\rhd_{mcd} A$ 和 $P\rhd_{mcd} B$ 均涉及收缩 $P$ 的剩余,从而 $P\rhd_{mcd} A$ 呈形其中 $M\rhd_{mcd} M’,N\rhd_{mcd} N’$ 而 $P\rhd_{mcd} B$ 呈形其中 $M\rhd_{mcd} M’’,N\rhd_{mcd} N’’$ ,根据归纳假设可知对于 $M,N$ 存在 $M^+,N^+$ 使得满足下图
    CR4
    取 $T\equiv M^+\lbrack x:=N^+\rbrack$ 于是所以 $A\rhd_{mcd} T$ 且 $B\rhd_{mcd} T$

定理: $\twoheadrightarrow_{\beta}$ 具有 CR 性质

证明:
设 $P\twoheadrightarrow_{\beta} M,P\twoheadrightarrow_{\beta} N$ 只需要证明:

因为如果上式成立,设 $P\rightarrow_{\beta} M_1\rightarrow_{\beta}\cdots\rightarrow_{\beta}M_n\equiv M$ ,如下图
CR5
令 $T\equiv T_n$ ,则显然 $M\twoheadrightarrow_{\beta} T\land N\twoheadrightarrow_{\beta} T$
又因为 $\rightarrow_{\beta}$ 归约是 $\rhd_{mcd}$ 归约,且 $\rhd_{mcd}$ 归约是 $\twoheadrightarrow_{\beta}$ 归约,所以要证明 $(*)$ ,只需证

下面对 $P\twoheadrightarrow_{\beta} N$ 的归约步数 $k$ 作归纳以证明上式:

  • k=1,即 $P\rightarrow_{\beta} N$ ,从而 $P\rhd_{mcd} N$ ,根据引理3知又因为 $M\rhd_{mcd} T\Rightarrow M\twoheadrightarrow_{\beta} T$ 所以上式成立
  • 假设归约步数等于 $k$ 时成立,当归约步数等于 $k+1$ 时,设 $P\twoheadrightarrow_{\beta} N’\rightarrow_{\beta} N$ ,其中 $P\twoheadrightarrow_{\beta} N’$ 的归约步数等于 $k$ 则根据归纳假设因为 $N’\rightarrow_{\beta} N\Rightarrow N’\rhd_{mcd} N$ ,所以根据引理3于是且 $N\rhd_{mcd} T$ ,所以原式成立,证明过程如下
    CR6

类似可证明 $\twoheadrightarrow_{\eta},\twoheadrightarrow_{\beta\eta}$ 都具有CR性质