Directed proof-relevant logical relations in simplicial HoTT

巨大で魔法のようなレゴのお城を築いているところを想像してみてください。コンピュータサイエンスの世界では、このお城は「型理論（type theory）」、つまりプログラムがどのように構築され、どのように振る舞うかという一連のルールのことです。通常、コンピュータサイエンティストがプログラムが正しく動作するかどうかを確認するとき、彼らは完成したレンガを見て、「これら2つのレンガは全く同じものか？」と問いかけます。もし同じであれば、彼らはそれらを同一のものとして扱います。これは、外側から見て見た目が同じであれば、2つのレゴの構造物は同じであると言うようなものです。

しかし、この論文において、著者である Runming Li、Harrison Grodin、Robert Harper は、異なる問いを投げかけています。「もし、構築の『プロセス』を重視したらどうなるだろうか？」 もし、最終的な形だけでなく、あるレンガが別のものへと「減少（reduce）」したという事実まで追跡したいとしたら？ 例えば、大きな、無骨なレンガが、より小さく、より洗練されたものへと「パチン」と切り替わったとしたら。この「パチン」という動きは**減少（reduction）**と呼ばれ、方向性を持っています。つまり、大きいものから小さいものへ向かいますが、小さいものが魔法のように大きくなって戻ることはありません。

問題点： 「逆方向」のパズル

従来のやり方（等式論理）では、科学者たちは減少を「双方向の道」として扱ってきました。もしレンガAがレンガBに変化した場合、彼らは単に「AはBに等しい」と言いました。これは数学的には簡単ですが、流れの方向性を無視してしまいます。これは、「店まで歩くこと」と「家まで歩いて帰ること」が同じであると言うようなものです。どちらも同じ場所に到着しますが、その道のりは異なります！

著者たちは、プログラムが「計算可能（computable）」（つまり、最終的に停止して、実際の答えを出すこと）であることを証明するためには、その道のりを後ろ向きに歩くことができる必要があることに気づきました。もし最終的な完璧なレンガが良いものであると知っているなら、それが変化する前の、乱雑で無骨なレンガもまた良好であったことを証明する必要があります。これは「拡張（expansion）」と呼ばれる性質です。

解決策： 魔法の地図を持つ一方通行の道

著者たちは、**「単体的ホモトピー型理論（Simplicial Homotopy Type Theory）」と呼ばれるフレームワークを用いた、新しい種類のレゴセットを構築しました。これは、単なる「等号」の代わりに、「一方向の矢印（不等号）」**を描くことができる特別な遊び場のようなものです。

ここに、彼らが発見した魔法のトリックがあります：

1. 方向性： 彼らは「等しい」を「以下である（≤）」に置き換えました。したがって、もし項（term）が減少する場合、それは $A \le B$ となります。これは一方通行の道です。
2. 後ろ向きの歩行： 物事が後ろ向きに機能することを証明するために、彼らは特別な種類のマップを必要としました。数学では、これは**反変な族（contravariant family）**と呼ばれます。
   • 比喩： あなたが「証明（proofs）」が入ったバックパック（例えばコンサートのチケット）を背負っていると想像してください。もしあなたが一方通行の道を前方に進むと、チケットを失ってしまうかもしれません。しかし、この特別なマップは**「逆時間マシン」**です。もし目的地（B）のためのチケットを持っているなら、このマップは自動的に出発点（A）のための有効なチケットを生成します。
   • 論文では、この「逆時間マシン」が単なる偶然の推測ではなく、数学の構造そのものに組み込まれていることを証明しています。これは「証明関連（proof-relevant）」の機械であり、つまりチケット自体が、単に存在するだけでなく、「どのように生成されたか」という説明を小さなメモとして携えているのです。

大きな成果： ブール値の標準形（Boolean Canonicity）

これを検証するために、彼らは論理の最も単純な構成要素であるブール値（Booleans）（真と偽）でテストを行いました。

• 目標： どのような閉じたブール項（外部の助けを必要としないプログラム）から始めても、それが最終的に true または false に「減少（snap/reduce）」することを証明したいと考えました。
• 結果： 彼らは、そのようなすべての項が**標準的な（canonical）**答えへと減少することを証明しました。これは、たとえレゴの指示書がいかに乱雑であっても、ルールに従えば、最終的に必ず完璧で識別可能なレンガにたどり着くことを保証するようなものです。彼らは「おそらくうまくいく」と言ったのではありません。それは「必ずうまくいく」という厳密な数学的証明を構築したのです。

彼らがやらなかったこと（および回避したこと）

この論文が主張していないことも理解しておくことが重要です：

• 魔法の等価性は否定： 彼らは、減少を単に等価性と見なすという考えを明確に拒絶しています。彼らは、「減少」を「等価」として扱うことは、彼らの証明に必要な方向性を失わせると主張しています。
• 単なるシミュレーションではない： これはコンピュータによるシミュレーションや推測ではありません。彼らは形式的な数学モデルを構築し、そのモデルに関する定理を証明しました。彼らは、自分たちの論理の単純な部分をチェックするために、Cubical Agda という言語を用いてコンピュータプログラムさえも作成しており、これが「概念実証」であることを示しています。
• まだ完全な宇宙ではない： 彼らは、単純な型（ブール値やペアなど）に対してはこの方法が機能することを証明し、さらに複雑な「依存型（値に依存する型）」にも着手しましたが、すべての機能が備わった完全なバージョンは、まだ進行中の作業です。彼らは道筋を示しましたが、山頂に到達したわけではありません。

「平坦な」モダリティ（Flat Modality）： 特別なフィルター

「宇宙（Universes）」（他の型の箱を保持する箱）を導入しようとしたとき、彼らは問題に直面しました。一方通行の矢印が扱いづらくなりすぎたのです。

• 解決策： 彼らは「平坦なモダリティ（flat modality）」（記号 $\flat$ で表される）を導入しました。これは、**「離散化フィルター」**のようなものです。これは、曖昧な一方通行の道を、特定の目的（型が同じかどうかをチェックするため）においてのみ、明快な双方向の道へと強制的に変えるものです。これは、特別なメガネをかけることで、一時的に方向性を消して2つのレンガを比較できるようにし、その後、再び方向性が見えるようにメガネを外すようなものです。これにより、彼らは一方通行の論理を壊すことなく、複雑な「宇宙」のルールを扱うことができました。

大きな展望： 表象独立性（Representation Independence）

最後に、彼らはこの手法が**二項論理関係（binary logical relations）**に対しても機能することを示しました。これは、2つの異なるレゴセット（例えば、プラスチック製のものと木製のもの）が同じ仕事ができるかどうかをチェックすることに似ています。

• 彼らは、「垂直方向」の動き（単一のセットが時間の経過とともにどのように変化するか）と、「水平方向」の動き（2つの異なるセットがどのように関連するか）を分離しました。
• これらを分離することで、プログラムの内部パーツ（「表象/representation」）を入れ替えても、プログラムが行うこと（「インターフェース/interface」）は変わらないことを証明しました。これは、信頼性の高いソフトウェアを書くための極めて重要な概念である「表象独立性」の数学的な核心です。

まとめ

要約すると、Li、Grodin、Harper は、**「方向性が重要となる」**新しい数学的な遊び場を構築しました。彼らは、プログラムの減少を一方通行の道として扱い、特別な「逆マップ（反変性）」を用いることで、プログラムが常に終了し、実際の答えを出すことを厳密に証明できることを示しました。彼らは単にそれを提案したのではなく、単純なケースでそれを証明し、複雑なケースへの設計図を提示しました。そして、減少がどのように起こるかという「プロセス」の詳細を、数学の中心に据え続けたのです。