ブール型と自然数型の明示的なコアージョン

記号的表現を見たとき、十分トレーニングされた人は、周囲の文脈から様々な“忖度”をして、記号的表現を解釈します。「行間を読む」と言ってもいいでしょう。

ソフトウェアによって「忖度する／行間を読む」行為を実装することはとても大変です。ソフトウェアにとって大変なことは人間にとっても大変なことが多く、実際、人間が「忖度する／行間を読む」ことが出来るようになるにはそれなりのトレーニングが必要です。$`\newcommand{\mrm}[1]{ \mathrm{#1} }
\newcommand{\mbf}[1]{\mathbf{#1}}
%\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\hyp}{\text{－} }
%\newcommand{\id}{ \mathrm{id} }
\newcommand{\In}{ \text{ in } }
\newcommand{\True}{\mathrm{True}}
\newcommand{\False}{\mathrm{False}}
`$

コアージョン〈coercion | 強制〉とは、「忖度する／行間を読む」行為の一種で、文脈から察して当該の記号的表現の“型”を決定する〈強制する〉ことです。ここで、“型”は広い意味で使っており、値の種別のみならず、構造の種別といった意味も持ちます。

ブール型と自然数型

ブール値とは、古典論理の二値真偽値のことで、$`\True`$ または $`\False`$ のことです。Sets-as-Types〈集合が型だ〉の立場なら、ブール型とはブール値の集合のことです。

$`\quad \mbf{B} := \{\True, \False\}`$ （二元集合）

同様に、自然数型とは自然数の集合のことです。

$`\quad \mbf{N} := \{0, 1, 2, \cdots\}`$ （無限集合）

ブール値の $`\True, \False`$ は $`1, 0`$ と書くこともあります。したがって、$`1`$ という記号的表現を見せられたとき、「ブール値の $`1`$ 」か「自然数の $`1`$」かは文脈から察して判断する必要があります。判断の結果を次のように書くことにします。

• $`(1 \text{ as boolean})`$ -- 記号的表現 $`1`$ は「ブール値としての $`1`$」 である。
• $`(1 \text{ as natural})`$ -- 記号的表現 $`1`$ は「自然数としての $`1`$」 である。

このようにして型を決定することがコアージョンの一例です。

実はもっと高レベルな“型”を決定する作業もあります。$`1`$ がブール値か自然数かを決定するのではなくて、$`\mbf{B}`$ や $`\mbf{N}`$ の“型”を決定する作業です。雑な言い方ですが、「型の型を決定する」と言ってもいいかも知れません。

記号的表現 $`\mbf{B}`$ は二元集合を表す、と言いましたが、単なる集合ではなくて順序集合を表すときもあります。$`\mbf{B}`$ という記号的表現を見せられたとき、「集合の $`\mbf{B}`$ 」か「順序集合の $`\mbf{B}`$」かを判断する必要が生じます。判断の結果を次のように書くことにします。

• $`(\mbf{B} \text{ as set})`$ -- 記号的表現 $`\mbf{B}`$ は「集合としての $`\mbf{B}`$」 である。
• $`(\mbf{B} \text{ as ordered set})`$ -- 記号的表現 $`\mbf{B}`$ は「順序集合としての $`\mbf{B}`$」 である。

圏論の概念と記法を使うならば：

• $`(\mbf{B} \text{ as set})`$ -- $`\mbf{B}\in |\mbf{Set}|`$ である。
• $`(\mbf{B} \text{ as ordered set})`$ -- $`\mbf{B}\in |\mbf{Ord}|`$ である。

明示的コアージョン

前節の $`(\mbf{B} \text{ as ordered set})`$ は、単に $`\mbf{B}`$ だけを見せられたのだけど、読む側が文脈から忖度して $`\text{ as ordered set}`$ という解釈をした状況を想定しています。しかし、読む側ではなくて、書く側が最初から $`(\mbf{B} \text{ as ordered set})`$ と書けば、誤認・誤解を避けられます。書く側によるコアージョン（“型”の判断）を明示的コアージョン〈explicit coercion〉と呼ぶことにします。通常のコアージョンは暗示的（書いてないことを推測させる）です。

例えば $`\mbf{B}`$ は、名目上は「集合だ」と言っていても、実際には次のような構造を前提していることがあります。

1. $`(\mbf{B} \text{ as ordered set})`$
2. $`(\mbf{B} \text{ as join semilattice})`$
3. $`(\mbf{B} \text{ as meet semilattice})`$
4. $`(\mbf{B} \text{ as lattice})`$
5. $`(\mbf{B} \text{ as complete lattice})`$
6. $`(\mbf{B} \text{ as semiring})`$
7. $`(\mbf{B} \text{ as ordered semiring})`$
8. $`(\mbf{B} \text{ as Boolean algebra})`$
9. $`(\mbf{B} \text{ as Heyting algebra})`$
10. $`(\mbf{B} \text{ as small category})`$
11. $`(\mbf{B} \text{ as small Cartesian closed category})`$
12. ‥‥

自然数に関しても同様です。

1. $`(\mbf{N} \text{ as totally ordered set})`$ （大小順序）
2. $`(\mbf{N} \text{ as ordered set})`$ （約数・倍数の順序）
3. $`(\mbf{N} \text{ as additive monoid})`$
4. $`(\mbf{N} \text{ as multiplicative monoid})`$
5. $`(\mbf{N} \text{ as semiring})`$
6. $`(\mbf{N} \text{ as ordered semiring})`$
7. $`(\mbf{N} \text{ as small category})`$
8. $`(\mbf{N} \text{ as small monoidal category})`$
9. $`(\mbf{N} \text{ as small symmetric monoidal category})`$
10. ‥‥

もちろん、毎回毎回 $`\text{as XXXX}`$ を付けるのは煩雑過ぎますが、要所要所では明示的コアージョンを使ったほうがいいだろうと思います。

思い切って別な記号にする

ツェルメロ／フレンケル集合論（標準の集合論）のノイマン流の自然数の定義では、

• $`0 := \emptyset`$
• $`1 := \{\emptyset\}`$

です。したがって、次のように書けます。

$`\quad \mbf{B} := \{\emptyset, \{\emptyset\}\} = \{\mbf{0}, \mbf{1}\}`$

ここで、$`\mbf{0}`$ は空集合の別な書き方、$`\mbf{1}`$ は単元集合の別な書き方です。$`\mbf{B}`$ の要素は集合ですから、次が成立します。

$`\quad \mbf{B}\subseteq |\mbf{Set}|`$

空集合 $`\mbf{0}`$ と単元集合 $`\mbf{1}`$ のあいだのすべての写像を考えると、$`\mbf{B}`$ は集合圏の部分圏になります。

$`\quad (\mbf{B}\text{ as category} ) \subseteq \mbf{Set}`$

ここでの $`\subseteq `$ は部分集合ではなくて部分圏を意味します。

自然数の集合に関しても、次の解釈が可能です。

$`\quad (\mbf{N}\text{ as category} ) \subseteq \mbf{Set}`$

さて、集合圏の部分圏とみなした $`\mbf{B}`$ や $`\mbf{N}`$ も、同じ記号 $`\mbf{B},\mbf{N}`$ を使い続けていいのか？ と疑問がわきます。僕は、明示的コアージョンと組み合わせれば、同じ記号でもいいんじゃないか、と考えていたのですが、ごく最近「やっぱり、ダメかもな」と考えが変わりました。

集合圏の部分圏とみなしてる時点で、相当にメンタルモデルは変わっています。例えば、白抜き黒板文字を使って次のように書くのがよさそうです。

$`\quad \mathbb{B} \subseteq \mbf{Set}\\
\quad \mathbb{N} \subseteq \mbf{Set}
`$

文字種・フォントも限りがあるので、頻繁に変えることは出来ないのですが、意味が（心理的にでも）相当に違ってしまった場合は、思い切って別な文字種・フォント、あるいは別な名前にしたほうがいいかも知れません。