简介
于理论计算机科学中, Church-Rosser 定理 讲述了当我们尝试给任意 \(\lambda\)-表达式 的变体应用 \(reduction\) 规则时, 不管所规约排序如何, 也定不会影响到最终的运行结果. 该定理由 Alonzo Church 与 J. Barkley Rosser 于 1936 年时证明得出, 并以他们的名称所命名.
\(\beta\)-范式 (\(\beta\)-normal form, \(\beta\)-nf)
定义
- \(\beta\)-redex 的项是类似于 (\(\lambda x. M)\ N\) 这样的表达式, 而这个例子中 \(M[x := N]\) 则是其的 \(contractum\).
- 一个 \(\lambda\)-项 \(M\) 被称为 \(\beta\)-nf 若其没有 \(\beta\)-redex 作为子表达式.
- 对于 \(\exists N\), 若有项 \(M =_{\beta} N\) 且 \(N\) 本身存在 \(\beta\)-nf, 则 \(M\) 亦有 \(\beta\)-nf.
例如 \((\lambda x. xx)\ y\) 本身并不是一个 \(\beta\)-nf, 但于 \(\beta\)-规约 之后存在项 \(yy\), 这便是一个 \(\beta\)-nf 了.
引理
设有 \(M, M', N, L \in \Lambda\).
设 \(M\) 为 \(\beta\)-nf, 则有 \(M \twoheadrightarrow_{\beta} N \implies N \equiv M\).
若 \(M \to_{\beta} M'\), 则有 \(M[x := N] \to_{\beta} M'[x := N]\)
证明
由于 \(M\) 是 \(\beta\)-nf, 定不存在任何的 \(\beta\)-redex, 所以永远都不会有 \(M \to_{\beta} N\) 的情况出现. 因此即使有 \(M \twoheadrightarrow_{\beta} N\), 也势必是 \(M \equiv N\).
直接应用 \(\to_{\beta}\) 的规则进行规约亦能得出同样的结果.
Church-Rosser 定理
定义
若果 \(M \twoheadrightarrow_{\beta} N_1, M \twoheadrightarrow_{\beta} N_2\), 则存在某些 \(N_3\) 有 \(N_1 \twoheadrightarrow_{\beta} N_3\) 且 \(N_2 \twoheadrightarrow_{\beta} N_3\), 如图:
\[ \xymatrix{ & M \[email protected]{->>}[ld] \[email protected]{->>}[rd] & \\ N_1 \[email protected]{.>>}[rd] & & N_2 \[email protected]{.>>}[ld] \\ & N_3 & } \]
