ヒヤマセミナー（２，３）に行ってきたよ
日時：2009/2/19（木）、2009/3/19（木） 18:00〜21:00
場所：マイ・スペース＆ビジネスブース 池袋西武横店7号室
参加人数：ｲﾊﾟｰｲ
http://d.hatena.ne.jp/m-hiyama/20090204/1233722560
http://d.hatena.ne.jp/m-hiyama/20090309/1236559613
前回エントリ
-
手元にセミナーのメモがあるので、ちょっと振り返ってみる。でもすでに他の参加者の方がまとめてくれてるので、なるべくゆるーく。「お絵描き分」高めで。
まず復習。関数を以下のように描く。
例として２引数関数ｆの場合。上に出てる２本のヒゲは引数、下の１本は戻り値。大文字のアルファベットは型を意味する。
-
次、カリー化とは。
(1)から、ｙのヒゲを残してｆがぼよんと飛び出す感じで?になる。元のｆとは少し違うのでｆ^と呼ぶことにする。ｆ^からはｘのヒゲが伸びている。ｙのヒゲが伸びているほうは意味ありげにE1とか書いているけど、あまり気にしなくていいかもしれない。EngineのＥとかEvalのＥとかの意味だそうで。
この変形操作がラムダ変換とか、カリー化とか。（と個人的に思っている）詳しく聞かないでください。
(2)から(3)へ、もう一段階変形することができる。ｆともｆ^とも違うのでｆ^^と呼ぶ。ｆ^^の上にはヒゲは伸びていず、代わりにE2からｘのヒゲが伸びている。
これが檜山さんの言うところのオダンゴ図。
-
これだとわかった気になる（ならん？）だけかもしれないので、数式でも書きましょう。
関数ｆが、実は ２ｘ＋ｙ という式だった、という設定で以下のように書く。縦棒の前が引数で後が式です。関数適用をすると＜＞が取れます。
ｆ ＝ ＜ｘ，ｙ｜２ｘ＋ｙ＞
関数適用：ｆ(ｘ，ｙ) ＝ ２ｘ＋ｙ
ラムダ変換してみる。
ｆ＾＝ Λ＜ｘ，ｙ｜２ｘ＋ｙ＞
＝ ＜ｘ｜λｙ．(２ｘ＋ｙ)＞
関数適用：ｆ＾(ｘ) ＝ λｙ．(２ｘ＋ｙ)
Λというのは、関数をラムダ変換するための演算子。実際にやっているのは引数ｙを取り外して、λをつけて縦棒の右側に移動。これで完了。
上の図で言うと(2)の段階に来てる。図を見ると確かに、ｆ＾はｘを引数として、得体の知れないものを返している。この得体の知れないものがλｙ．（２ｘ＋ｙ）に対応する。
もう一段階、ラムダ変換。
ｆ＾＾＝ Λｆ＾
＝ Λ＜ｘ｜λｙ．(２ｘ＋ｙ)＞
＝ ＜｜λｘ．λｙ．(２ｘ＋ｙ)＞
関数適用：ｆ＾＾() ＝ λｘ．λｙ．(２ｘ＋ｙ)
ｆ＾＾は引数を取らず、しこたま得体の知れない λｘ．λｙ．(２ｘ＋ｙ) というものを返す関数、とわかる。
-
ｆとｆ＾とｆ＾＾はどういう関係があるのか？
ここにきて上の図のE1, E2が意味を持つ。E1はｆ＾から出た得体の知れないものとｙとを受け取り、関数の値ｆ(ｘ，ｙ)を返す。
ｆ(ｘ，ｙ) ＝ Ｅ１(ｆ＾(ｘ)，ｙ)
ｆ＾(ｘ) ＝ Ｅ２（ｆ＾＾()，ｘ)
-
ここら辺までが第２回の前半部。
第２回の後半部はちょっと置いといて、
第３回の前半部は諸事情により遅刻して、
第３回の後半部。来た、見た、え？論理学？ここ教養？
詳細はKuwataさんのエントリを見てくださいということで。
-
オダンゴ図にタプルを導入しよう。
右上のｘとｙをまとめてタプルをつくる。ｆはタプル１個を引数に取る関数と見ることもできて、それをラムダ変換したのが上の図。
この図と、以下の証明図。似てない？
A B
-------- [And]
A ∧ B ⇒ C A ∧ B
-------------------- [MP]
C
（Kuwataさんとこから引用）
この証明が言わんとしているのは、「A ∧ B ⇒ C」なるルールと、Ａと、Ｂという３つの前提からＣを導くことができまっせという、まっとうな証明。
２つの図をじーっと眺めていると、オダンゴ図中で黒丸で示している操作がそれぞれ証明の各ステップに対応している。タプルを作る操作は証明図でいう[And]、関数適用は[MP]。
んで、どうもこの、「ラムダ計算と命題論理の証明との間に完全な対応があるんだぜ！」ていう、意見or仮説or原理のことをカリー＝ハワード対応というそうだ。Wikipediaに項目がないのが痛い。困ったときのen:Wikipdia。んー法則かな？
-
オダンゴ図をもう少し変形。
赤い丸の部分を３引数の関数とみて、カリー化でｙとｘを下に延ばす。
右側では対応する証明。カリー化に対応するものは[DT]という規則。本当に１対１に対応しているらしい。証明は全体として恒真文「Ａ∧Ｂ⊃Ｃ ⇔ Ａ⊃（Ｂ⊃Ｃ）」の証明になっている。なんてことだ！ お絵かきで証明ができてしまった。
-
ここでメモは途切れている。
残り３０分くらいから檜山さんの進行スピードが徐々にあがりはじめ、このへんで音速を超えてたので、ペンをおいてただスライドを眺めているしかなかった。
-
ふだん仕事で使ってないような頭の部分が刺激されたような感じで楽しかったです。
檜山さん、参加者の皆さん、３回にもわたるセミナーお疲れ様でした。多謝
