参考：http://d.hatena.ne.jp/m-hiyama/20090204/1233722560
ヒヤマセミナー第二段です。もう懇親会は終了してる頃ですね。私は出ずにお暇しちゃいましたが。
池袋の会場は満席でした。空調のクーラーがかかるほどに途中暑かったです。
前半はラムダ計算のお絵描き、後半は計算機の停止性の話でした。後半の結論としては「バグのないソフトは作れません」ということです*1。
上のような言明の是非（というか可否？）について、こちらで議論しています。私は今のところ、上の文言を修正する気は全くありませんが、誤解を生みやすいことは事実ですので、時間があればリンク先を確認してみてください。後、脚注は必ず参照のこと。
しかし、すべてを超越している神様の世界と、すべてが論理で片付く計算機の世界の狭間に生きる我々人間は、理屈では無理とわかっていても、上司から「やれ」といわれたら天竺に飛ばされてもやらなきゃいけないという不条理の世界に生きているのです*2。しみじみ。
そういやあのとき、友人（職業プログラマですが停止性の話とかはたぶん知らない）が言ってくれた一言が至言だった、と改めて感じました。
「その天竺の教えがバグってね？」
…いや、本当の結論の結論は（正確な文言は忘れましたが）「我々は不可知の知を知ることはできる。これはなんと不思議なことよ」ということだったんですが、いやまったく、私もそう思います。人間はこの自己言及のパラドックスの落とし穴がどこにありそうかを見定め、あまつさえ構造を外側から眺めてたりできるんですよね。なので、穴ぽこだらけの計算機でも十分やっていけているという。
たまに無理解な上司に「穴のない計算機を作れるようにしろ」とか言われて困ったりする程度で（まだ言うか）
ところで、お絵描き（ラムダ計算）の話がなんで計算可能性の話につながるの？檜山さんはどうつなげたかったの？というところで、セミナーが終わった後はてはて、と思っておりまして。で、前回もご一緒したKuwataさん（顔と名前が一致せず、失礼しました）がたまたま今回席が前後してて、終わった後やっぱり同じ質問を私にされて。
たぶん、ラムダ抽象（f を f^ にする操作）が入ることでコード（関数）とデータ（値）が同じ整数/バイナリにエンコードできるようになって、その2つが一緒くたに扱えるようになったからパラドックスも発生するようになったってことですかね、とその場で答えてしまったんですが、はてさて模範解答だったかどうか。大きく外れてはいないと思ってるんですが。
あとそうそう。話は前後しますが、前半のラムダ計算のお絵描きの方。
少し気になって、休憩の合間に檜山さんとも議論したんですけど、評価エンジンＥの型は、受け取る関数の引数の数ではなく、ハット(^)の数に依存するはず。
なので途中、
f(x,y) = E2(f^(x), y)
f(x) = E1(f^(), x)
と、上下の2式のEが違う型だという解説がなされていたんですが（Eの添字に注目）、引数の型を無視すれば同じになると思います。
時間があったらもっと書くかもしれませんが（たぶんない）、とりあえず、備忘録。
そんなこんなで、次回も楽しみにしております。
