※ 子供の話ばかりじゃアレ(?)だから、「カリー/ハワード(Curry-Howard)対応をうんと一般化するとどうなるか」みたいなネタで。
以前紹介したことがあるバエズ&ステイのロゼッタストーン論文がarXivに入っていました。
- 題名: Physics, Topology, Logic and Computation: A Rosetta Stone
- 著者: John C. Baez, Mike Stay
- URL: http://arxiv.org/abs/0903.0340
- ページ数: 73
この論文の最後のほうにある「The Rosetta Stone テーブル」のlarger versionは次のようなものです。
画像だとコピーに不便ですからテキストにしたもの:
Category Theory | Physics | Topology | Logic | Computation |
---|---|---|---|---|
object | Hilbert space | manifold | proposition | data type |
morphism | operator | cobordism | proof | program |
tensor product of objects | Hilbert space of joint system | disjoint union of manifolds | conjunction of propositions | product of data types |
tensor product of morphisms | parallel processes | disjoint union of cobordisms | proofs carried out in parallel | programs executing in parallel |
internal hom | Hilbert space of 'anti-X and Y' | disjoint union of orientation-reversed | conditional proposition | function type |
日本語にしておくと:
圏論 | 物理 | トポロジー | 論理 | 計算 |
---|---|---|---|---|
対象 | ヒルベルト空間 | 多様体 | 命題 | データ型 |
射 | 作用素 | コボルディズム | 証明 | プログラム |
対象のテンソル積 | 複合系のヒルベルト空間 | 多様体の直和 | 命題の連言 | データ型の直積 |
射のテンソル積 | 並行した物理過程 | コボルディズムの直和 | 並列に遂行される証明 | 並列実行されるプログラム |
内部ホム | 「反XとY」のヒルベルト空間 | 向きを逆にしたモノとの直和 | 条件付き命題 | 関数型 |
1月まで圏論勉強会のテキストに使っていた"Temperley-Lieb Algebra: From Knot Theory to Logic and Computation via Quantum Mechanics" (PDF, 44pages) も複数の分野を横断する共通性を話題にしたものでした。統計力学のテンパリー/リーブ代数と結び目理論のジョーンズ多項式、線形論理のカット消去、平面内でお絵描きする平面ラムダ計算(planar lambda calculus)などの不思議な対応を述べています。
Esfandiar Haghverdiのプレゼン(現状、インターネットで見つからないみたいです)によると、線形論理の創始者ジラール(J.-Y. Girard)は次のような対応を考えているようです。
ジラールの用語 | 手続き的解釈 | 関数的解釈 | 論理的解釈 | |
---|---|---|---|---|
アルゴリズム(algorithm) | プログラム | 式 | 証明 | |
計算(computation) | 実行 | 評価/簡約 | cut消去 | |
データ(datum) | 結果 | 値 | cutなし証明 |
ジラールとその周辺では、並列処理のアルゴリズムとかデッドロックの問題をマジで扱っているんですが、その道具がヒルベルト空間だったりC*環だったり、、、ウーム、わからんわ。だけど、物理と計算は本質的につながっているらしいという印象は抱きます。