プログラミング言語において、「小さい、等しい、大きい」を表す三値の比較関数を用いて、値同士の順序関係を自分で定義することがある。
たとえばJavaでは
Comparator
インターフェースのcompareメソッドを実装するが、このような関数が完全な前順序関係を特徴づけることを確認する。以下の性質はJavaのドキュメントを参考にした。
任意の集合$X$に対して、$f:X \times X \to \mathbf{N}$を以下の性質をもつ関数であるとする。
この関数$f$が$X$上の完全な前順序関係を特徴づける。すなわち、以下の条件を満たす二項関係$\preceq$を特徴づけることを示す。
$f: X \times X \to \mathbf{N}$を先の性質を満たす関数とする。$\preceq$を以下で定義する。
$$\begin{eqnarray}
x \preceq y \Leftrightarrow f(x,y) \leq 0\end{eqnarray}$$
反射律を示す。$f(x,x) = -f(x,x)$より$f(x,x) = 0$。したがって$x \preceq x$。
推移律を示す。$x \preceq y,\, y \preceq z$を仮定して$x \preceq z$を導く。仮定より$f(x,y)$および$f(y,z)$は$-1$または$0$である。いずれか片方が$0$の場合、たとえば$f(x,y) =0$の場合、$f(x,z) = f(y,z) \leq 0$より$x \leq z$である。$f(y,z)=0$の場合も同様。いずれも$-1$の場合は$f(z,y) >0,\, f(y,x) >0$より$f(z,x) >0$、すなわち$f(x,z) = -f(z,x) < 0$より$x \leq z$である。結局いずれの場合でも$x \preceq z$である。
完全性を示す。$f(x,y) \leq 0$または$f(x,y) > 0$である。$f(x,y) \leq 0$のとき、$x \preceq y$である。$f(x,y) > 0$のとき、$f(y,x) = -f(x,y) < 0$より$y \preceq x$である。以上より$x \preceq y$または$y \preceq x$である。
完全な前順序関係$\preceq$を用いて、関数$f: X \times X \to \mathbf{N}$を以下のように定義する。
$$\begin{eqnarray}
f(x,y) = \begin{cases}
-1 & x \preceq y,\, \neg (y \preceq x)\\
0 & x \preceq y,\, y \preceq x\\
1 & y \preceq x,\, \neg (x \preceq y)
\end{cases}\end{eqnarray}$$
$f(x,y)$が$-1,\, 0,\, 1$のいずれかであることは明らか。
$f(x,y)=-f(y,x)$も明らか。
$f(x,y) >0$と$f(y,z)>0$を仮定して$f(x,z) > 0$を導く。仮定より$y \preceq x,\, \neg (x \preceq y),\, z \preceq y$である。推移律より$z \preceq x$である。さらに$x \preceq z$を仮定すると推移律より$x \preceq y$が導かれ、これは$\neg (x \preceq y)$に矛盾するので仮定$x \preceq z$は否定される。以上より$f(x,z)=1>0$。
$f(x,y)=0$と仮定する。これは$x \preceq y,\, y \preceq x$を意味するので
$$\begin{eqnarray}
&x \preceq z
\Rightarrow y \preceq z\ (\because 推移律)\\
&y \preceq z
\Rightarrow x \preceq z\ (\because 推移律)\end{eqnarray}$$となり、$x \preceq z$と$y \preceq z$は同値。同様に$z \preceq x$と$z \preceq y$が同値になるから、$f(x,z)=f(y,z)$。
関数$f$から関係$\preceq$を定義し、それにもとづいて関数$f'$を定義すると$f=f'$である。
関係$\preceq \subseteq X \times X$から関数$f$を定義し、それにもとづいて関係$\preceq'$を定義すると$\preceq=\preceq'$である。
証明は省略する。