日々の流転

λ. チャーチ・ロッサーの定理の証明に挫折

ここ数日Agdaでチャーチ・ロッサーの定理を証明することに熱中していたのだけど、なんか上手くいかずに詰まっていた。チャーチロッサーの定理の証明の流れの本質的な部分はすぐに書けていたのだけど、細かい部分で色々とひっかかったり嵌ったりとか。

特に任意のラムダ式 M1[x,y], M2[y], M3 に対して M1[x:=M2[y]][y:=M3] = M1[y:=M3][x:=M2[y:=M3]] が成り立つことの証明。構造帰納法で示せば良いのだけど、実際にAgdaで証明を書こうとするとラムダ抽象の場合が面倒過ぎで……。 その後、ラムダ式のデータ型「data Term a = Var a | App (Term a) (Term a) | Lam (Term (Maybe a))」*1がモナドになっている事を証明出来れば良く、直接証明するよりもその方が筋が良さそうという事に気付いたのだけど、「(m >>= f) >>= g = m >>= (\x -> f x >>= g)」の証明のラムダ抽象の場合がやっぱり面倒過ぎで……

結局、まだその部分の証明は書けていないけど、燃え尽きたので中断。

λ. 『謎の彼女X (2)』 植芝 理一

いつの間にか二巻が出ていた。