Church-Rosser の定理 - yoshitake-hのブログ

「式 $f(x)$ の中の $x$ に $a$ を代入する」という操作を
$(\lambda x.f(x))a\underset{\beta}{\longrightarrow} f(a)$
と書こう，というのが λ-calculus．この操作を β-reduction という．

β-reduction の合成を $M\to N$ と書くことにすると，Church-Rosser の定理は， $M\to N_1,\,M\to N_2$ のとき， $N_1\to N,\,N_2\to N$ となる式 $N$ が存在することを主張する．
証明のポイントは，β-reduction の特定の合成である parallel reduction というものを考えること．