Quantum Weakest Preconditions Revisited: Pre-expectations for Expected Runtime Analysis

量子コンピュータのプログラムが停止するまでにどれくらいの時間がかかるかを予測しようとしている場面を想像してみてください。昔々、科学者たちには「最弱前件条件（weakest preconditions）」と呼ばれるルールブックがありました。それは、まるで魔法の水晶玉のようなもので、「もし、この特定のセットアップから開始すれば、プログラムはあの特定の結末を迎える」と教えてくれます。しかし、そこには落とし穴がありました。その水晶玉は、答えが小さく扱いやすい数字である場合にしか機能しなかったのです。もしプログラムが10億年かかるかもしれない、あるいは永遠に続くかもしれない場合、水晶玉は壊れてしまい、「できません」と言ってしまうのでした。

Christina Gehnen、Dominique Unruh、そして Joost-Pieter Katoen によるこの論文は、まったく新しい、超強力な水晶玉を紹介しています。彼らはそれを 「プレ・エクスペクテーション（Pre-expectations：事前期待値）」 と呼んでいます。

問題点：「無限」の罠

著者たちは、量子界における奇妙な不具合を指摘しています。古典的な世界（普通のコンピュータなど）では、もしプログラムが最終的に停止することが保証されていれば、通常、停止にかかる時間は有限です。しかし、量子の世界では物事はより不気味になります。プログラムが**「ほとんど確実に停止する（almost surely terminating）」、つまり100万回実行しても毎回必ず停止するとしても、その停止するまでの「平均時間」が実際には「無限大」**になるということが起こり得るのです。

これは、コイン投げのゲームのようなものです。表が出たら終了です。裏が出たら、もう一度投げます。ほとんどの場合、すぐに終了します。しかし、あまりにも長い間、裏が出続けることがあり、その結果、停止するまでの平均時間が無限になってしまうことがあります。量子のバージョンでは、プログラムが確実に終了する場合であっても、このようなことが起こり得ます。古いツールは、この「無限の平均」を扱うことができませんでした。なぜなら、それらは有限の数字のために作られていたからです。また、永遠に止まらずに走り続ける可能性のあるプログラムも扱うことができませんでした。

解決策：新しい数え方

著者たちは、数字が巨大であろうと無限であろうと気にしない、新しいフレームワークを構築しました。彼らはこれを行うために、**「報酬（rewards）」**という概念を導入しました。

量子コンピュータがステップを進めるたびに、金貨を1枚もらえると考えてみてください。

• 古い方法： プログラムが終了した後に、金貨を数えなければなりませんでした。もしプログラムが終了しなければ、数えるべき金貨が存在しません。
• 新しい方法： 著者たちは、「すべてのステップの前に金貨を1枚ずつ足していこう」と言います。こうすることで、たとえプログラムが永遠に続いたとしても、計算を行うことができます。「どれくらいの金貨を集めることが期待できるか？」と問うことができるのです。もし答えが無限であれば、私たちの新しい数学はそれを処理できます。もし答えが有限の数であれば、それもまた素晴らしいことです。

彼らはこれを 「最弱事前期待値（Weakest Pre-expectation）」 と呼んでいます。これは、プログラムの終点から始点へと逆方向に遡り、正確な答えを事前に知ることなく、期待される「コスト（または実行時間）」を計算する方法です。

彼らが証明したこと（そしてしなかったこと）

著者たちは単に推測したのではなく、これが機能することを証明するために、厳密な数学的エンジンを構築しました。

• 彼らは、この新しい手法が**「無限次元の空間」（例えば、0か1かだけでなく、どんな数にもなり得る量子整数など）で動作することを証明しました**。
• 彼らは、プログラムが停止することが保証されていない（非停止の）場合でも、「コスト」を「報酬」として表現できる限り、期待される実行時間を計算できることを証明しました。
• 彼らは、停止するプログラムに対して、この新しい手法が古い手法と同じ正確な答えを与えることを証明しました。ただし、古い手法が失敗したケースも扱えるようになっています。

しかし、彼らは自分たちがやっていないことについても注意深く述べています。彼らは、これが量子コンピュータを速くするという意味ではありません。あらゆる量子問題を解決するという意味でもありません。彼らは、確率論（サイコロを振るようなルール）の規則を、そのまま量子力学に貼り付けることはできないことを明確に示しました。量子の世界では、プログラムが「ほとんど確実に停止する」としても、期待される実行時間が無限になることがあります。古いルールでは、「もし止まるなら、時間は有限である」とされていました。著者たちは、量子の世界ではそのルールは間違っていることを証明したのです。

「量子ウォーク」の例

彼らの新しいツールを披露するために、彼らは「量子ウォーク（Quantum Walk）」を分析しました。ウォーカー（歩行者）が直線の上を歩いている様子を想像してください。

• 通常のウォークでは、ウォーカーはランダムに左または右へ動きます。
• 彼らの量子バージョンでは、ウォーカーは「コイン（量子ビット）」によって制御され、左へ動くか、その場に留まります。

彼らは非常に興味深い発見をしました：

1. ウォーカーが負の数からスタートする場合、それは決して止まりません（永遠に左へ歩き続けます）。
2. ウォーカーが正の数からスタートする場合、それは必ず止まります。
3. しかし、ここが肝心な点ですが、ウォーカーが「重ね合わせ（superposition）」（多くの位置が混ざり合った状態）でスタートする場合、プログラムは確率1で停止しますが、停止するまでの期待時間は無限になります。

彼らの新しい「事前期待値」の数学を用いることで、異なる初期位置からどれくらいの時間がかかるかを正確に計算することができました。彼らは、平均時間が無限になる特定の初期状態さえも見つけ出し、「止まるなら、それは速い」と単純に仮定することはできないことを証明したのです。

まとめ

著者たちは、答えが「無限」である場合や、プログラムが永遠に走り続ける可能性がある場合でも、量子プログラムの実行時間を分析することを可能にする、新しい数学的規則を作り上げました。彼らは、答えが小さく限定された数でなければならないという古い要件を取り払いました。

彼らはこれが機能する可能性を示唆しただけではありません。彼らは、この新しい言語の構文（syntax）（文法）、意味論（semantics）（意味）、そしてその論理が成立するという証明を提供しました。彼らは、「報酬（ステップをコインとして数えること）」を用いることで、ようやく複雑で無限の量子プログラムの実行時間を、行き詰まることなく考察できるようになったことを示しました。これは、以前のツールでは決してできなかった、量子の「無限」の側面を鮮明に見通すための新しいレンズなのです。