Church-Rosserの定理

Church-Rosser theorem

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

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

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

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

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

証明 ref 『(理論)12 計算モデルの基礎理論』.icon 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はラムダ抽象の集合

証明

いろいろある

『(理論)12 計算モデルの基礎理論』.icon 付録A

TaitとPer Martin-Löfの証明

https://gyazo.com/a78636b88d5b882f0c6524f4a86b99c4

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

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

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

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