偏序集上的单调映射

保持次序的映射 ​

设 $(P,{\le }_P)$ 与 $(Q,{\le }_Q)$ 是偏序集公理库偏序Partial order · Partially ordered set满足自反、反对称和传递性的关系。，函数公理库函数Function · Map · Mapping由定义域、陪域和单值图共同组成，并把每个输入送到唯一输出的映射。 $f:P\to Q$ 称为单调映射、保序映射或 isotone map，若

$$\mathrm{\forall }x,y\in P,x{\le }_{P}y⟹f(x){\le }_{Q}f(y).$$

定义中的两个次序可能不同，因此写证明时不能把下标无声省去。条件只要求可比较元素的像保持方向；若 $x$ 与 $y$ 在 $P$ 中不可比，单调性不要求 $f(x)$ 与 $f(y)$ 在 $Q$ 中可比。

当定义域和值域相同，$F:P\to P$ 常称为单调算子。满足 $F(x)=x$ 的元素是不动点；满足 $F(x)\le x$ 的是前不动点，满足 $x\le F(x)$ 的是后不动点。三类对象不能混称，因为许多最小不动点公式先在所有前不动点中取下确界，再证明所得元素确实为不动点。

与更强性质的区别 ​

单调不等于严格单调。严格单调要求 $x{<}_{P}y$ 时 $f(x){<}_{Q}f(y)$；常值映射保持非严格次序，却显然不严格。单调映射也不必反映次序：从任意偏序到单点偏序的映射都是单调的，但它把全部差异压成同一个像。

若 $f$ 既保序又满足

$$f(x){\le }_{Q}f(y)⟹x{\le }_{P}y,$$

则它反映次序；单射且同时保序、反映次序的映射才是序嵌入。双射的单调映射也未必自动成为序同构，逆映射是否保序仍需检查。

单调性还不同于分析中的连续性。在实数通常次序上，阶跃函数可以单调却在跳点不连续；常值函数连续且单调，但 $x\mapsto x^2$ 在整条实线上连续却不单调。Scott 连续公理库DCPO 与 Scott 连续Directed-complete partial order · DCPO · Scott-continuous function以有向近似的上确界及保持这种极限的映射描述逐步增长的信息。要求保存有向上确界，是比单调更强、专门服务信息逼近极限的条件。

幂集上的可达性算子 ​

给定状态集合 $S$、初始集合 $I\subseteq S$ 与一步关系 $\to$，在幂集 $(\mathcal{P}(S),\subseteq )$ 上定义

$$F(X)=I\cup \mathrm{post}(X),\mathrm{post}(X)=\{s^{\prime }\in S:\mathrm{\exists }s\in X,s\to s^{\prime }\}.$$

若 $X\subseteq Y$，每个从 $X$ 中状态出发的一步后继也从 $Y$ 中状态出发，所以 $\mathrm{post}(X)\subseteq \mathrm{post}(Y)$，进而 $F(X)\subseteq F(Y)$。这是一份完整的单调性证明：先任取较小集合中的像元素，再用包含关系把同一个见证搬到较大集合。

从 $X_0=\varnothing$ 开始迭代，得到

$$X_1=I,X_2=I\cup \mathrm{post}(I),X_3=I\cup \mathrm{post}(I)\cup {\mathrm{post}}^2(I),\dots$$

每一步都不小于前一步，有限状态空间中最终会稳定在全部可达状态。这里的增长来自 $F$ 的具体形式与初值；“$F$ 单调”本身并不保证任意轨道 $x,F(x),F^2(x),\dots$ 都递增，还需先有 $x\le F(x)$。

组合、点态次序与反例 ​

单调映射的复合仍单调。若 $f:P\to Q$、$g:Q\to R$ 都保序，则 $x{\le }_{P}y$ 依次推出 $f(x){\le }_{Q}f(y)$ 与 $g(f(x)){\le }_{R}g(f(y))$。这使复杂转移函数可以由局部保序部件组合，而无需重新逐点证明整体方向。

函数集合 $Q^P$ 若按点态次序

$$f⪯g⟺\mathrm{\forall }x\in P,f(x){\le }_{Q}g(x)$$

排序，就能比较两个分析器或变换器谁给出的结果更小。点态比较不是按函数值总和、运行时间或语法长度排序，量词覆盖定义域中的每个输入。

一个常见失败是把“对若干样本保持大小”当作全称证明。例如 $h(x)=x^2$ 在 $0,1,2$ 上递增，却在 $-2<-1$ 时给出 $4>1$，因此不是 $\mathbb{R}$ 上的单调映射。另一种错误是把 antitone 映射也叫单调：集合补运算满足 $A\subseteq B\Rightarrow B^c\subseteq A^c$，它反转而非保持次序。

不动点理论中的作用 ​

单调算子把“输入信息增加时，结论不能倒退”形式化，是完备格公理库完备格Complete lattice · Complete ordered lattice任意子集都具有上确界和下确界，从而包含顶元、底元并支持任意族合流的格。、数据流方程和抽象语义的共同接口。Knaster–Tarski 不动点定理只要求完备格上的单调自映射，不要求距离、导数或压缩常数。

这也说明单调与收敛速度是两件事。单调性允许按次序比较迭代结果，却不承诺有限步稳定，更不承诺唯一不动点；在无限升链上，迭代可能持续增长，静态分析因而还需要 widening 等终止机制。

参考资料

• B. A. Davey and H. A. Priestley, Introduction to Lattices and Order, 2nd ed., Cambridge University Press, 2002, §§1.4, 2.1。
• Garrett Birkhoff, Lattice Theory, 3rd ed., American Mathematical Society, 1967, Ch. I。
• Alfred Tarski, “A Lattice-Theoretical Fixpoint Theorem and Its Applications,” Pacific Journal of Mathematics 5(2), 1955, pp. 285–309。