「技術者／プログラマのためのラムダ計算、論理、圏」セミナー第2回

行ってきました。自分なりに復讐、もとい復習。
前半はラムダ計算の話。
たとえば g = < a,b,x | a*x+b > という関数を考えるとき、g^ = < a,b | λx.a*x+b >、g^^ = < a | λb.λx.a*x+b >、g^^^ = < | λa.λb.λx.a*x+b >という関数を作ることができる（これがラムダ抽象？）。
絵にすると↓こんな感じ。

これを見てて思ったのが、↓みたいに定義して、g1 が g^、g2 が g^^、g3 が g^^^ にそれぞれ対応していると考えてはどうか？ということ。絵の複雑さと式の複雑さが一致していて、納得しやすい気がします。
そうだとすると g, g1, g2, g3 は“等しい”ので、g, g^, g^^, g^^^ も“等しい”と考えていいのかな。
別の言い方をすると、g :: Int -> Int -> Int -> Int を Int -> Int -> (Int -> Int) と解釈するか、Int -> (Int -> Int -> Int) と解釈するかの違いでしかないのでは、と思います。
[追記] 色々と問題があったので訂正しました。

Prelude> let g a b x = a * x + b
Prelude> g 3 5 7
26
Prelude> let g1 a b = (+ b) . (* a)
Prelude> g1 3 5 7
26
Prelude> let g2 a = (. (* a)) . (+)
Prelude> g2 3 5 7
26
Prelude> let g3 = (. (+)) . (flip (.)) . (*)
Prelude> g3 3 5 7
26

で、実際に g^^^ を評価する過程は↓（E₁ や E₂ とかのナンバリングは間違ってるかも）。E₁ と E₂ を区別する必要はないんじゃない？というのは、やはり後で話題になっていました。仮に、出力される関数（λx.3*x+5）と値（26）を区別するのであれば、この絵での E₁ は若干扱いが変わってきて、E₂ や E₃ も、値を得るまでにあと何回評価する必要があるかという回数（番号）を意識する必要が出てくるんじゃないか、という結論でした。

後半は計算可能性の話。
このあたりにも載ってるし、説明は理解できるのですが、何となく腑に落ちない（騙された気がする）ところがあります。
形式的な記号操作で証明できると嬉しいなぁと思ったのですが‥‥これは自分への宿題かな。

その他、雑感。

• スーツは 2/30 でした。みんなどんな仕事をしてるんだろう。
• Haskeller は、いるところにはいるものだと思いました。ただ集団で生息しているのは、まだ見たことありません。
• 量子ファイナンス工学w

最後になりましたが、このような機会を作っていただいて、檜山さんありがとうございます。