A coalgebraic higher-order modal fixed-point logic

あなたは、コンピュータに未来について考える方法を教えようとしていると想像してみてください。あなたは、交通信号ネットワーク、ビデオゲームの世界、あるいはロボットの意思決定プロセスのような複雑なシステムを見て、「このロボットはいつか動けなくなるか？」「ロボットが確実に勝利するパスは存在するのか？」といった問いに答えさせたいと考えています。何十年もの間、コンピュータ科学者たちは、こうした問いを投げかけるために「様相論理（modal logic）」と呼ばれる特別な数学的言語を使用してきました。この言語を「魔法の呪文」のセットだと考えてみてください。ある呪文は「今、何が真であるか」をチェックし、別の呪文は「いつか何かが起こるか」をチェックします。

しかし、現実の世界は混沌としています。システムは単に「オン」か「オフ」であるだけではありません。例えば「70%の確率で左へ行き、30%の確率で右に行く」といったこともあります。また、どのように見るかによってルールの変わるシステムもあります。あるいは、システムがあまりに複雑で、関数が他の関数に作用する（例：材料リスト自体を書き換えるレシピのようなもの）場合もあります。これに対処するために、科学者たちは2つの強力なツールを開発しました。一つは確率を持つシステム（コイン投げのようなもの）のためのツールであり、もう一つは高階の複雑さ（ルールがルールを変えるようなもの）を持つシステムのためのツールです。ここで大きな疑問が生じます。「これら両方の世界を同時に理解できる、単一の普遍的な『マスター言語』を構築できるだろうか？」というのが、コンピュータ科学者のライアン・テイ、ハルシュ・ベオハル、チャールズ・グレロイスが解決しようとしたパズルです。

コンピュータの世界のためのユニバーサル翻訳機

この論文において、著者らは「余代数的高階様相不動点論理（Coalgebraic Higher-Order Modal Fixed-Point Logic）」、略して「Coalgebraic HFL」という、新しい超強力な言語を紹介しています。これが何であるかを理解するために、「余代数（coalgebra）」を恐ろしい数学用語としてではなく、あらゆる種類の動的なシステムの「普遍的な設計図」だと想像してみてください。単純な交通信号であれ、複雑なロボットであれ、あるいは確率的なゲームであれ、余代数とはシステムが現在の状態から次の状態へとどのように遷移するかを記述する方法に過ぎません。

著者らは、すでに複雑で高レベルなルールを扱うことに長けていた既存の論理言語（HFL）を取り出し、そこに「述語リフティング（predicate liftings）」と呼ばれる「メガネ」を与えました。このメガネをアダプターだと考えてください。以前は、この論理は特定のタイプのシステムしか見ることができませんでした。しかし、このアダプターがあれば、論理は、単純な「はい／いいえ」の選択、複雑な確率の雲、あるいは高階関数を含むものなど、余代数の設計図に適合する「あらゆる」システムを見ることができるようになりました。これは、同じボタンを使ってテレビ、ドローン、スマート冷蔵庫のすべてを操作できるユニバーサルリモコンを手に入れたようなものです。

大きな発見：すべてを統べる一つの論理

この論文の主要な発見は、この新しい「Coalgebraic HFL」が、その二つの有名な先祖の仕事を同時にこなすほど強力であるということです。これは、標準的なコンピュータプログラム（多くの場合、単なる「はい／いいえ」の決定）の論理と、確率的なシステム（物事が一定の確率で起こるもの）の論理の両方を記述できます。

これを証明するために、著者らは単に「機能する」と言っただけではありません。古い世界の非常に困難な2つの問題が、この新しい言語に完璧に翻訳できることを示しました。

1. 「空集合」問題： 非決定的なマシン（一度に多くの経路を選択できるロボット）を想像してください。ロボットが成功する経路が「存在する」のか、それとも何としても失敗するのかを知りたいとします。著者らは、この問いを投げかけることは、彼らの新しい論理における特定の質問をすることと全く同じであることを示しました。
2. 「値1」問題： 確率に基づいて意思決定を行うロボット（サイコロの目のように）を想像してください。ロボットが成功する確率が正確に100%（または「1」）となる戦略が存在するかを知りたいとします。著者らは、このトリッキーな確率の問題も、彼らの新しい論理におけるモデル検査問題に帰着できることを証明しました。

簡単に言えば、彼らは「橋」を架けたのです。もし新しい論理で問題を解くことができれば、それは事実上、古い世界におけるこれらの難しい問題を解いたことになります。これは、二つの異なるコンピュータシステムの考え方を一つの屋根の下に統合したということであり、非常に重要なことです。

彼らがどのように行ったか：「サポート」のトリック

これを実現するために、著者らはルールの定義に細心の注意を払いました。彼らは「サポート（support）」という概念を導入しました。これは、システムの「指紋」のようなものです。彼らは、もしシステムがある特定の数学的ルール（具体的には、「包含関係（inclusions）」と「弱い広幅プルバック（weak wide pullbacks）」を保持する、つまりズームイン・アウトしてもシステムが一貫して動作するという高度な方法）に従っているならば、あらゆるマシンの「トップ値（top value）」を定義できることを示しました。

そして、彼らは「探偵」として機能する特定の公式（この論理における特定の呪文）を構築しました。この探偵の公式は、マシンを観察してその「トップ値」を計算します。マシンが単純な「はい／いいえ」のロボットであれば、公式はそれが「はい」と言えるかどうかをチェックします。マシンが確率ロボットであれば、公式はそれが100%の成功率に到達できるかどうかをチェックします。論文では、その公式が出す答えが、あらゆるシナリオを通じてロボットを実行して得られる答えと全く同一であることを数学的に証明しています。

それができないこと（現時点では）

この論文が主張して「いない」ことも明記しておく必要があります。著者らは、彼らの論理が確率的システムの性質を捉えてはいるものの、存在する最も高度な確率論的論理（PHFL）の「あらゆる」細部を捉えているわけではないことを明確にしています。具体的には、「上方閉包部分集合（upwards-closed subsets）」（値が共に上昇していくグループ、という技術的な言い方）を含む非常に複雑な公式については、現在のバージョンでは完璧には扱えません。彼らはこれを限界として認め、将来の研究課題として挙げています。

さらに、彼らはこの論理をコンピュータ上で実際に実行することが「どの程度難しいか」については示していません。実際、彼らは、特に確率を含むシステムの場合、公式が真であるかどうかをチェックする問題は「決定不能（undecidable）」であることが知られていると指摘しています。これは、ある種の複雑なシステムにおいては、有限の時間内に答えを保証できるコンピュータプログラムは存在しないことを意味します。著者らはこれを解決したとは主張しておらず、単に、たとえ問題自体が一般的なケースにおいて解決不可能であったとしても、彼らの新しい論理がその問題を記述するための「正しい言語」であることを示したのです。

なぜこれが重要なのか

なぜ、ロボットの経路をチェックする論理に、好奇心旺盛なティーンエイジャーが関心を持つ必要があるのでしょうか？ それは、私たちの世界が自動化されるにつれ、かつてないほど複雑で不確実なシステムを構築しているからです。私たちは、雨や霧に対処する自動運転車（確率）や、何層ものルールに基づいて意思決定を行うAI（高階関数）を手にしています。

この論文は、これらすべてのシステムについて語るための、単一の統一された方法の理論的基礎を提供しています。新しいロボットやゲームごとに新しい言語を発明する代わりに、私たちは最終的に、この「Coalgebraic HFL」を使用して、デジタル世界が安全で、公平で、意図通りに動作することを検証できるようになるかもしれません。これは、テクノロジーがいかに複雑になろうとも、私たちの技術がクラッシュせず、不正をせず、私たちが求める通りに正確に動作することを、数学的に証明できる世界への一歩なのです。