技術者／プログラマのためのラムダ計算、論理、圏 第3回に行ってきた

実は第2回にも行っていたんだけど内容をまったく咀嚼できず、そのうちやろうと思っているうちに第3回が開催されてしまった ^^;

第2回 ラムダ計算と停止性問題
第2回は、主にラムダ計算について。前回の復習からはじまって、回路図のような絵を交えながらラムダ抽象化につなげていき、最後はJavaScriptのようなCのような疑似コードを使って、チューリングマシンの停止性問題を背理法で証明して終わった（と思う）。詳しくは、檜山さんのBlogに書いてあるので、そちらを見た方が良いと思う。

セミナー資料
紙芝居：ラムダ抽象
セミナー非参加者にもわかるリアルワールド向けラムダ計算
なぜ停止性について話したのか？

第3回 自然演繹と型付きラムダ計算、カリー／ハワード対応
第3回は、カリー・ハワード対応についての感覚的な理解がゴール。第2回とはうってかわって論理を中心に話をすすめていき、論理でやっていることが最終的にラムダ計算に対応することを感覚的に理解することで、カリー・ハワード対応を感じるのが目的、という感じ。こちらも、檜山さんのところに、他の参加者さんのまとめへのリンクを含めてきちんと色々書いてあるのでまとめは書きません、というか書けません！

セミナ資料
カリー／ハワード（Curry-Howard）の対応を知らない子供達および大人達へ
演繹系の話題と演習

もともと、「素数の音楽」「暗号解読」「論理学入門」あたりの書籍や、TM（T字形ER）のセミナでの疑問（数理論理学まわり）解消のためにちょこちょこ調べていたこともあって、今回の話の大半は馴染みがあった。とはいえ、雰囲気つかむことを重視してたので、導入規則や除去規則についてあまりよくわかっていなかったのだが、今回具体例をもとに理解できたのはとても良かった。
セミナの内容の本筋としては「計算と論理は以下のように対応する」

論理	算術
演繹系	算術回路キット
推論	基本演算
証明図	計算図
演繹系の証明図	算術回路キットの計算図
証明可能	計算可能
derived rule	計算のマクロ
公理	最初から使える定数
定理	計算済み定数

でFAな感じなんですが、話の中でちらちら出てくる用語や、自分が既に知っていることとの関係がよくわからなくてもやもやしている。というか、聞けば聞くほど疑問が増えるという状態...

• 檜山さん的アプローチでのラムダとは少しは仲良くなった気がするが、一般的（形式的というか記号的というか）なラムダ計算についてイマイチわかっていない感
• カリー／ハワード対応が何を意味しているのか（この理解が何につながっていくのか）
• 自然演繹以外の演繹系と、型付ラムダ計算以外の計算も対応するのか？
• フォーマルメソッドや自動証明との関係は？
• プロセス論理との関係は？
• 型推論との関係は？
• 結局、絵算というのは何がエキサイティングなんでしょう？

檜山さんのエントリによると、話題同士の関係についてこれからいくつかエントリをあげつつ説明してくださるようなので、それらのエントリをながめつつ、自分なりに理解を深める過程を書いていこうと思う。ううむ...文系は土台からしてしょぼいからつらいなぁ...。

何か関係ありそうなリンク
型＝命題、プログラム＝証明
　Haskellを例に、型推論との関係について説明してくれそう。
Curry-Howard対応を知らないこども達
　サーセン（笑）
Curry-Howard Isomorphism
　ざっと読んだけど、概要を把握するにはとても良さそう。
CiteSeer : Curry-Howard Isomorphism
　カリー／ハワード同型対応についてきちんと書いてあるらしい論文。
自然演繹-Wikipedia
　型理論や線形論理との関係も書いてある。
ラムダ計算-Wikipedia
　ここに書いてあることが「そりゃそうだよねぇ」と言えるくらいにはなりたい。