from ラムダ計算

略して「CR性がある」などとも言う

名前の由来はAlonzo ChurchとJohn Barkley Rosser

同じラムダ式はどの順番で簡約しても、それ以上簡約できない状態になったとき、それらは必ず一意になる

任意のラムダ抽象はたかだか1つのβ正規形しか持たない

正規形を持たないものもある

ex. ((\lambda x.xx)(\lambda x.xx))

β簡約がChurch-Rosserの定理を満たす\Leftrightarrowβ簡約がβ簡約の合流性を持つ

証明 ref p.90

定理

\forall M,N\in\Lambda[M=_\beta N\Rightarrow \exist L\in\Lambda[M\xrightarrow{\ast}_\beta L\;\mathrm{かつ}\;N\xrightarrow{\ast}_\beta L]]

前提

\Lambdaはラムダ抽象の集合

証明

いろいろある

付録A

TaitとPer Martin-Löfの証明

『C言語による計算の理論』 付録B.1

これは I(IΩ) の簡約グラフ

あくまでも「簡約しきったときに同じものに到達する」ことを言っているのであって、

「簡約を繰り返したら同じものに到達する」とは言っていない

上図のようにループがあり得るので、適切なルートを選んで簡約を進めないといけない