参考：http://show.zoho.com/public/takeo.bono/lambda%20calculus%20and%20CCC
このスライドは、「ラムダ計算と圏論を学びたがっている量子物理学研究者」という、超偏ったターゲット層を狙って書かれているため、あんまり一般向けの説明とはいえません。あと、狙いが外れたところもあったんで。
以下、思っていたことなどを箇条書き。自分用メモも兼ねてるので、後で編集するかもです。
- 一番の狙いはラムダ計算と量子情報との接点。
- ポイントは monoidal product と currying です。
- でも途中のストーリーが、物理屋さんにはちょっと回りくどくなっています。
- 回りくどくなってしまったのは、monoidal productが登場するまでに monad → λc → closed Freyd category と進めているため。途中の説明に必要な概念が多すぎました。
- この流れを思いついたのは、haskell-cafe MLのこのスレをふと思い出したから。
- そういう意味では、この流れは計算機屋向けだったかもしれません。
- 逆に、計算機屋さんには、closed Freyd category とか κ category が Arrows の背景理論になってることを知っとくと楽しいかもしれません。
- ただし、レベル設定は高めです。
- 一箇所、普通の計算機屋（というか、非物理屋）さんにはすぐに理解できないものをあっさり導入している箇所があります。「随伴」（adjointness, adjunction）です。
- 物理屋さんは共役だのwikipedia:随伴作用素だのに慣れ親しんでる為、随伴の概念を全く苦にしないことを身近なサンプルで知ってました。なので、説明全くナシに使ってます。
- サブの狙いは「計算機屋がなんで圏論をやってるのか」を物理屋さんに説明すること。その辺の理由は、ジョニーとの事前の会話で、ゲストがそういうのに興味があると聞いてたので。
- だから、なるたけ計算機屋のロジックで話を進めたかったという気持ちがあります。途中の話がモナドとか経由したのはそういう理由もあります。
- 絵算系は敢えて最後に軽く触れるだけにしました。ほっといても、いずれその話題にはなるだろうと踏んでたんで。
- ちょうど話し終わって、絵算の質問が出たところでエキスパートに話をつなげたので、なのでこの狙いは僕的には大正解だった訳ですがｗ
- λ計算は本来なら（正統的には）α、β（＋η）の各conversionをもって説明するのが正しいと思うのですが、このスライドでは省いてます。
- 代わりに出てくる、Projection, Abstraction, Application は、単純型付きラムダ計算の型付け規則です。
- なんでこうしたかって言うと、currying を圏論ベースで説明する（＋最後の絵算まで持っていく）にはこっちの方が都合が良かったからです。
- この辺、ヒヤマセミナーの説明はうまいなと後で思いました。特に、大きいラムダと小さいラムダ、あたり。
- monad → λcの辺りは書ききれなかったので未完成。
- 本番ではホワイトボードで説明しました。
- ていうか、ここでスライド1枚は明らかに無理がありました。ええ。
- 本番ではホワイトボードで説明しました。
