示例#

1. $(\mathbb{Z}, \le)$
2. $(\mathscr{P}(x), \subseteq)$，其中 $\mathscr{P}$ 表示幂集
3. $(\mathbb{Z}^2, \sqsubseteq)$，其中，$(a, b) \sqsubseteq (a', b') \Leftrightarrow a \ge a' \land b \ge b'$

  前面提到，偏序集中并非所有元素都能够比较关系，如 $(\mathscr{P}(\{1, 2\}), \subseteq)$ 中的元素 $\{1\}$ 和 $\{2\}$ 之间就不能进行比较。示例3表示了区间包含关系。

示例#

1. 整数 $(\mathbb{Z}, \le, max, min)$

2. 整数区间 $(\{[a, b] | a, b \in \mathbb{Z}, a \le b\} \cup {0}, \subseteq, \sqcup, \sqcap)$，其中：

   $$[a, b] \sqcup [a', b'] \stackrel{\text{def}}{=} [\min(a, a'), \max(b, b')]$$ $$[a, b] \sqcap [a', b'] \stackrel{\text{def}}{=} [\max(a, a'), \min(b, b')], \text{ or } \emptyset \text{ if } \max(a, a') > \min(b, b')$$

如，整数区间 $(\{[a, b] | a, b \in \{0, 1, 2\}, a \le b\} \cup {0}, \subseteq, \sqcup, \sqcap)$，其中每条边表示偏序关系。

示例#

1. 幂集 $(\mathscr{P}(S), \subseteq, \cup, \cap, \empty, S)$   如 $(\mathscr{P}\{0, 1, 2\}, \subseteq, \cup, \cap, \empty, \{0, 1, 2\})$：

  其中，对于子集 $\{\{1\}, \{2\}, \{0, 1\}\}$，其最小上界为 $\{0, 1, 2\}$，最大下界为 $\empty$。

2. 带无穷界的整数区间

递增链#

IMPORTANT

  设序列 $(d_i)_{i \in \mathbb{N}}$ 是链，如果对于 $\forall i \in \mathbb{N}$ 都有：$d_i \sqsubseteq d_{i+1}$，则称该链为递增链。

递增链条件（$\mathrm{Ascending\ Chain\ Condition, ACC}$）#

IMPORTANT

  设偏序集 $(D, \sqsubseteq)$，如果对其中的任意递增链 $d_0 \sqsubseteq d_1 \sqsubseteq ...$ 最终都会稳定（即 $\exist n \in \mathbb{N}$ 使得对所有 $m > n$，有 $a_m = a_n$），则称 $D$ 满足递增链条件。

TIP

  这里只要求 $(D, \sqsubseteq)$ 满足偏序集，因此该偏序集中可以没有任何递增链，甚至可以不存在任何链。

  有穷高度的链肯定满足递增链条件$ACC$，但是满足递增链条件的链不一定是有穷高度（比如有可能存在不稳定的递减链）。

TIP

  链 $C$ 的高度定义为：链 $C$ 中存在的最长严格递增链，则该最长严格递增链的长度称为链 $C$ 的高度，记作 $\mathrm{ht}(C)$。

  其中，严格递增链是在递增链定义的基础上要求 $d_i \sqsubset d_{i+1}$，即要求 $d_i \not = d_{i+1}$。

  因此，对于递增链在趋于稳定后，后半段是稳定值 $a_m$ 的无限重复，并未构成严格递增链关系，此时该链的高度也并非无穷。

IMPORTANT

  完全格且满足递增链条件是不动点迭代终止的充分条件！

示例#

1. $(\mathbb{N}, \sqsubseteq)$

  不是 $\mathrm{CPO}$，$\mathrm{N}$ 本身构成链，其最小上界为 $\infin$，但是 $\infin \not \in \mathrm{N}$；

2. $(\mathbb{N} \cup \{\infin\}, \sqsubseteq)$

  是 $\mathrm{CPO}$。

单调性#

IMPORTANT

  设偏序集 $(D, \sqsubseteq)$ 和 $(D', \sqsubseteq')$ 上的全函数 $f: D \rightarrow D'$，若 $\forall x, y \in D$，且只要 $x \sqsubseteq y$ 则有 $f(x) \sqsubseteq' f(y)$，则该全函数 $f$ 是单调的。

  这里的偏序集 $(D, \sqsubseteq)$ 和 $(D', \sqsubseteq')$ 可以理解成定义域和值域。需要注意的是，$f(x) \sqsubseteq' f(y)$ 中 $\sqsubseteq$ 需要映射到 $\sqsubseteq'$。若 $D$ 中存在链 $s$，单调性确保了该链经函数 $f$ 映射到 $D'$ 后构成新链 $s'$（根据单调性定义很容易证明）。

上确界连续（$\sqcup-$连续）#

IMPORTANT

定义一：   设 $(D, \sqsubseteq)$ 和 $(D', \sqsubseteq')$ 是完全偏序（$\mathrm{CPO}$），存在全函数 $f: D \rightarrow D'$，若对 $D$ 中的每条链 $s$，$\sqcup f(s)$ 存在且有 $f(\sqcup s) = \sqcup f(s)$，则称 $f$ 是 $\sqcup-$连续（上确界连续）的

  上面的定义中其实隐含了函数单调性：$\forall x, y \in D$ 且 $x \sqsubseteq y$，则 $x,y$ 在同一条链 $\{x, y\}$上，而根据定义 $f(y) = f(\sqcup \{x, y\}) = \sqcup f(\{x, y\}) = \sqcup \{f(x), f(y)\}$，而 $f(x) \sqsubseteq' \sqcup \{f(x), f(y)\}$，从而 $f(x) \sqsubseteq' f(y)$，故得证函数 $f$ 是单调的。

  函数 $f$ 单调性保证了 $D$ 中的链 $s$ 经函数 $f$ 映射到 $(D', \sqsubseteq')$ 后仍然构成链 $s'$。于是上面的定义可以理解为：对 $D$ 中的任意一条链 $s$，$f$ 作用在链 $s$ 的最小上界（上确界）上的结果，等于 $f$ 作用在链 $s$ 中的每个元素构成的新链 $s' = f(s)$ 的最小上界（上确界），也即 $f(\sqcup s) = \sqcup f(s)$。

IMPORTANT

定义二：   函数 $f$ 是 $\sqcup-$连续的，当且仅当 $f$ 是单调的且对 $D$ 中的每条链 $s$，有 $f(\sqcup s) \sqsubseteq' \sqcup f(s)$。

  这里和定义一相对比，条件给出函数 $f$ 是单调的，并且 $f(\sqcup s) \sqsubseteq' \sqcup f(s)$，因此实际上我们只需要基于函数 $f$ 的单调性证明 $\sqcup f(s) \sqsubseteq' f(\sqcup s)$ 即可得到定义一中的条件，也就能够证明函数 $f$ 是 $\sqcup-$连续。

  证明如下：$\forall x \in s$，有 $x \sqsubseteq \sqcup s$，于是 $f(x) \sqsubseteq' f(\sqcup s)$，即对链 $s$ 中任意元素 $x$ 映射到 $D'$ 中都有上界 $f(\sqcup s)$，于是 $\sqcup f(s) = \sqcup \{f(x_1), ..., f(x_k)\} \sqsubseteq' f(\sqcup s)$。根据条件 $f(\sqcup s) \sqsubseteq' \sqcup f(s)$，于是有

  再根据定义一，可知函数 $f$ 是 $\sqcup-$连续的。

TIP

  若 $D$ 只包含有穷链，则 $f$ 是 $\sqcup-$ 连续的当且仅当 $f$ 是单调的。

  提示一下，既然是有穷链，则 $\sqcup s \in s$，而根据单调性即可证明 $\sqcup f(s) = f(\sqcup s)$。

示例#

  考虑从 $(\mathbb{N}\cup \{\infin\}, \le)$ 到 $(\{F, T\}, \sqsubseteq)$ 的函数 $f(x)$，其中 $F \sqsubseteq T$，判断函数 $f(x)$ 单调性与 $\sqcup-$连续性：

1. $f(x): \mathrm{if\ x\ge 2\ then\ T\ else\ F}$
2. $f(x): \mathrm{if\ x == \infin\ then\ T\ else\ F}$

  显然，两者中的 $f(x)$ 均单调。但是 2.中 $f(x)$ 不是 $\sqcup-$连续的，理由如下：

  根据定义，$\mathbb{N}\cup \{\infin\}$ 中任意链 $s$ 均有，$\sqcup f(s)$ 存在且有 $f(\sqcup s) = \sqcup f(s)$ ，而对于2.中的 $f(x)$，不妨取 $s = \mathbb{N}$，由于 $\infin \not \in \mathbb{N}$，于是 $\sqcup f(s) = F \sqsubseteq T = f(\sqcup s)$，故得证。

基础概念#

IMPORTANT

  设 $f$ 是偏序集$(D, \sqsubseteq)$ 上的函数，则 $D$ 中元素 $x$ 称为函数 $f$ 的：

1. 不动点（$\mathrm{fixpoint}$）：若 $\color{red}{\mathrm{f(x) = x}}$；
2. 前不动点（$\mathrm{pre-fixpoint}$）：若 $\color{red}{\mathrm{x \sqsubseteq f(x)}}$；
3. 后不动点（$\mathrm{post-fixpoint}$）：若 $\color{red}{\mathrm{f(x) \sqsubseteq x}}$.

  图中的 $pre$ 和 $post$ 都是相对于不动点 $x_0$，实际上 $post$ 所指部分相对于 $x_1$ 也是前不动点。

IMPORTANT

  不动点集合 $\mathrm{fp}\ f = \{x \in D: f(x) = x\}$；

  $x \in \mathrm{fp}\ f$，若对任意 $y \in \mathrm{fp}\ f$ 皆有 $x \sqsubseteq y$，则称 $x$ 为函数 $f$ 的最小不动点，记作 $\mathrm{lfp}\ f$；

  $x \in \mathrm{fp}\ f$，若对任意 $y \in \mathrm{fp}\ f$ 皆有 $y \sqsubseteq x$，则称 $x$ 为函数 $f$ 的最大不动点，记作 $\mathrm{gfp}\ f$；

  记 $\mathrm{lfp}_d\ f$ 为关于偏序 $\sqsubseteq$ 比 $d$ 大的最小不动点；

  记 $\mathrm{gfp}_d\ f$ 为关于偏序 $\sqsubseteq$ 比 $d$ 小的最大不动点；

应用示例#

  以不动点理论在联立递归方程求解中的应用为例：

1. 问题背景：联立递归方程

  考虑由两个递归方程组成的方程组：

  其中，$x_1, x_2$ 是格 $x$ 中的元素；$f, g$ 是定义在该格上的函数。

2. 转化为不动点问题

  为求解上述方程组，我们可以将其抽象为一个函数的不动点问题：

  定义函数 $F: X \times X \rightarrow X \times X$，其中 $X \times X$ 表示原格的 “乘积格”，保持偏序结构，函数 $F$ 形式为：

  此时，方程组的解 $(x_1, x_2)$ 满足:

  即 $(x_1, x_2)$ 是函数 $F$ 的不动点，于是原方程组最小解为 $\mathrm{lfp}\ F$。

$\mathrm{Tarski}$ 不动点定理#

IMPORTANT

  完全格$(D, \sqsubseteq, \sqcup, \sqcap, \bot, \top)$ 上的单调函数 $f: D \rightarrow D$ 的不动点集合 $\mathrm{fp}$ 构成一个非空完全格，且：

$$\begin{align*} & \mathrm{lfp}\ f = \sqcap \mathrm{postfp}\ f = \sqcap \{x \in D: f(x) \sqsubseteq x\} \\ & \mathrm{gfp}\ f = \sqcup \mathrm{prefp}\ f = \sqcup \{x \in D: f(x) \sqsupseteq x\} \\ \end{align*}$$

  其中，由不动点构成的非空完全格为 $(\text{fp } f, \sqsubseteq, \lambda S.\text{lfp}_{\sqcup S}, \lambda S.\text{gfp}_{\sqcap S}, \text{lfp } f, \text{gfp } f)$，其中 $\lambda S$ 构造一个以 “集合 $S$” 为输入、以 “对应的不动点” 为输出的函数，于是 $\lambda S.\text{lfp}_{\sqcup S}$ 表示对应的最小不动点，$\lambda S.\text{gfp}_{\sqcap S}$ 表示对应的最大不动点。

TIP

  $\mathrm{Tarski}$ 不动点定理证明了不动点存在性，但并未给出求解不动点的方法。

$\mathrm{Kleene}$ 不动点定理#

IMPORTANT

  设 $(D, \sqsubseteq)$ 为完全偏序 $CPO$，若函数 $f: D \rightarrow D$ 是 $\sqcup-$连续的，则有：

$$\mathrm{lfp}\ f = \sqcup \{f^i(\bot)| i \in \mathbb{N}\}$$

  其中，$i \in \mathbb{N}$ 表示迭代次数。

TIP

  $\mathrm{Kleene}$ 不动点定理给出了实际求解不动点的方法：从 $CPO$ 的 $\bot$ 开始，反复应用函数 $f$ 进行迭代来构造序列：$\bot, f(\bot), f(f(\bot)), ..., f^n(\bot)$，该序列的”最小上确界”就是函数 $f$ 的最小不动点。

满足递增链条件的完全偏序 $CPO$ 上的不动点迭代#

  $\mathrm{Kleene}$ 不动点定理并未要求迭代过程必须在有限步内终止，其核心实际上是通过无穷迭代的极限来定义不动点，而这种极限在多数情况下无法通过实际计算抵达。于是需要更加严格条件来保证不动点迭代的终止性。

IMPORTANT

  若 $CPO(D, \sqsubseteq, \sqcup, \bot)$ 上没有无穷递增链，$f$ 是 $D$ 上的单调函数，那么 $\mathrm{Kleene}$ 迭代序列 $a_{i+1} = f(a_i)$ 将会在有穷时间内收敛于 $\mathrm{lfp}_\bot \ f$。

TIP

  有穷高度的链肯定满足递增链条件$ACC$，但是满足递增链条件的链不一定是有穷高度（比如有可能存在不稳定的递减链）。

  而对 $CPO$ 而言存在最小元 $\bot$，于是满足递增链条件的 $CPO$ 一定没有无穷递增链。

  在一些问题上，如：

• 有穷格：即格中元素个数是有穷的，如符号格；
• 满足递增链条件的无穷格：即格中元素个数是无穷的，但是格的高度是有穷的，如常量格.

  上述定理提供了迭代方法来精确地计算最小不动点，并且保证了迭代计算的终止性。

数据流方程组（$\mathrm{dataflow\ equation\ system}$）#

  给定数据流系统 $\mathcal{S} = (Lab, E, F, (D, \sqsubseteq), \iota, \varphi)$，其中 $Lab = \{1, \dots, n\}$（不失一般性）

• $\mathcal{S}$ 确定方程组（其中 $l \in Lab$）：

  $$\text{Al}_l = \begin{cases} \iota & if\ l \in E \\ \bigsqcup \{\varphi_{l'}(\text{Al}_{l'}) \mid (l', l) \in F\} & otherwise \end{cases}$$

• $(d_1, \dots, d_n) \in D^n$ 被称为解，若：

  $$d_l = \begin{cases} \iota & if\ l \in E \\ \bigsqcup \{\varphi_{l'}(d_{l'}) \mid (l', l) \in F\} & otherwise \end{cases}$$

• $\mathcal{S}$ 确定变换：

  $$\Phi_{\mathcal{S}}: D^n \rightarrow D^n: (d_1, \dots, d_n) \rightarrow (d_1', \dots, d_n')$$

  其中

  $$d_l' := \begin{cases} \iota & if\ l \in E \\ \bigsqcup \{\varphi_{l'}(d_{l'}) \mid (l', l) \in F\} & otherwise \end{cases}$$

  $(d_1, \dots, d_n) \in D^n$求解该方程组当且仅当它是 $\Phi_{\mathcal{S}}$ 的不动点。

要点分析#

• $(D, \sqsubseteq)$ 是完全格，确保 $\Phi_S$ 良定义。
• 由于 $(D, \sqsubseteq)$ 是满足 $ACC$ 的完全格，因此 $(D^n, \sqsubseteq^n)$ 也是完全格（其中 $(d_1, \dots, d_n) \sqsubseteq^n (d_1', \dots, d_n')$ 当且仅当对所有 $1 \leq i \leq n$，有 $d_i \sqsubseteq d_i'$）。
• 传递函数 $\varphi_l$ 在 $(D, \sqsubseteq)$ 中的单调性，蕴含 $\Phi_S$ 在 $(D^n, \sqsubseteq^n)$ 中的单调性（因为上确界算子 $\bigsqcup$ 也具有单调性）。
• 因此，（最小）不动点可通过迭代有效计算： $$\text{fix}(\Phi_S) = \bigsqcup \{\Phi_S^k(\bot_{D^n}) \mid k \in \mathbb{N}\}$$ 其中 $\bot_{D^n} = \underbrace{(\bot_D, \dots, \bot_D)}_{n \text{ 次}}$。
• 若 $(D, \sqsubseteq)$ 的高度为 $m$ $\implies (D^n, \sqsubseteq^n)$ 的高度为 $m \cdot n$ $\implies$ 不动点迭代最多需要 $m \cdot n$ 步。