2007-08-24 [長年日記]
λ. チャーチ・ロッサーの定理の証明
先日は「燃え尽きたので中断する」と書いたが、どうにも気になって頭から離れずモヤモヤしていたら、今日の飲み会中にアイディアを思いついて、結局証明できた。 まだ整理できていない部分が多いが、こんな感じになっている。
【2007-09-09追記】 Frank Pfenning が A Proof of the Church-Rosser Theorem and its Representation in a Logical Framework で LF (の実装のElf)で証明を表現している。後で比較する?
λ. 同期飲み会
![[OTL party]](./images/20070824_0.jpg)
挫折禁止
OTLは「お酒を楽しもうラボ」か何かの略なんですが、どう見ても狙って名前を付けたとしか……
＞飲み会中にアイディアを思いついて<br>すごい。<br><br>で、さらに進化形として、勤務中でもバックグラウンドで業務とは関係ないコトの「アイディアを思いついて」…<br>んなことはない（かな？）。
関係ないことをしている時にアイディアを思いつくというのは良くありますし、当然仕事中に思いつくこともあります (^^;