チャーチ・ロッサーの定理

チャーチ・ロッサーの定理（チャーチ・ロッサーのていり、英: Church–Rosser theorem）とは、同じラムダ式から始まる二個の異なる簡約がある場合、それぞれの簡約から一連の簡約を行うことで到達可能な式があることを述べる定理である。詳しくは合流性を参照。