从不动点定理到编程语言

偏序关系

集合上的偏序关系满足如下条件。对任意、、，
- （自反性） $x \leq x$
- （反对称性）如果 $x \leq y$ ， $y \leq x$ ，那么 $x = y$
- （传递性）如果 $x \leq y$ ， $y \leq z$ ，那么 $x \leq z$
设为序列，为映射
- 如果 $x_1 \leq x_2 \leq \cdots$ ，那么 $\{ x_i \}$ 称为递增序列
- 如果对任意 $x \leq y$ ，我们有 $f(x) \leq f(y)$ ，那么 $f$ 称为递增映射
设为递增序列，为递增映射
- 如果 $l$ 为 $\{ x_i \}$ 的最小上界，那么它称为 $\{ x_i \}$ 的极限，记为 $l = \lim_{i \to \infty} x_i$
- 如果对任意递增序列 $\{ x_i \}$ ，我们有 $f(\lim_{i \to \infty} x_i) = \lim_{i \to \infty} f(x_i)$ ，那么 $f$ 称为连续映射
注意，在连续映射的定义中，未必每个递增序列都有极限。如果每个递增序列都有最小上界，那么 $(X, \leq)$ 称为弱完备空间，连续映射需要定义在弱完备空间中
进一步，如果每个子集 $A \subset X$ 都有最小上界（记为 $\sup A$ ，称为上确界），那么 $(X, \leq)$ 称为强完备空间。强完备空间是弱完备空间，原因是递增序列是子集
强完备空间的每个子集都有最大下界（记为，称为下确界）
- 设
  $B = \{ y \in X : y \leq x \text{ for any } x \in A \}$
  为 $A$ 的下界构成的集合。由 $(X, \leq)$ 的强完备性，可取 $l = \sup B$
- 对任意 $x \in A$ ， $x$ 为 $B$ 的上界。由上确界的最小性，可得 $l \leq x$ 。也就是说， $l$ 为 $A$ 的下界
- 如果 $l'$ 为 $A$ 的另一个下界，那么 $l' \in B$ 。由上确界是上界，可得 $l' \leq l$
设 $A$ 为集合， $\mathscr{P}(A)$ 为 $A$ 的幂集， $\subset$ 为“包含”关系。 $(\mathscr{P}(A), \subset)$ 是弱完备的，原因是每个递增序列 $X_1 \subset X_2 \subset \cdots$ 都有极限 $\cup_{i \geq 1} X_i$
进一步， $(\mathscr{P}(A), \subset)$ 是强完备的，原因是每个子集 $\mathscr{A} \subset \mathscr{P}(A)$ 都有最小上界 $\cup_{X \in \mathscr{A}} X$

不动点定理

（第一不动点定理）设为弱完备空间。如果连续，并且有最小元素，那么如下的迭代方法给出了的最小不动点
$p = \lim_{i \to \infty} f^i(m).$
- 为不动点：
  - 因为 $m$ 为最小元素， $f$ 递增，所以
    $m \leq f(m) \leq \cdots$
    由 $(X, \leq)$ 的弱完备性，递增序列 $\{ f^i(m) \}$ 有极限 $p = \lim_{i \to \infty} f^i(m)$
  - 由于 $f$ 连续，故
    $f(p) = f(\lim_{i \to \infty} f^i(m)) = \lim_{i \to \infty} f^{i + 1}(m) = p.$
- 为最小不动点：
  - 如果 $q$ 为另一个不动点，那么 $f(q) = q$ ，并且
    $m \leq q,\; f(m) \leq f(q) = q,\; \ldots$
    也就是说， $q$ 为 $\{ f^i(m) \}$ 的上界。由极限的最小性，可得 $p \leq q$
（第二不动点定理）设为强完备空间。如果递增，那么如下的下确界方法给出了的最小不动点
$p = \inf A, \text{ where } A = \{ x \in X : f(x) \leq x \}.$
- ：
  - 对任意 $x \in A$ ，由于 $f$ 递增，故
    $p \leq x \Rightarrow f(p) \leq f(x) \leq x.$
    也就是说， $f(p)$ 为 $A$ 的一个下界。由下确界的最大性，可得 $f(p) \leq p$
- ：
  - 由于 $f$ 递增，故 $f(f(p)) \leq f(p)$ 。也就是说， $f(p) \in A$ 。由下确界是下界，可得 $p \leq f(p)$
- 为最小不动点：
  - 如果 $q$ 为另一个不动点，那么 $q \in A$ 。由下确界是下界，可得 $p \leq q$

从不动点定理到编程语言

编程语言源于归纳定义，归纳定义源于不动点定理
归纳定义
- 设 $A$ 为集合， $f: A^n \to A$ 为映射。如果子集 $C \subset A$ 满足
  $x_1, \ldots, x_n \in C \Rightarrow f(x_1, \ldots, x_n) \in C,$
  那么 $C$ 称为在 $f$ 下封闭
- 进一步，如果 $C \subset A$ 是在 $f_i: A^{n_i} \to A$ ， $i \geq 1$ 下封闭的最小子集，那么 $C$ 由 $f_i$ 归纳定义
归纳定义的存在性
- 定义
  $F: \mathscr{P}(A) \to \mathscr{P}(A),\; F(X) = \cup_{i \geq 1} f_i(X^{n_i}).$
  那么 $X$ 在 $f_i$ ， $i \geq 1$ 下封闭当且仅当 $F(X) \subset X$
- 由上面的笔记， $(\mathscr{P}(A), \subset)$ 是强完备的。进一步， $F$ 递增。因此，我们可以使用第二不动点定理，得到 $F$ 的最小不动点 $C$
  注意， $C$ 也是在 $f_i: A^{n_i} \to A$ ， $i \geq 1$ 下封闭的最小子集，原因是
  $C = \inf \mathscr{A}, \text{ where } \mathscr{A} = \{ X \in \mathscr{P}(A) : F(X) \subset X \}.$
- 我们也可以使用第一不动点定理。注意到 $\mathscr{P}(A)$ 有最小元素 $\emptyset$ ，并且 $F$ 连续，
  $F(\cup_{j \geq 1} X_j) = \cup_{i, j \geq 1} f_i(X_j^{n_i}) = \cup_{j \geq 1} F(X_j).$
  因此，
  $C = \lim_{i \to \infty} F^i(\emptyset) = \cup_{i \geq 1} F^i(\emptyset).$
  为了得到 $C \neq \emptyset$ ，某些 $f_i$ 必须将空集 $\emptyset = A^0$ 映射到非空集
归纳定义的第一个作用是定义递归结构，比如设 $A$ 为 $a$ 、 $b$ 、 $c$ 的字符串构成的集合。那么， $\{ a^nbc^n : n \geq 0 \}$ 的归纳定义为
$f_1: \emptyset \to A,\; \mapsto b.\quad f_2: A \to A,\; t \mapsto atc.$
如果我们将 $a$ 视为左括号、将 $c$ 视为右括号，那么上面定义了一种嵌套括号的语言
归纳定义的第二个作用是对递归结构进行证明。在数理逻辑和计算机科学中， $f_i: (x_1, \ldots, x_{n_i}) \mapsto t$ 称为推理规则，记为
$\dfrac{x_1 \ldots x_{n_i}}{t}$
这里， $x_1 \ldots x_{n_i}$ 为前提， $t$ 为结论。没有前提的推理规则称为公理。比如 $\{ a^nbc^n : n \geq 0 \}$ 的推理规则为
$\dfrac{}{b} \quad \dfrac{t}{atc}$
首先，我们可以利用推理规则证明 $x \in C$ 。注意， $x \in C = \cup_{i \geq 1} F^i(\emptyset)$ 等价于 $x \in F^i(\emptyset)$ 对某个 $i \geq 1$ 成立，所以我们只需构造一个从公理出发的、有限的推理规则链，比如
$\dfrac{}{\dfrac{b}{\dfrac{abc}{aabcc}}}$
在一般情况下，这会构成一棵树，称为演绎树
其次，我们可以对推理规则使用结构归纳法。如果具有性质可以推出具有性质，，那么整个也具有性质
- 令 $P = \{ x \in A : x \text{ has property }\mathcal{P} \}$
- $F^0(\emptyset) = \emptyset \subset P$ 。如果 $F^k(\emptyset) \subset P$ ，那么对任意 $x_1, \ldots x_{n_i} \in F^k(\emptyset) \subset P$ ，由条件可知， $f_i(x_1, \ldots x_{n_i}) \in P$ ， $i \geq 1$ 。因此，
  $F^{k + 1}(\emptyset) = \cup_{i \geq 1} f_i(F^k(\emptyset)^{n_i}) \subset P.$
  由数学归纳法， $F^k(\emptyset) \subset P$ , $k \geq 0$ ，故
  $C = \cup_{i \geq 1} F^i(\emptyset) \subset P.$
结构归纳法是数学归纳法的一种推广形式，原因是数学归纳法是如下推理规则的结构归纳法
$\dfrac{}{0} \quad \dfrac{n}{n + 1}$