通常の型 Int や Bool にBottom型を追加した集合

一般に、集合Sに\botを追加した集合をS_\botと表記する

だから、\mathrm{Int}_\botや\mathrm{Bool}_\botになる

例えば、\mathrm{Bool}の値は、 true と false だが、

\mathrm{Bool}_\botの値は、 true 、 false 、 ⊥ である

Haskellの場合は、通常の型に既にbottomは含まれている

それが undefined という値

Bool 型は3つの値、 true 、 false 、 ⊥ が属している

同様にvoid型 () も2つの値、 () , ⊥ が属している

(inhabitantの話と若干ズレるのでややこしいな)

inhabitantの話をしている時は、普通 ⊥ を無視すると思う

この集合は

平坦領域である

つまり記号のイメージとしての\sqsubsetのようなものが、\botとの関係にしかない

\bot \sqsubset aか

a=bにしかならない

\bot以外が並列にある感じ

自然数の通常の大小関係\leも定義されてはいるが、\sqsubseteqとは無関係である

意味近似順序の観点で見れば、1と2の定義のされ具合は同じである

そう書くと、1\sqsubseteq2と書けてしまいそうなので、言い方がちょっと良くないな

例えば、 Int に\botを加えた集合\mathrm{Int}_\botを意味近似順序(\sqsubseteq)で順序付けした時

ハッセ図式は、以下のようになる

図を見れば明らかだが、

以下は成り立つ

\bot \sqsubseteq 1

\bot \sqsubseteq 2

1 \sqsubseteq 1

以下は成り立たない

1 \sqsubseteq 2

2 \sqsubseteq 1

Just や Either みたいに引数を持つ型の場合は？ ref

正格か非正格かで、平坦領域になるかどうか変わる

正格なら平坦領域になる

非正格なら平坦にはならない

参考