部分関数の半順序集合
集合\mathrm{Fun}(S,T)
部分関数なので、出力が未定義になることもある
関数f\in\mathrm{Fun}(S,T)について見ている
fの定義域\mathrm{dom}(f)内の元を引数に取ると、f(x)\in Tとなる
しかし、定義域に入っていないyの場合は、出力が未定義になる
\mathrm{dom}(f)=Sのこともある
この場合は、普通にSからTの全域関数となる
この集合に、半順序を定義する
f,g\in\mathrm{Fun}(S,T)に対して、
f\sqsubseteq g \Leftrightarrow\forall x\in S\;(f(x)が定義されていればg(x)も定義されf(x)=g(x))
つまり、
\forall x\in\mathrm{dom}(f)に対しては、f(x)=g(x)であり、
かつ、\mathrm{dom}(f) \sube\mathrm{dom}(g)となっている
どちらも部分関数ではあるが、gの方が定義域が大きい
部分関数における意味近似順序を定義している
極大元
SからTへの全域関数
最小限
\mathrm{dom}(\bot)=\emptysetになるような関数\bot
何も定義されていない
\bot(x)=\bot
右辺は値の\bot
cpoである
例えば、こんな関数は定義できない
hsg :: Int -> Int
g undefined = 1
g _ = undefiend単調性に違反している
\mathrm{undefined} \sqsubseteq n \nRightarrow 1 \sqsubseteq \mathrm{undefined}
これはありうる
hsg :: Int -> Int
g undefined = 1
g _ = 1\mathrm{undefined} \sqsubseteq n \Rightarrow 1\sqsubseteq 1
例えば、
g = const 1 とか関数の具体例
これは\mathrm{Fun}(\mathbb{N},\mathbb{N})という半順序集合の1つの部分関数
参考