简介

于理论计算机科学中, Church-Rosser 定理 讲述了当我们尝试给任意 \(\lambda\)-表达式 的变体应用 \(reduction\) 规则时, 不管所规约排序如何, 也定不会影响到最终的运行结果. 该定理由 Alonzo ChurchJ. Barkley Rosser 于 1936 年时证明得出, 并以他们的名称所命名.

\(\beta\)-范式 (\(\beta\)-normal form, \(\beta\)-nf)

定义

  1. \(\beta\)-redex 的项是类似于 (\(\lambda x. M)\ N\) 这样的表达式, 而这个例子中 \(M[x := N]\) 则是其的 \(contractum\).
  2. 一个 \(\lambda\)-项 \(M\) 被称为 \(\beta\)-nf 若其没有 \(\beta\)-redex 作为子表达式.
  3. 对于 \(\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\).

  1. \(M\)\(\beta\)-nf, 则有 \(M \twoheadrightarrow_{\beta} N \implies N \equiv M\).

  2. \(M \to_{\beta} M'\), 则有 \(M[x := N] \to_{\beta} M'[x := N]\)

证明

  1. 由于 \(M\)\(\beta\)-nf, 定不存在任何的 \(\beta\)-redex, 所以永远都不会有 \(M \to_{\beta} N\) 的情况出现. 因此即使有 \(M \twoheadrightarrow_{\beta} N\), 也势必是 \(M \equiv N\).

  2. 直接应用 \(\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 & } \]