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

3行要約

1. ラムダ計算において、項の書き換え順序によらず最終的な結果が一意に定まることを示す定理。
2. 計算の合流性（コンフルエンス）を保証し、計算体系の整合性を証明する。
3. 関数型プログラミング言語の理論的基礎を支える重要な定理である。