2009年3月21日土曜日

技術者/プログラマのためのラムダ計算、論理、圏 第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
 ここに書いてあることが「そりゃそうだよねぇ」と言えるくらいにはなりたい。

1 件のコメント:

kentaro さんのコメント...

はぁ...色々書いたあとでFFが落ちたよ...気を取り直して。

http://www.kmonos.net/wlog/61.html#_0538060508

ここに思った以上に幅広く色々書いてあったので、概要レベルの疑問点はかなり解消された気がしている。

・Curry-Howard対応は、直観主義命題論理の命題と単純型付きラムダ計算の型が、また自然演繹の証明と単純型付きλ計算のプログラムとの対応を言う
・否定は継続に対応するらしい。Schemeとかにあるらしい。使ったことない。
・二重否定除去則を認めないと証明できないような命題でも、not notをつけてまわれば証明できる命題に変換できる、という定理があるらしく、これにCPS変換というのが対応するらしい
・ヒルベルトスタイルの証明(演繹系?)は、ラムダ計算ではなくSKIコンビネータというものに対応するらしい
・普通(?)の言語の型システムでは(1+1=2)のような命題を型として表現できないが、定理証明系の言語ではこういうものまで表現できたりするらしい