Intro
有种前菜只是刚刚上完的感觉。
递归数据结构是非常常见的结构，给递归数据结构赋予的类型通常会是一个递归的类型。
经典的例如
data IntList
= Nil
| Cons Int IntList当然这里还没有讲到参数化类型，因此这里 List 作为“容器”的概念，其内容类型的区分是通过名字完成的。
为了避免这样自引用的情况（类似于 ULC 中定义递归的方式），引入算子 \(\mu\)。那么上面的 haskell 类型定义就可以形式化地写成下面的样子 \[ \text{IntList=$\mu X.\left<\text{Nil}, \Set{\text{hd=Int, tl=}X}\right>$} \] 一个分析中的例子可以是这样的：给定函数 \(f\)，定义算子 \(\gamma\) 使得 \(\gamma f\) 为方程 \(f(x)=x\) 的解集。此处 \(\mu\) 的作用是类似的。
类比 \(\text{fix}\) combinator，这个 \(\mu\) 同样可以像剥洋葱一样一层层剥开类型并且不收敛。
Equivalence
书上讲有两种构造递归类型的方法，它们的区别在于对如下问题的回答不同：
递归类型本身和它剥开一层后的类型，二者关系如何？
这个“剥开”函数一般叫 \(\text{fold}\colon T\mapsto T\)
- equi-recursive approach 认为它们是同一个类型，在语境下可以等价替换，type checker 负责决定把具体的递归类型剥开到什么程度。
- iso-recursive approach 认为它们不同，但是是同构的。即 \(\text{unfold}\circ\text{fold}=id_T\)。同时代码需要显式地在需要剥开的地方写出 \(\text{fold}\) 和 \(\text{unfold}\)
Induction, Coinduction
定义
若 \(F:2^U\mapsto 2^U\) 满足 \(\forall X\subseteq Y, F(X)\subseteq F(Y)\)， 则称 \(F\) 是 \(U\) 上的单调函数
通常把这个（朴素意义的）集合 \(U\) 叫做 Universe，即我们所有可能讨论的所有元素组成的集合。
- 若 \(F(X)\subseteq X\)，则称 \(X\) 是 \(F\)-closed 的
- 若 \(X\subseteq F(X)\) ，则称 \(X\) 是 \(F\)-consistent 的
- 若 \(F(X)=X\)，则称 \(X\) 是 \(F\) 的不动点（fixed point）
可以发现 \(F\) 本质上是定义在格上的函数，并且这个格是由 \(\left<U,\subseteq\right>\) 导出的。
通常把 \(F\) 的最小不动点写成 \(\mu F\)，最大不动点写成 \(\nu F\)。
定理
Knaster-Tarski 定理的叙述如下：
- 所有 \(F\)-closed 集之交是 \(F\) 的最小不动点
- 所有 \(F\)-consistent 集之并是 \(F\) 的最大不动点
证一下①：
考虑 \(C=\Set{S\mid F(S)\subseteq S}\)，不妨记 \(M=\bigcap C\)，下面即证明 \(F(M)=M\) 且 \(\forall X\subseteq U, F(X)=X\Rightarrow M\subseteq X\)
注意到 \(\forall S\in C\) 都有 \(M\subseteq S\)，因此 \(\forall S\in C\) 都有 \(F(M)\subseteq F(S)\)，这说明 \(F(M)\subseteq \bigcap_{S\in C} F(S)\)
又由 \(C\) 的定义可知 \(F(M)\subseteq\bigcap_{S\in C} F(S)\subseteq \bigcap C=M\)，因此 \(F(M)\subseteq M\)；
另一侧由反证法，不妨假设存在 \(x\in M\) 使得 \(x\not\in F(M)\)，此时记 \(M'=F(M)\)，那么有 \(M'\subseteq M\)，根据单调性有 \(F(M')\subseteq F(M)=M'\)，因此 \(M'\in C\)，这说明 \(M=\bigcap C\subseteq M'=F(M)\)，矛盾；故假设不成立，即 \(M\subseteq F(M)\)
综上就有 \(M=F(M)\)，这说明 \(M=\bigcap C\) 是 \(F\) 的一个不动点，下面证明这是最小的不动点。
由反证法设存在更小不动点 \(M''\subsetneq M\)，则根据不动点定义有 \(M''\in C\)，这说明 \(M=\bigcap C\subseteq M''\subsetneq M\)，矛盾；故假设不成立，不存在更小的不动点了。
②的证明是对偶的。定理的另一种叙述如下：
- Principle of induction 若 \(X\) 是 \(F\)-closed 集，那么 \(\mu F\subseteq X\)
- Principle of coinduction 若 \(X\) 是 \(F\)-consistent 集，那么 \(X\subseteq\nu F\)
Subtyping
tnnd，卖了一个很大的关子就跑了，今天就到这吧。