「集合とはなにか」を読んでます。
面白いです。良くわからないので何回も見直してます。
ついでにと思って、「層と圏とトポス」も買ってみました。
集合がある性質を表す物の集まりなんだけど、それを色々拡張して行くと、この方が便利だ、あの方が便利だって話になって行って、圏論が産まれてHaskellはその圏論を元にした言語だってことなんだろうなぁと。圏論はそういう事で素晴らしい者なんだろうなぁとは思うのですが、コンパイラを作る上で無くてはならないものではないので、とりあえずおいておこうと思います。ここで圏論に行くと、HaskellかScalazかっていう話に進むんでしょうけど。
例によって分かる範囲で、まじめに読んで、途中から眠くなって来たので斜め読みで最後まで見ただけなので、詳しい理解は出来てないのですが、記号は覚えても忘れそうだけど、スラスラ読めてよかったです。
群が抜けてますけど、どうなってるか良くわからないのでいいやと。
量子集合論みたいなのも展開出来るはず見たいな話が書いてあって、今どうなってるとか全然知りませんが、線形代数を基礎にしている量子力学とはまた違った、非連続的な量子力学の理解とかに繋がるのかなぁとか名前だけ見て思ったのでした。
ということで、ググってみると、おお、量子集合論の論文とかがあって、面白いですね。量子力学の実験結果を元に、事実である命題として集合論を作る際に使っているのかな？
量子化とかは、こうして見ているパソコンのグラフィックスも、デジタルな音声も全て量子化された情報なのですぐにどうこうってわけではないかもしれませんけど、いろいろと役に立ちそうです。
多分、夢の除染装置であるコスモクリーナーを実際に作る場合もも量子化された原子のサイズが重要な鍵となってるんじゃないのかなっと。
あと、物語としても面白くてよかったです。
で、こちらの方面も色々見て見ててまとめられると面白いだろうなぁと思ったんですけど、やっぱり、コンパイラ造りに直接必要ないので、そこそこにしておきます。やる気がなくなったらみてみよう。
一階記述論理をゲーデルって人が考えて、その友達がこの本の作者ってことなのかな？
凄い人だし、何を考えて集合論が出来て来たのかがずいぶんわかりました。
でも、Coqをやってから見てるので、集合と命題については分かるけど、動的言語で書かれているので分かり辛いんだなと思いました。SetとPropがあるけどTypeがないから分かり辛いんで。
集合と命題に型を加えた理論が欲しいってなると型理論になるわけです。型理論はどうも、ラッセルのパラドックスにより素朴集合論の問題が明らかにされたことを受けて、型理論を構築したそうです。でも、不確定性定理は存在しうるのでどうこうって話になってるらしいと。
そして、型システムは型理論を形式的な言語の基盤にしてるらしいと。
Coqを理解していけば型理論について理解が進む事になるし、型理論があると集合論も分かりやすくなる部分もあるけど、全てを表す事が出来る訳ではないのかな。
動的なCoqみたいなので、集合を記述出来たら良いんでないかなぁと思います。そういうのが出来るかどうかもわからないですけど。型はあるけど、明示されないって感じになるのかな？
要するに、型のない世界で普通に集合論があって、そこで型を追加して言語を作るのが型理論の話で、型理論を使って証明出来る事を使って作った言語がCoqなので、型理論の後の話がCoqなんだけど、型がある方が分かりやすいって事もあるよと。
RubyとJavaでJavaのほうが分かりやすい事もあると。
そんな話でした。
あと、不確定性定理をゲーデルさんが考えたそうなんですが、不確定性原理と観測問題（かんそくもんだい）とかと似通ってるのかなぁ。名前も似てるし。原理と定理は別に２つあるんですね。とか、観測する事で位置が決まる。観測しない間は、確率でしかない。とかいうのは、遅延評価だよなぁとか。
数学者が結構精神的に弱る人が多いみたいなんだけど、それもまた、脳内のシナプスの使い方が、論理的な事を考えるように最適化されて行った結果なんじゃないかなぁとか、思ったりしました。
高速に演算する為に、３つも４つもの同じような回路を使っていた物を、１つで、すぐに結果が出るようにして行くと、日常生活が困難になる方向に進んで行ってしまうとかあるんじゃないのかなと。
論理的に正確さを求めて行くと、不正確であるものの存在を認めざるを得なくなるのだと気がついて、そういう目で周りをみると、１００％なんてあり得ないのに、100%の自信を持って話す人がいて、それが信用ならないってことになり、人間不信になって行く。
そういう話なのかなと思ったりしました。
あと、強いエネルギーを持っている物の存在確率の半径みたいなのは広いとかなんとからしいんですけど、そいつを観測するとなると、行動範囲を狭められるので、嬉しくない。
確率的に、その狭い範囲にいる確率は減るので、スケジュールにあわせるのが辛くなるとかで、遅刻とかしやすくなってしまう。でも、それが駄目だっていう世間の目と、そんな事いわれても時間にあわせるのが大変なんだっていうのとのギャップもまた、苦しむ原因の１つなんじゃないかと。
体調が良くないと動けない人に、スケジュールぴったりに動けというのは酷だって思うのでした。それが出来る人はいいけど、出来ない人に取ってそいつは辛い話なのですよ。
大物ぶってるわけでもなく、動けない人は色々理由があってうごけないんだよなぁ。スケジュールがぴったり守れることは良いことですけど、それだけを物差しとして、友達を選ぶような人達とは残念ながら友達になれそうにないって思ったりするのかなと。
権威に興味があるのであって、俺個人に興味がある訳ではないだろうとか。ってほとんど愚痴になってしまってますけど。
