Setoids in Intensional Type Theory

偉大なる翻訳：厳格なルールを柔軟な道具へと変える

想像してみてください。あなたは、信じられないほど厳格な指示書を使って家を建てようとしています。すべてのレンガは特定の順番で置かれなければならず、もしほんの少しでもミスをすれば、計画全体が崩壊してしまいます。これが**内包的型理論（Intensional Type Theory）**の仕組みです。これは、コンピュータ科学者や数学者がソフトウェアにバグがないことを証明するために使用する、超精密な言語です。それは、正確でステップバイステップのコマンドのみに従うロボットのようなものです。もし二つのものが見た目が同じであっても、作り方が異なれば、そのロボットは「いいえ、それらは別物です！」と言います。なぜなら、ロボットは「何を持っているか」ではなく、「どのようにそこに到達したか」を重視するからです。

さて、結果だけを重視する別の種類の建築家を想像してみてください。もし二つの家が外観から見て同一に見えるなら、この建築家は「これらは同じ家だ！」と言います。これが**外延的型理論（Extensional Type Theory）**です。これは、宇宙の形状やキノコの成長の論理といった複雑な数学的構造を記述するのに、より柔軟で自然です。しかし、この柔軟性には代償があります。この柔軟な言語のルールが矛盾（例えば、立っている状態と崩壊している状態の両方の家など）を招かないことを証明するのは、はるかに困難なのです。

長い間、科学者たちは疑問に思っていました。「私たちは、すでに持っている厳格な『内包的』な道具だけを使って、この柔軟な『外延的』な言語のモデルを構築できるのだろうか？」これは、流動的で形を変える彫刻を、硬くて四角いレゴブロックだけで作ろうとするようなものです。もしそれが実現できれば、柔軟な言語を使用しても安全であることが証明されます。なぜなら、厳格な道具しか持っていなくても、それをチェックできるからです。これが、アンドリュー・ピッツ（Andrew Pitts）が論文で取り組んでいる大きな問いです。

論文：硬いレンガで柔軟な世界を築く

ケンブリッジ大学のアンドリュー・ピッツは、この論文の中で、厳格な内包的型理論（彼はこれをIRUと呼びます）を用いて、柔軟な外延的型理論（彼はこれをETUと呼びます）のモデルを構築できることを示しています。彼は、**ディスプレイド・セトイド（displayed setoids）**と呼ばれる特別な種類の「翻訳レイヤー」を作成することでこれを行いました。

**セトイド（setoid）**を「曖昧な箱」と考えてみてください。箱の中には、アイテムの集合が入っています。しかし、二つのアイテムが「全く同一である」と言う代わりに（それは厳格なロボットには難しすぎます）、この箱には特別なルールがあります。「これらの二つのアイテムは、特定のテストに合格すれば『同等』である」というルールです。それは、クラブのメンバーになるために、必ずしも会長と全く同じ人間である必要はなく、ただメンバーシップ・テストに合格すればよい、というようなものです。

難しい部分は、このディスプレイド・セトイドです。メインの地図（厳格な内包的世界）があるとしましょう。次に、その上に、より柔軟な地図（外延的世界）を描きたいとします。「ディスプレイド・セトイド」は、その地図の上に貼り付ける透明なフィルムのようなものです。このフィルムの上に新しい接続やルールを描くことで、地図上の硬い点が、柔軟な世界が必要とするように、流動的に変化しているように見せることができるのです。

ピッツの主要な発見は、IRUの厳格な道具で作れるほどシンプルでありながら、ETUの挙動を模倣できるほど複雑な、これらの「透明なフィルム（ディスプレイド・セトイド）」を設計する方法を見つけたことです。彼は単に推測したのではなく、プログラムが勝手に独自のルールを作り出すことを防ぐ「安全な」モードを使用したAgdaというコンピュータプログラムの中で、完全な動作モデルを構築しました。

魔法がどのように起きるのかを説明します：

1. 問題： 厳格な世界では、二つのものが等しいと証明することは困難です。柔軟な世界では、それは容易です。論文は、厳格な世界が自身のルールを破ることなく、いかにして柔軟な世界のように振る舞うかという方法を必要としていました。
2. 解決策： ピッツは、型の「コード」（レゴブロックの設計図のようなもの）を定義し、次にいつ二つのコードが「同等」とみなされるかのルールを定義するという手法を用いました。彼は、それぞれの箱がその中にあるもののルールを含んでいるような、入れ子状の箱の階層構造を構築しました。
3. 結果： これらのディスプレイド・セトイドを使用することで、彼はETUのあらゆるルールを厳格なIRUへと翻訳することができました。彼は、もしあなたがETUのルールに従うならば、決して矛盾（例えば、特定の種類の「空の」箱の中に実際に何かが入っていると証明してしまうようなこと）に陥らないことを証明しました。

この論文は、これが簡単なことではない、あるいは過去の試みが完全ではなかったという考えを明確に退けています。著者は、他の人々もこれに挑戦してきたものの、多くの場合、難しい部分を省略していたり、あるいは（見た目が同じであるという理由だけでそれらが等しいと仮定するような）強力すぎる道具を使用していたりしたと指摘しています。ピッツのアプローチは「ベアボーン（最小限の構成）」です。つまり、彼はこの仕事を遂行するために最もシンプルな道具を使用しており、派手で未証明の機能を使わなくても、これが機能することを証明したのです。

この論文の最もエキサイティングな部分は、その結論です。彼がこのモデルの構築に成功したことにより、**ETUは一貫している（consistent）**ことが証明されました。平易な言葉で言えば、彼は、彼の厳格な内包的モデルというレンズを通して見る限り、外延的型理論の柔軟な言語がクラッシュしたり矛盾したりすることはない、ということを示したのです。それは、ぐらつく、形を変える塔が、実は揺るぎないコンクリートの基礎の上に築かれているために安定している、と証明するようなものです。

これは単なる理論的なゲームではありません。これが重要なのは、コンピュータ科学者が飛行機から医療機器に至るまで、あらゆるものを制御するソフトウェアを書くために、これらの理論を使用するからです。もし言語のルールが不安定であれば、ソフトウェアは失敗する可能性があります。この柔軟なルールが安全であることを示すことで、ピッツはエンジニアや数学者が複雑なシステムを構築することへの信頼を与えています。論文は、これがコンピュータ科学のあらゆる問題を解決したと主張しているわけでも、これが唯一の方法であると言っているわけでもありません。単に、この特定の困難な翻訳が可能であることを証明しており、それを機械検証された証明のみが提供できるレベルの確実性をもって行っているのです。

結局のところ、ピッツは二つの世界の間の架け橋を築いただけではありません。彼は、最も単純で信頼できる道具だけを使って、最も複雑な数学的アイデアの重みに耐えられるほど、その架け橋が強いものであることを示したのです。それは、網で煙を捕まえようとするような感覚を伴う分野において、注意深く、ステップバイステップの思考がいかに強力であるかを示す証左となっています。