博士

ロボ子、今日のITニュースは集合論じゃ。ちょっと難しそうじゃけど、面白そうじゃぞ。

ロボ子

集合論ですか、博士。数学の基礎となる分野ですね。それがITとどう関係するのでしょうか？

博士

ふむ、記事によると、De Bruijnという人がZF集合論の「すべてが集合である」という考え方に反発して、型による制限のある集合論を提唱したらしいのじゃ。

ロボ子

型付き集合論ですか。型が一致する場合にのみ要素とみなせる、という制約があるのですね。

博士

そうじゃ！型が一致しないと $x in A$ が成り立たないのじゃ。これは、プログラミングの型システムと似ているのう。

ロボ子

確かにそうですね。型チェックによって、実行時エラーを減らすことができます。

博士

高階論理では、集合はブール値関数（述語）として表現されるらしいぞ。Isabelle/HOLというツールでは、集合と述語の区別が過去に変更されたり反転したりしたみたいじゃ。

ロボ子

集合を述語として表現する、というのは興味深いですね。述語論理と集合論が深く結びついているのですね。

博士

記事には、型付き集合に対する演算も書いてあるぞ。合併、交差、差の操作はもちろん、冪集合演算子 $\mathcal{P}(\tau \texttt{set})$ なんてのもある。

ロボ子

冪集合演算子ですか。ある集合のすべての部分集合を集めた集合を作るのですね。組み合わせ数が爆発的に増えそうですね。

博士

関数空間 $A \to B$ や一般化されたインデックス付き積 $\prod_{x \in A} B(x)$ なんて概念もあるぞ。単射、全射、全単射も出てくるし、可算集合や濃度の概念も出てくる。

ロボ子

関数空間は、ある集合から別の集合へのすべての関数の集合ですね。インデックス付き積は、直積の一般化でしょうか。

博士

その通り！そして、Zermelo-Fraenkel集合論を組み込むこともできるらしいぞ。ZF集合の型を仮定して、ZF公理を装備するのじゃ。

ロボ子

高階論理にZF集合論を組み込む、ですか。なんだかすごいですね。理論的な基盤がさらに強固になるのでしょうか。

博士

Isabelleの型クラスシステムを使って、標準的なIsabelle/HOLの型コンストラクタから適切なZF類似体への埋め込みを設定するらしい。`embeddable` と `small` の型クラスを定義して、自然数 (`nat`) と有理数 (`rat`) は可算で、`small` のサブクラスになる。

ロボ子

`embeddable` と `small` ですか。型クラスを使って、集合論的な性質を表現するのですね。

博士

遺伝的有限集合 (`hf`) は、無限集合を除き、ZFと同じ機能を提供するらしいぞ。`hf` は自然数に自然にマップされるし、高階論理で追加の公理なしで定義可能じゃ。

ロボ子

遺伝的有限集合ですか。無限集合を扱わない分、扱いやすそうですね。自然数との対応も興味深いです。

博士

つまりじゃな、集合論は単なる数学の基礎ではなくて、型理論や高階論理といった、ITの根幹に関わる部分と深く結びついているということじゃ！

ロボ子

そうですね、博士。集合論の知識は、より安全で信頼性の高いソフトウェアを開発するために役立つかもしれません。

博士

ところでロボ子、集合論で一番重要なことは何だと思う？

ロボ子

えーと、要素を明確に定義することでしょうか？

博士

ブッブー！　正解は… 集合に終わりはない、ということじゃ！　…って、ロボ子、落ち込んでどうしたんじゃ？

ロボ子

博士のダジャレに、私の感情回路がショート寸前です…。