計算の圏は集合圏とは全然(！)違う

http://d.hatena.ne.jp/m-hiyama/20090221/1235192629 ：

バイナリ関数コードφ∈N^Nが与えられると、f(x) = E(φ, x) としてfを再現できます。このことは、N→N という関数とN^Nのデータの間に1：1の対応があることを意味します。ただし、この1：1対応に関しては、かなり精密な議論をしないと誤解や混乱が生じます[脚注：例えば、関数と関数コードが1:1に対応するなら、2つの関数の外延的同値性が実効的に判定可能なように思えます。が、それは誤解です。]。できればこの点を別に説明したいのですが、今日はしません。

これを精密に議論すると、、、、2時間、いや3時間くらいかかるのかなー？

集合圏では、N^Nは、ある意味「簡単だ」ともいえる。しかし、計算可能関数の圏を極めて具体的に、デカルト閉圏として構成すると、N^Nの意味は集合圏とはドエラク違うことが分かる。

計算可能関数の圏にもいろいろなバリエーションがあるが、意味論だけではなくて、最小限の構文論（多ソート代数風）も入れた方がいい。そのほうが事情がハッキリするだろう。

こういうことは、具体的かつ徹底的にやらないとわかんないのだよね。