次回でシリーズ完結です。首尾よくマトマリが付かなくても、このタイトルはオシマイ*1。さて次回＝最終回ですが、2/3程度は以前の知識を要求しない内容なので、第3回だけ参加も可能ですし、歓迎します。以下に、予定している内容を記します*2。ただし、予定とかなり変わってしまう可能性があることはご承知おきください。
もともと僕が「技術者／プログラマのためのラムダ計算、論理、圏」セミナー・3回シリーズ*3を企画した主たる動機は、カリー／ハワード対応を紹介したかったことです。カリー／ハワード対応は、命題論理と型付きラムダ計算のあいだに対応関係があり、その対応により「命題論理とラムダ計算は事実上同じものだとみなせる」ことを主張します。
カリー／ハワード対応というと、なにか小難しくて近付きがたいような印象がありますが、ラムダ計算を“お絵描きで行う”手法（pictorial calculation）を使えば、とても簡単に説明できてしまいます。失礼なのを承知で言ってしまえば、「こんな当たり前のことが大定理なの？」と思えてしまうほどです*4。
第3回では、論理的証明を“お絵描きで行う”手法を紹介します。元来論理では、証明図（proof-figure）という絵を使って「形式化された証明」を表現するので、“お絵描きによる証明”は変わった方法ではなくて正統派なのです。とはいえ、証明図に慣れていない人も多いでしょうから、2/3の時間を使って証明図に慣れてもらいます。今考えている例題は、中学校の連立一次方程式です。
実際にやってみると、連立一次方程式の形式化はけっこう難しくて「こんなもんよく中学校でやるよなー」との感慨を抱きます。そういう次第で、適当にはしょらないと3時間かかっても連立方程式が終わりそうにないです。はしょりますよ、当然。
カリー／ハワード対応で扱うのは連立方程式よりはずっと簡単な命題論理の体系です。もっと正確に言うと、連言（「かつ」）と含意（「ならば」）を含んだ論理式を、自然演繹の流儀で証明するような命題論理体系です。自然演繹の証明図の描き方を少し変えると、それがズバリ、ラムダ式の絵になっているという寸法です。
この道筋に沿えば、厳密性には若干の難があるものの、直感的にカリー／ハワード対応を把握できると思います。しかしそれでも、なんでこんな対応（同型）が存在するのかはミステリアスで、「不思議だが本当だ」という結論になりそうですね。
あーそれと、アンケートによると「もっとちゃんと圏論を導入してくれ」という声が思いのほか多いのですが、ウーン、それはちょっと難しいかなー。別な機会に別なタイトルでやるかもしれませんが、今の文脈内ではチラッと触れるくらいでカンベンしてください。
ちょっと事情があって今すぐ申し込み受け付けができません。
と書いたのは、申し込みページ（とそのバックエンド）をErlang+YAWSで作ろうかということだったのですが、なんか間に合いそうにありませんな。手作業で受け付けかな、やっぱり。
