さらにさらに「ラムダ計算、論理、圏」セミナーへの補足・応答： 今日中に他のエントリーにも一言二言。
映画マトリックスは好きな映画の一つだ。
マトリックスの世界、ミニモイの国、ネバーランドなんかを妄想するのはいいよね、仮想の世界のなかに入り込んだり世界を外から眺めたり。マジでトレーニングになるよ。
限られたロジックで世界を認識する知的生命体は何処まで世界を認知できるかと言うことを考えてみたい。
この問題意識は重要だと思います。「閉圏、弱いラムダ計算、弱い論理」における、「“そとの人”と“なかの人”」の議論はまさにこの問題です。
実際のプログラミング言語のラムダ式って、ぶっちゃけ大きなラムダ式だよな普通。例えば Hakell の場合、ラムダ抽象は以下のどっちでもいい。
\x -> \y -> x + y
\ x y -> x + y
実際のプログラミング言語のラムダ式が何を意味するかは、プログラミング言語や実行環境の問題じゃありません。僕らの気持ちや心の問題です。ある式が、現実的であれ仮想的であれ、世界のなかの実在物を記述しているんだ、という解釈であればそれは大きなラムダ式として読めます。一方、記号計算機に実行させる高級機械語を手で書いているんだ、と思えばそりゃ小さなラムダ式。それぞれ、表示的意味論と操作的意味論に基づく解釈と言ってもいいのかも知れません。
それと、\x y -> x + y って書き方が2引数を表しているわけじゃなくて、単なる略記。教科書に載っているラムダ計算でも、λx.λy.M は λxy.M と略記します。しいて2引数関数といえば、1タプル引数の \(x, y) -> x + y かな。ほんとの多引数とタプル1引数の関係はけっこう難しいです（今は触れない）。
タイポなのか意図的なのか：
何か書いてて怪しくなってきたけど、こんな氷原にしかならんなあ。
寒い？
ある程度の表現力（氷原力じゃない）と計算力を持つ計算機構は、必然的に自己言及の能力を獲得してしまうんだよね。それで自己言及に起因するパラドックスも必然的に抱え込んでしまう、と。能力の獲得に伴い不可能性を受け入れざるを得ない点が面白いですね。
