集合論と圏論がズレるとき：空リスト問題 - 檜山正幸のキマイラ飼育記 (はてなBlog)

プログラミング言語や型理論の文脈で、空リストの型つけ〈タイピング〉が話題になることがあります。集合論と圏論で解釈してみると、結果が違ってきます。発想が違うので結果がズレるのは驚くことではありませんが、意外に思う人もいるかも知れません。 $\newcommand{\Map}{\mathrm{Map}} \newcommand{\uMap}{\underline{\mathrm{Map}} } \newcommand{\Imp}{\Rightarrow } \newcommand{\Iff}{\Leftrightarrow } \newcommand{\dom}{\mathrm{dom} } \newcommand{\cod}{\mathrm{cod} } \newcommand{\cat}[1]{\mathcal{#1} } % category \newcommand{\Pow}{\mathrm{Pow} } \newcommand{\hyp}{\text{-} } \newcommand{\List}{\mathrm{List} } % \require{color} \newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} }% \newcommand{\For}{\Keyword{For } }% \newcommand{\Define}{\Keyword{Define } }% \newcommand{\Holds}{\Keyword{Holds } }%$

内容：

はじめに
圏のホムセットは交わらない
写像集合とは
リストの定義
空リストの型

はじめに

ここで言う集合論は、ガチの公理的集合論ではなくて、公理的集合論寄りの素朴集合論です。よく知られた集合論的概念は普通に使っていいとします。集合圏 ${\bf Set}$ は、普通の集合論に基づいて考えます。集合圏の対象の集まり $|{\bf Set}|$ は「すべての集合の集まり〈類〉」です。集合圏のホムセット ${\bf Set}(A, B)$ は、「集合 $A$ から集合 $B$ への写像の集合」です。

集合圏のホムセット ${\bf Set}(A, B)$ とは別に、集合論的に構成された「集合 $A$ から集合 $B$ への写像の集合」は $\uMap(A, B)$ と書くことにします。下線を付けているのは、僕は $\Map(A, B)$ を ${\bf Set}(A, B)$ の別表記として使っているからです。定義から $\Map(A, B) = {\bf Set}(A, B)$ となってしまって、話すことがありません。

話すことがあるということは、 ${\bf Set}(A, B)$ と $\uMap(A, B)$ は幾分か違う、ってことです。それが今回の話題。

圏のホムセットは交わらない

かつて「ホムセットは交わるのか」で話題にしたことがありますが、圏のホムセットは交わりません。このことは、次の論理式として書けます。

$\quad (A, B) \ne (C, D) \Imp \cat{C}(A, B) \cap \cat{C}(C, D) = \emptyset$

同じことですが、次のようにも書けます。

$\quad \cat{C}(A, B) \cap \cat{C}(C, D) \ne \emptyset \Imp (A, B) = (C, D)$

これを示してみます。

空でない集合から要素をとって $f \in \cat{C}(A, B) \cap \cat{C}(C, D)$ とします。これはつまり、

$\quad (\dom(f) = A \land \cod(f) = B) \land (\dom(f) = C \land \cod(f) = D)$

これより

$\quad A = \dom(f) = C\\ \quad B = \cod(f) = D$

言い換えれば：

$\quad (A, B) = (C, D)$

圏論では、射のプロファイル（域・余域のペア）が違えば、射の実体を見るまでもなく違う射だと判断します。肩書きが違えば中身がなんであっても違うのです。特に、 $A \ne B$ のとき、 ${\bf Set}(\emptyset, A) \cap {\bf Set}(\emptyset, B) = \emptyset$ です。

写像集合とは

次に、集合論的に構成された「集合 $A$ から集合 $B$ への写像の集合」 $\uMap(A, B)$ を構成します。 $A$ から $B$ への写像を、 $A$ から $B$ への関係の特殊なものだとみなします。関係 $R:A \to B$ の集合論的実体は $R\subseteq A\times B$ だとします。 $A$ から $B$ への関係が写像である条件は次です。

$\For R \subseteq A\times B\\ \Define \mathrm{IsMap}(R) :\Iff \\ \quad \forall x\in A. \exists y\in B.\, (x, y)\in R \\ \quad \land \\ \quad \forall x\in A. \forall y, y'\in B.\, ((x, y)\in R \land (x, y')\in R) \Imp y = y'$

写像とは、全域的に定義された値が一意的な関係です。未定義（値が無し）や多値（値がたくさん）が起きてはダメです。今定義した述語 $\mathrm{IsMap}$ を使って写像集合を定義します。

$\For A, B\in |{\bf Set}|\\ \Define \uMap(A, B) := \{ R\in \Pow(A\times B) \mid \mathrm{IsMap}(R) \}$

ここで、 $\Pow(\hyp)$ はベキ集合です。

定義から、 $\uMap(A, B) \subseteq \Pow(A\times B)$ です。特に、

$\quad \uMap(\emptyset, A) \subseteq \Pow(\emptyset \times A) = \Pow(\emptyset)\\ \quad \Pow(\emptyset) = \{\emptyset\}$

なので、次のどちらかが成立します。

$\uMap(\emptyset, B) = \{\} = \emptyset$
$\uMap(\emptyset, B) = \{\emptyset\}$

どちらになるかは $\mathrm{IsMap}(\emptyset)$ の真偽によりますが、 $\mathrm{IsMap}(\emptyset)$ は真です（成立してます）。なぜかというと、写像の条件である $\forall x\in \emptyset.(\cdots)$ を $\forall x.(x\in \emptyset \Imp \cdots)$ と書き換えてみると、含意の前件が偽となり命題は常に真となるからです。

このことから、集合 $B$ が何であっても、

$\quad \uMap(\emptyset, B) = \{\emptyset\}$

$B \ne C$ であっても、

$\quad \uMap(\emptyset, B)\cap \uMap(\emptyset, C) \ne \emptyset$

です。集合圏のホムセットの場合とは事情が異なります。

$A \ne \emptyset$ の場合でもあっても、次が成立します。

$\quad B \ne \emptyset \land C \ne \emptyset \land B \subseteq C \land B \ne C\\ \quad \Imp \uMap(A, B) \cap \uMap(A, C) \ne \emptyset$

異なる集合ペア $(A, B) \ne (C, D)$ に対しても、

$\quad \uMap(A, B) \cap \uMap(C, D) \ne \emptyset$

となることはけっこうあります。

集合圏のホムセットは次のように定義されていると思えばいいでしょう。

$\For A, B\in |{\bf Set}|\\ \Define {\bf Set}(A, B) := \{A\}\times \uMap(A, B) \times \{B\}$

リストの定義

集合 $A$ に対して、 $A$ の要素を成分とするリストの集合を $\List(A)$ と書きます。ここでは、 $\List(\hyp)$ の定義を2種類準備します。それに先立ち次の約束をしておきます。

$\quad \bar{0} = \{\}\\ \quad \bar{1} = \{1\}\\ \quad \bar{2} = \{1, 2\}\\ \quad \bar{n} = \{1, 2, \cdots, n\}$

2種類のリストは $\List 1(\hyp),\, \List 2(\hyp)$ とします。以下に出てくる記号 ' $+$ ' は集合の直和です。

$\For A \in |{\bf Set}|\\ \Define \List 1(A) := {\bf Set}(\bar{0}, A) + {\bf Set}(\bar{1}, A) + {\bf Set}(\bar{2}, A) + \cdots$

$\For A \in |{\bf Set}|\\ \Define \List 2(A) := \uMap(\bar{0}, A) + \uMap(\bar{1}, A) + \uMap(\bar{2}, A) + \cdots$

長さが0のリストの集合を $\List 1_0(A),\, \List 2_0(A)$ とすると、

$\quad \List 1_0(A) = {\bf Set}(\bar{0}, A) \\ \quad \List 2_0(A) = \uMap(\bar{0}, A)$

空リストの型

$\List 1_0(A),\, \List 2_0(A)$ はどちらも単元集合〈singleton set〉であり、ただひとつの要素は空リストです。が、全体として空リストが“どのくらいあるか”はそれぞれの場合で違ってきます。

$\List 1_0(A) = {\bf Set}(\bar{0}, A)$ だと、集合 $A$ ごとに異なる空リストが存在します。空集合 $\bar{0} = \emptyset$ は集合圏の始対象なので、集合 $A$ ごとに射 $\emptyset \to A$ が一本ずつあるのです。空リストの正体は始対象からの射で、空リストはたくさんあります。そして、空リストの型（空リストが所属する集合）もたくさんあります。

$\List 1_0(A) = \uMap(\bar{0}, A)$ だと、集合 $A$ によらずにこの世にひとつだけの空リストが存在します。空リストの型を（そうしたいなら）一意に決めることが出来ます。その型は集合 $A$ とは無関係な「空リストのみの型」（集合としては $\{()\}$ ）というべきものです。

例えば構文的に $()$ と書かれた空リストを目の前に出されて「これの型は何か？」と聞かれても答えようがありません。何らかの背景に基づいて答えるにしても、背景により答え方は変わってきます。それはそういうものです。