Embedding Modal Logics into Logics of Bunched Implications

あなたは、ミステリーを解決しようとしている探偵だと想像してください。しかし、あなたには思考の仕方に関する2つの異なるルールブックがあります。一つは「必要性のガイド」と呼ばれるもので、これはあらゆる可能な現実において何が「真」であるべきかを判断するのに優れています。もしあらゆる可能世界で雨が降っているなら、このガイドはその現象が「必然的」であることを教えてくれます。もう一つのルールブックは、「リソース・マネージャー」と呼ばれるもので、これはお金やエネルギー、コンピュータのメモリといった物理的なものを扱うための設計図です。ここには特別なルールがあります。リソースを単にコピー＆ペーストすることはできないというルールです。もし1ドルを使ってクッキーを買ったなら、その1ドルは消えてしまいます。その1ドルを使って再び2つ目のクッキーを買うことはできません。これは「分離論理（separation logic）」の世界であり、そこでは物事は繰り返されるのではなく、分割され、結合されます。

長い間、これら2つのルールブックは異なる言語を話しているようでした。「必要性のガイド」（S4と呼ばれる種類の論理）と「リソース・マネージャー」（BBIと呼ばれる論理）は、まるで同じソフトウェアを実行できない2つの異なるオペレーティングシステムのようなものでした。コンピュータ科学者や論理学者は、これらを結びつけることに深い関心を寄せています。なぜなら、これらを翻訳できれば、一方の強力なツールを使って他方の問題を解決できるからです。これは、コンピュータプログラムが安全であることを確認し、プログラムがクラッシュしたり秘密のデータを漏洩したりしないことを保証するために非常に重要です。大きな疑問は、「『必然性』のルールを、意味を失うことなく『リソース』のルールへと変換する完璧な翻訳機を作れるか？」ということでした。

本論文は、この翻訳機を構築するための全く新しい方法を提示しています。著者であるダニエレ・サンソニとラナルド・クラウストンは、「必要性のガイド」（S4）が「リソース・マネージャー」（BBI）の中に完璧に埋め込み可能であることを示す証明を作成しました。従来の試みは、これらの論理がどのように振る舞うかを示す複雑な視覚的マップに依存していましたが、この新しい証明は完全に「構文的（syntactical）」なものです。つまり、完成したパズルの絵を見るのではなく、ピースを動かしてパズルを解くように、記号とルール自体を並べ替えることで機能します。

著者たちは、この翻訳が驚くほど頑健であることを示しています。これは単に基本的なルールに対して機能するだけでなく、どちらかのシステムに新しい、より複雑なルールが追加されたとしても、その真実性を維持します。彼らは、リソースのルールを必要性のルールへと書き戻す「逆翻訳機」を発明することで、これを証明しました。もし、あるルールを「必要性」から「リソース」へ翻訳し、その直後に再び「必要性」へと翻訳した場合、元のルールと全く同じものに戻ることを彼らは実証しました。この「打ち消し合い」の効果が、このつながりが強固で信頼できるものであることを証明しています。

さらに、本論文は「仮定のリスト」がある場合に何が起こるかという難しい問題にも取り組んでいます。論理学では、しばしば「Xと仮定するならば、Yが導かれる」といった表現を用います。著者たちは、単純なリストであっても、あるいはリソースをグループ化する特殊な方法である「バンチ（bunches）」によって整理された複雑な構造であっても、仮定を扱っている場合でも、この翻訳が機能することを証明しました。また、彼らはこの手法が、ハイブリッドな特徴（特定の場所を指定する名前付けなど）を扱ったり、新しい論理結合子を追加したりする、リソース・マネージャーのいくつかの高度なバージョンに対しても有効であることを示しました。

要するに、この論文は単に両者の間にリンクがあることを示唆するだけでなく、これら2つの論理の世界が深くつながっていることを示す厳密でステップ・バイ・ステップの証明を提供しています。それは、「必然性」（何が真であるべきか）という概念が、「リソース」（何を所有しており、それをどのように分割するか）というレンズを通して完全に理解できることを示しています。これは、モダル論理の問題をリソースベースの思考を用いて解決すること、またその逆を行うことへの扉を開き、複雑なコンピュータシステムが正しく動作していることを検証することをより容易にする可能性があります。著者たちは、自分たちの結果が確立された数学的基礎の上に築かれていることをもって、この新しい翻訳機が単なる巧妙なトリックではなく、これらのシステムがどのように関連しているかについての根本的な真理であることを確信しています。