状態遷移・不変量・単調量

集合 $X$（状態の全体）と、$X$ 上の二項関係 $x\to x'$（1 回の操作で $x$ から $x'$ に移れる）を考える。有限回の操作で $x$ から $x'$ に移れること（$n\ge0$ 回の連鎖 $x=x_0\to x_1\to\cdots\to x_n=x'$ があること）を $x\to^*x'$ と書き、$x'$ は $x$ から到達可能という。関数 $I:X\to Y$ が不変量であるとは、$x\to x'$ ならば $I(x)=I(x')$ であることをいう。関数 $V:X\to\mathbb{N}_0$ が単調量であるとは、$x\to x'$ ならば $V(x')<V(x)$ であることをいう。