環、有界、STモナド

全部話題バラバラです。

1.なぜ物理量は環なのか？

　今ゼミでIsham某量子論本を読んでいたりするのですが、これに限らず、ある文脈において、次のような対比が語られる事があります。すなわち、

古典力学では物理量のなす環構造が可換であったが、量子論では一般に非可換になる。

　この可換非可換という対比は、単にある種の代数構造の条件開放という意味で「少なくとも数学的には」自然な一般化の発想でそれで例えば可換/非可換C*環が、GN双対を通じて普通の幾何(コンパクトハウスドルフ位相空間)/非可換幾何の対比になるだとか、あるいは量子群だとかいう名称がここに由来するだとかいった話に繋がったり、物理では非可換性によって、物理量の同時測定、同時値付与ができない、不確定性関係につながるとか、そういった風潮や言い回しの背景を提供しているようにに思います。（そうでないならそれは良いことなのでどうでもいいです）

　しかし、ほんとかよ？　毎度のことですが、この手の言説の雑さ加減、ちょっと反省してくれというお気持ちが湧いてきます。　いや、数学的な構造それ自体に興味があるので、可換非可換を対比しますというのは別にいいんですよ。それは自由にやればいいし、やっていきをした結果として理論物理に有意な構造が手に入ればそれを使うのもいいですが。　問題は、物理学の基礎や定式化において「量子論は物理量環が非可換になったやつ」という言説が目に余るということです。

　まずそもそもですが、

定式化段階で「物理量が可換環である」とみなせる理論、そんなにあるか？

という点です。大体において、こういう状況での可換環というのは力学相空間 $X$ 上の $C(X)$ のことを指しているはずです。要するに、「力学的相空間/状態空間があって、物理量がその上の複素数値関数で、各点積による可換環構造をもつ」というビジョンは古典力学ではありがちだよね？ということを想定して、古典物理は可換C*環だ！といっているのです。

　はー、ちょっと待てよと。例えば学部でやるような以下の古典理論を見てみますよ？

解析力学(L)
- ラグランジアン： $TN$ 上 $\mathbb{R}$ 値関数、加法的、 $\mathbb{R}$ mod、しかし乗法的でない。
- Noetherモーメント：リー群が作用しているとき、リー代数からNoetherモーメントの対応は $TN$ 上 $\mathbb{R}$ 値関数へ線形、乗法的ではない。
解析力学(H)
- ハミルトニアンベクトル場： $\mathbb{R}$ mod、乗法をもたない。
- poisson環： $\mathbb{R}$ mod、乗法を持つが可換ではない。
古典場理論(電磁気,流体含む)
- 電磁気の各種量：基本変数がベクトル場や微分形式なのでいずれも $\mathbb{R}$ mod、乗法はない。外積はgradeを上げる上に可換ではない。
- 物理量として、密度関数の領域積分や、あるいはその密度関数自体を取るので、そもそも乗法は限られた状況でしか入らない。(例えばエネルギー密度の計算やポインティングベクトル場など)
熱力学
- 熱力学関数：状態空間上の実凸関数だが、同次性を持つことを強いられるので、乗法を無制限にとれない。系の拡大と加法が取れるので $\mathbb{R}$ mod。
相対論
- 古典場の理論に準じる。大体テンソル場およびその領域積分が基本的物理量なので、乗法は無制限にとれない。

　実数値関数ばっかやんけ！というツッコミをおいておいても、殆どが $\mathbb{R}$ modであって、 $\mathbb{R}$ algじゃないわけですよ。algebraっぽい奴だって各点積とは違うし。いや、それでも解析力学で、任意の物理量として $TN,TN^*$ 上関数環の、poissonではない各点積関数環を考えられるでしょ、と思うかもしれません。しかしそれにどんな物理的意味がありますか？poissonはハミルトニアンベクトル場の無限小リー微分としての意味がありますが、各点積はなんですか？ええ？なんもないでしょう？　第一ですよ、環構造を定義する方法なんて、今やいくらでもあるわけです。集合が手に入ったら適当が環を持ってきて関数環、形式的積を定義して自由生成、結合的演算があったらそれで環とか、数学的構造が手に入ったらまぁご自由に作ってくださいと。そんななかで大事なことは、（物理において）「その積が物理的動機にモチベートされている」かどうかであって、その意味でいえば相空間複素関数環の各点積構造、ほとんど動機がないわけですよ。解析力学で各点積関数環を作れるのは、単に「作れてしまう」から計算や試案に便利というだけであって、それ自体に統一された第一級の物理的な解釈があるわけではないのです。

　こうしてみると、ガッツリ環として最初から宣言しているのは、ハミルトン形式のPoisson環くらいで、これは最初から非可換なわけですから「量子論では物理量は非可換！」とか「？？？？」じゃないですか。大体角運動量の議論とかですら、リー代数->正準力学系->ユニタリ表現で、非可換な代数が準同型になることを使っているわけで、それをスルーして、「非可換性を強調するときだけ $C(X)$ 、実際の運用の時はpoissonにアナロジーを求める」なんてダブスタもいいとこです。いい加減にしろ。

　これ結構悪影響があって、というのも量子力学では物理量は作用素で表現しますが、まぁ案の定「作用素」ですから、環になりますよね？そして「量子物理量の環構造の物理的意味が不明」という問題が発生してしまうのです。

　しかしまってくれ、そもそも環構造に物理的意味が最初から憑依していたケースは、そもそも古典物理ですら限られているわけで、その古典物理の物理量環だって、「相空間があって、値が実数値だから定義できる」という意味しかない。だからこの意味不明問題は、そもそも定式化がナンセンスであって、積構造に何を期待するかというのは、ヒルベルト空間の作用素という数学的モデルの実装戦略を採用した我々が最初に動機づけすべきことなのです。で、それがない？　何も宣言してないんだから無くて当然でしょう。そしてそれで何も困ることはない。

　もう一つの悪影響は、「物理量が実数値である」という思い込みを強めてしまう点です。

　というのも、例えば量子測定では、測定値集合は別に実数に限られてなんかいないし、任意の可測または位相空間が認められます。これはごく当然のことで、例えば物理量の測定をするときに、僕らは測定器のUIの状態を見るわけじゃないですか。それは実数ですか？　なわけ無いですよね？　アナログメーターの針や、デジタル表示器のレジスタ状態をモデル化した某かを僕らは認識しているわけで、そこまで含めたら測定値集合が実数でなくてはならないなんてことには全くならない。このメーター系のモデルは、とりあえず確率論の文脈に置くので、可測空間でありさえすればよいのです。ではどうして古典力学含む物理理論で、大量の実数由来の数学的構造が使われているのか、というのは単にそれぞれの状況で実数が便利な構造であった、というだけに過ぎません。なぜなら、個々の理論では実数を使う「動機」がそれぞれ微妙に異なるからです。

解析力学(L)
- ラグランジアンの最適化問題として書く： $\mathbb{R}$ の位相、順序構造。
- 相空間が多様体: $\mathbb{R}$ の位相構造。
解析力学(H)
- 相空間の変換群生成ベクトル場：座標微分なので成分が $\mathbb{R}$ 値になる。
古典場理論
- 同様に多様体上のベクトル場の双対として微分形式があるので、成分が $\mathbb{R}$ になる。
相対論
- 同様。
熱力学
- 操作可能性順序に関してエントロピーによる表現定理がある。つまり $\mathbb{R}$ の順序ベクトル空間構造。

　量子力学の測定概念が一気に位相空間や可測空間に一般化できた理由は、それだけ量子力学が古典力学と違って、内部に複雑な構造を備えていない、非常に素朴な理論であることによります。古典理論のように、個々の系に複雑な構造が入ってしまえば、その系に対する操作はその構造を保つようなインセンティブが働きます。ところが量子力学は一般論としてはヒルベルト空間を使う以上のことは言っていませんから、その写像もかなり自由に選べます。量子力学の古典的対応物は、 $\bf{Top},\bf{Meas}$ とかの類であって、間違っても $\bf{Symp}$ とかではないのです。その意味では、量子力学の公理で「物理量を作用素で表す」も本当はおかしいんですよ。最初からPOVMで宣言するのが筋ってもんです。

2.非有界 作用素はいつ必要になるのか？

　半分位続きですが、量子力学の数学的にまっとうな処理というのをやろうとすると、関数解析になるのですが、そこで面倒くさいのが、非有界作用素の扱いです。というのも、正準量子化とかいうクソ論法に量子力学の当初の仕事が頼ってしまったため、数学的定式化の後で、この位置と運動量に相当する掛け算作用素と微分作用素をまともに扱うハメになってしまったのです。

　非有界作用素の面倒臭さは何かというと、基本的に定義域が全域ではありません。それでも稠密に定義されるものを扱うので、「ほぼ全域定義」ではありますが、この「定義域」情報を持ち回す必要性によって、折角作用素「環」構造を作ってあげたのに、例えば加法や結合が、定義域に対してどういう影響を与えるかがまったく非自明で、個々の要素にいちいち付き合ってやらないといけなくなります。

　ところでですが、量子力学の測定理論概念でのCPTPとかPOVMとかの話は基本的に可分であれば有界作用素の議論で完結します。これはCPTP概念がもともと作用素環(したがって有界作用素環)に由来したり、測定理論としてのメソッドを確率分布の獲得としてきちんと定めたために、スペクトルが確率値で有界にバウンドされるおかげです。となると、（有限自由度）量子力学それ自体の定式化では、非有界作用素の登場する所はないのです。

　それで気になるのは、僕らは「いつ非有界作用素との付き合いを余儀なくされるのか」ということです。ごく原始的な測定にはいりません。位置と運動量については、正準量子化を採用しなければよいのです。たとえば最初から $L^2(\mathbb{R})$ 上の左正則表現をとれば、Stone定理でユニタリ表現を分解できるので、実質運動量に相当するPVMとそのユニタリ作用の概念をもったまま、難なく議論ができます。PVMですから当然有界です。ユニタリ表現をちゃんと自覚的に召喚すれば、ユニタリなのですから非有界性はどこにも出てきません。つまり「物理量を作用素で表す」という呪縛を解除すれば良いという話です。そのスペクトルに「物理量の値」としての意味しかないのならば、それをわざわざPVM要素にかけて積分してヒルベルト空間にねじ込む理由がありません。最初からPVMで扱えば有界になるし便利。もし、そのスペクトルに変換群が作用しているとしても、PVMの底集合に群が作用していて、それが密度行列に対するユニタリ表現との間に繋絡自然性条件が走っているとみなせば良いのですから、群作用も問題ない。

　有限自由度の個々の系に関して言う分には、非有界作用素を別の数学で殴る代用手続きがあるように見えます。

　そこで、複数の系の相互作用なんかを考えてみます。たとえば測定のモデルとしてvNプロトコルというのがあり、それは次の形をしています。

$\exp(itA\otimes P)$

　ここで $A$ は測りたい物理量で $P$ はメーター系の変換生成子です。しかし、これも取扱自体は有界作用素の範疇で実行できます。というのも $A$ をスペクトル分解して、これによる合成系のPVM上で $P$ によるユニタリ変換を直積分すれば良いからです。ユニタリ変換のPVM積分ですから、有界の範疇です。しかしここにはより興味深いことが起きていて、ここでは $A$ のスペクトルの「値自体」がメーターをどの程度動かすかを決めているのです。なので $A$ のスペクトルは「ただの測定値」ではありません。メーター系の変換群としての意味があることになって、それではこのプロトコルを一般化するとしたらどうなるのか？それを組織化するならどうすればいいか？という疑問が湧きます。

　思いかえせば、古典物理でも「物理量の（各点）積」ってこういう使い方をしていたよな、という気がしますね。例えば解析力学や古典場などで各点積相互作用項を突っ込むことで両者が両者に従って変換されるのが良い例です。つまり、いい感じの相互作用やある種の動作を引き起こすために、「積をとってみている」わけです。より素朴な古典物理の場合は、この相互作用それ自体を物理的イメージに基づいて行っている場合があったわけですが、（例えば常/偏微分方程式を「発見する」場合のdxなどを用いた投機的計算など：弾性体や曲線の方程式とか）いつしかそうした文脈が忘れ去られて、単なる「積構造」だけが引き継がれるようになったのかもしれません。量子力学でそうした正当な直観を回復する方法論があるのかについてはまだ謎です。

　脱線しました。非有界作用素に戻ってきますが、唯一これやばいなと思うのがあり、それはフォック空間を作る時のLadderoperatorです。

　自由場の量子化、というか量子化はクソなので、単に多粒子系ですが、相互作用をさしあたって深刻に考えなくていい場合は、とりあえずフォック空間を張る事ができます。これは一種の自由テンソル代数のようなものですが、量子論でのフォックは対称化や反対称化を行ったり、内積も適切に決めてやる必要があるので、単なるテンソル代数とは微妙に異なります。

　どういう普遍性で定義するのがベストか不明ですが、とりあえずgraded monoidかな？位に思っています。しかしここに問題点があり、粒子を合流させる積演算、およびそこから造られるLadderoperatorは非有界なのです。統計性処理のために。これは量子的調和振動子の計算ともあいます。

　ｳｵｰここへ来て非有界になってしまった。しかしこれはある意味では自然という見解があります。というのも、例えば素粒子現象のように初っ端から多粒子で、かつ識別不能な場合、可観測量とはなにかというと、一粒子の場合はPOVM要素で成立確率を返す汎関数ですが、このPOVM要素をLadderoperatorでフォック空間に輸送すると、「POVM要素を満たす粒子数期待値」を返す汎関数になるんですよ。でもこれは確かに自然な物理量に思えます。だって識別不能なんですから、どれがどの事象を成立させるかわからないわけで。

　すると、こうした状況では、単純な確率論としてのメソッドに基づく定式化がまずい気がしてきます。確率論は汎関数の評価値として $[0,1$ ]値だけを相手にすればいいので、有界になりますが、粒子数期待値となれば $[0,\infty)$ ですから、どんなつまらない物理量でも対応作用素が非有界になってしまいます。どうすれば…

3.STモナド

　Haskellは、他の言語では副作用とかよんでる振る舞いをきちんと型レベルで捕捉することに成功していますが、そのためにモナドを振り回す必要があります。まぁそれはよいのですが、例えばIOモナドはほぼなんでもできますが、純粋な計算をしたいというのに、ちょっとIOの力を借りただけで、 IOに汚染されたままになってしまってはたまりません。

　良くも悪くも、型の表現力と統制力が強力なので、やりたいことに対して丁度よい型による表現を探す事が求められているのだと思います。　そこで破壊的代入や参照や配列更新等ができつつも、最終的に値を純粋に取り出してモナド文脈から戻ってくることの出来るモナドとして STモナドがあります。しかしこのSTモナドの実行関数runSTの型がくせ者で、一見型を見ただけでは、これが何を意味するのか、これによってどんな利用制限がかかってくるのか、それは何故なのかがピンときません。

runST::forall a.(forall s. (ST s a))-> a

この全称量化こそがSTモナドのキモだったのですが、ようやくそれを了解したのでこれを書いています。

　ところでですが、述語論理において次の証明規則があります。

$\forall x. \phi \Rightarrow \phi(t/x)$

　これは全称量化の除去規則というやつで、全称量化束縛された変数の具体化に相当します。このとき $t$ は「実質的には」なんでもよいのですが、あくまで推論規則としてこれを見るにはちゃんと制限があります。それは $t$ は $\phi$ に代入されたときに、 $t$ 中の自由変数が捕獲されてはいけないということです。「実質的には」なんでもよい、といったのは、論理命題としてなら、 $\phi$ 中の束縛変数をアルファ変換などで置き換えても同値になるためです。しかし推論規則としてはこの制限は無視できません。今それぞれの論理式はただの記号列だからです。例として

$\phi(-)= \forall y.\exists z. (-) + z > 100 + y$

などを考えて、 $t=-z$ などとすれば破綻をきたす事がわかります。

　話を戻しますが、型システムと論理がいい感じに対応してそうというお話があります。

カリー＝ハワード同型対応 - Wikipedia

　詳しくは理解していませんが、型システムがどういう振る舞いをするかのアナロジーを論理に求めることはできそうです。そこでrunSTですが、何らかの具体的な値を吐かせるために使うわけですから、型変数のaはいずれ具体化されるはずです。このとき、先の述語論理のアナロジーで考えれば、aの具体化においてsを含むと、これが捕獲される事がわかります。したがって、runSTを含んで型検査をするときに、aにsを含む具体化を要求するようなコードは弾かれることになります。

　例えば不正なコードとして、

Haskell/存在量化された型 - Wikibooks

の例を見てみましょう。

v = runST (newSTRef True)

が不正ですが、これはnewSTRefの型が

newSTRef::a' -> ST s (STRef s a')

であることによります。このvの型を導出しようとすると何が起きるか見てみましょう。 ST s (STRef s a')をrunSTに代入するのですから、最終的に具体的なaを導出するには ST s (STRef s a')からrunSTの具体化の前提：forall s.(ST s a)を導く必要があります。このときaは全称量化されていたのですから、sを含んではいけません。ここで、forall導入を行ってforall s.ST s (STRef s a')としてもa=(STRef s a')となり、 sに依存したaしか示すことができません。そこでこの型チェックは失敗します。

　証明論的なこの不正の理由は納得できましたが、そもそもこのコードはなぜ弾かれるべきなのでしょうか？

　ここで、あえて型ST s aを「環境sと相互作用する返り値型aの計算」だと解釈してみましょう。 newSTRefの型a' -> ST s (STRef s a')は、参照型について「その参照が意味を持つ環境」sがSTRef s a'として型に組み込まれている事がわかります。すると、先のコードについては、「環境s上でしか意味を持たない参照」をs以外に持ち出すことが不正であると考えられます。

newSTRefがa->ST s (STRef s a)の返り値は、型変数sが二度出現し、それは同一です。これは

環境s上のアクションであること
得られる参照値は環境sにおいて有効なこと
この２つの環境は同一なこと

を示していると考えられます。　このほかのST文脈を利用する関数も、「ST sの外に出すべきでない」場合はその返り値がsに依存するようになっています。逆に言えばs依存していなければ、外に持ち出す事ができる事になります。

　たとえばSTArrayならfreezeすることによって、immutableArrayになり、これはST sのような文脈を持たないので、そのまま外に出すことができます。ただし、STArrayをfreezeする動作は配列のコピーを含むので効率の観点からコピーを省略してそのまま凍結する為の専用関数runSTArrayがあります。この型は

runSTArray::forall s.ST s (STArray s i e) -> Array i e

であり、runSTと比べると、あえてSTArray sと、ST sのsが揃えてあります。すなわち、この配列自体が存在する環境と、それを操作する環境が揃っており、かつ配列の中身には環境sに依存がないことを量化子で強いているのです。

　たとえばこの配列に環境sに依存したインデックスiや要素eが使われていれば弾かれますが、この配列自体がsに存在することはちょうどぴったり許されるのです。こうすることで、環境情報について整合的な、環境情報に依存しない要素からなる、環境情報をもつ配列を、環境情報を持たない純粋な配列として取り出すことが、ぴったり実現できます。

実際にはこのsというのは、実体がありません。実際STのドキュメントを見ると、

Control.Monad.ST

The strict state-transformer monad. A computation of type ST s a transforms an internal state indexed by s, and returns a value of type a. The s parameter is either an uninstantiated type variable (inside invocations of runST), or RealWorld (inside invocations of stToIO).

とあり、RealWorldへ具体化して実質的にIOとなるか、具体化されないままrunSTされるかしかありません。しかし実体の無いまま全称量化される仮想的な型変数をSTに組み込むことで、「計算環境」のような文脈と、それに伴う制御を与えていることになります。