通常の0引数の型に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の話をしている時は、普通⊥を無視すると思う
この集合は
つまり記号のイメージとしての$ \sqsubsetのようなものが、$ \botとの関係にしかないmrsekut.icon
$ \bot \sqsubset aか
$ a=bにしかならない
$ \bot以外が並列にある感じ
自然数の通常の大小関係$ \leも定義されてはいるが、$ \sqsubseteqとは無関係である
意味近似順序の観点で見れば、$ 1と$ 2の定義のされ具合は同じである そう書くと、$ 1\sqsubseteq2と書けてしまいそうなので、言い方がちょっと良くないなmrsekut.icon
例えば、Intに$ \botを加えた集合$ \mathrm{Int}_\botを意味近似順序($ \sqsubseteq)で順序付けした時 ハッセ図式は、以下のようになる
https://gyazo.com/f27b7f4cee6a78a5fd8412f86c3382df
図を見れば明らかだが、
以下は成り立つ
$ \bot \sqsubseteq 1
$ \bot \sqsubseteq 2
$ 1 \sqsubseteq 1
以下は成り立たない
$ 1 \sqsubseteq 2
$ 2 \sqsubseteq 1
JustやEitherみたいに引数を持つ型の場合は？ ref 正格か非正格かで、平坦領域になるかどうか変わる
正格なら平坦領域になる
https://gyazo.com/c50512fe8f2ee57887347e9389029a5f
非正格なら平坦にはならない
https://gyazo.com/9405855bd6da5202de1dd5dfff25fb97
参考