論理、圏、空間、その他いろいろ
本編コメントに答えるついでに、参照リンクやら戯言やらゴチャゴチャと。
プログラムの集まりが「圏」になるというのは、どなたの発見か知りませんが、計算機科学において金字塔のような成果なのではないでしょうか。
別に誰かの発見というわけではないような気がします。気が付いてみれば、みんなそんなふうに考えていた、というような状況かと。強いて人名を挙げれば、ゴグエン（Joseph Goguen→http://www.cs.ucsd.edu/users/goguen/）、モッギモッジ（Eugenio Moggi→http://www.disi.unige.it/person/MoggiE/）、アブラムスキー（Samson Abramsky→http://web.comlab.ox.ac.uk/oucl/people/samson.abramsky.html）あたりの貢献が大きいかな？ とはいえ、これも僕が知っている人々から選んだだけですが。
※ あっ、人名はカタカナ表記しようと努めてますが、発音は全然アテになりませんので。→この名前はなんて読むのだろう？ - 檜山正幸のキマイラ飼育記 (はてなBlog)
もし「宇宙」というものを巨大なある種の計算機とみなせるならば、
みなせるのか？ よくわかりませんね（強いてキーワードを挙げれば"reversible computation/computing"でしょうか）。
物理系の時間発展などの集まりにも、圏論的な意味付けができるのではないか、などと想像します。
ローベル（Lawvere→http://www.acsu.buffalo.edu/~wlawvere/）が、"Categorical Dynamics"（圏的力学）なんてことを言ってましたね、"Categories in Continuum Physics"（http://www.amazon.co.jp/gp/product/0387160965/）なんて本まで出してます、僕はよく知りませんが。
マーク・ホプキンス（Mark William Hopkins→Mark W. Hopkinsは今どこに？ - 檜山正幸のキマイラ飼育記 (はてなBlog)）は、場の量子論と形式言語理論が似てるなんて言ってまして、僕はけっこうホンキでマーク説を取り上げています。（→TQFTの定式化 - 檜山正幸のキマイラ飼育記 メモ編、誰が何言っているか、と、何がどこまで分かったか - 檜山正幸のキマイラ飼育記 メモ編）
ある程度抽象化すると、（位相的）場の量子論（TQFT)と形式言語理論が同じ定式化になるのは、間違いないようです。
それと、ジョン・バエズ（John C. Baez →http://math.ucr.edu/home/baez/）の周辺では、高次圏をバシバシ使って物理をやっているようですね。
はい、そうです。→コンパクト空間と論理／モデル論 - 檜山正幸のキマイラ飼育記 (はてなBlog)
１９３０年代すでにこのような研究がなされていたというのは驚くべきことだと思います。
確かにストーンの発想は凄いですね。でも、30年代は抽象代数やトポロジーが勃興してきた時期で、時代に勢いがあったのかも知れません（とか、歴史に無知な僕が言うことだから信用しないほうがいいけど）。
通常の代数幾何は「論理」の美しい一般化になっています。
同じことですが、論理が代数幾何の特殊事例というほうが適切な気がします。乗法的ベキ等体は{0, 1}の2元の可換環に限るのですが、一方、標数2の体も{0, 1}です。古典論理は標数2の体上の代数幾何という感じでしょう。標数0と正標数だと、違った代数幾何になりますが、正標数でも標数2は例外扱いのときが多いので、標数2だけはなんか特別な世界を形成している気がします。
フレームとロカールの対応についても初めて知りました。論理の研究になぜトポス理論が関係してくるのかが、これでなんとなく納得できたしだいです。
そういえば、フレーム／ロカールは、「Setの反対圏からのimplication」でチョット触れましたね。
位相のほうから言えば、古典論理に対応するブール空間てのはかなり特殊です、全不連結ですから。開集合と閉集合の区別があまりなくて、clopen setsがすごくたくさんある空間です。もっと一般の位相まで考えると、直観主義論理が出てきます。
つまり、「ブール空間→普通(?)の位相空間」が、「古典論理→直観主義論理」。束論的には「ブール束→ハイティング束」でしょうね。それで、束論の側で「ブール束→ハイティング束→もっと一般の束（フレーム）」と調子にのって一般化する、「ブール空間→普通(?)の位相空間→点概念がなくてもいい空間（ロカール）」となるのでしょう、たぶん。
一方で、直観主義論理の圏論的対応物がCCCやトポスになるので、空間、束、圏などは、同じものを別な定式化で見てるだけのようです、どうも。
また、「可換環」から「可換性」や「分配則」などの条件をはずせば、なにか新しい「論理」が得られるのでしょうか。
非可換に関しては、「論理とはなにか？」で紹介したLutz Strassburgerが、A Non-commutative Extension of Multiplicative Exponential Linear Logicなんてのを書いてますし、他にもnoncommutative linear logicネタはあるようです。クオンテール／クオンタロイド（quantale/quantaloid）も一般には非可換なモノです。
分配律を変形したものでは、linearly distributive（以前はweakly distributive） lawなんてのがあります。Cockett, Seelyの"Weakly Distributive Categories"（http://citeseer.ist.psu.edu/cockett91weakly.html）あたりからでしょうか。線形分配律は、a×(b + c) = a×b + c という形です。
もっとも、名前が分配でも、これは分配律とは別物だからdissociative law（解離法則）と呼ぼう、とかいうハナシもあるようですが。
