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

チャーチ・ロッサーの定理は、同じラムダ式から始まる二個の異なる簡約がある場合、それぞれの簡約から一連の簡約を行うことで到達可能な式があることを述べる定理である。