部分関数の半順序集合

集合$ \mathrm{Fun}(S,T)

集合$ Sから$ Tへの部分関数、の集合を$ \mathrm{Fun}(S,T)とする

部分関数なので、出力が未定義になることもある

https://gyazo.com/8aacf7bed85d7761e2f55dbdb1fb7a00

関数$ 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の方が定義域が大きい

部分関数における意味近似順序を定義しているmrsekut.icon

極大元

$ Sから$ Tへの全域関数

最小限

$ \mathrm{dom}(\bot)=\emptysetになるような関数$ \bot

何も定義されていない

$ \bot(x)=\bot

右辺は値の$ \botmrsekut.icon

cpoである

例えば、こんな関数は定義できない

code:hs

g :: Int -> Int

g undefined = 1

g _ = undefiend

単調性に違反している

$ \mathrm{undefined} \sqsubseteq n \nRightarrow 1 \sqsubseteq \mathrm{undefined}

これはありうる

code:hs

g :: 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つの部分関数

参考