「式 の中の に を代入する」という操作を と書こう，というのが λ-calculus．この操作を β-reduction という．β-reduction の合成を と書くことにすると，Church-Rosser の定理は， のとき， となる式 が存在することを主張する． 証明のポイントは，β-redu…