她很丑，还可怜兮兮的。但她身上洋溢着爱。

# 子类型化

# 子类型

# 包含

• 考虑如下作用：

  $$(\lambda r:\{x:Nat\}.r.x)\{x=0,y=1\}$$

  按照严格的记录类型定义，这是个非法的表达式。因为传入的参数类型为：$\{x:Nat,y:Nat\}$。但我们可以发现，它里面已经有了我们所需的$\{x:Nat\}$ 部分，至于 y，我们 不关心。此时我们称传递类型为$\{x:Nat,y:Nat\}$ 的参数给希望得到参数类型为$\{x:Nat\}$ 的函数总是安全的。

子类型关系的类型规则：

$$\frac{\Gamma\vdash t:S\quad S<:T}{\Gamma\vdash t:T}$$

通过增加这条类型规则，来通过一些类型检查。

# 子类型关系 "<:"

• 子类型关系显然有传递和自反性。而且对于记录类型，显然有：

  $$\{l_i:T_i,i\in1..n+k\}<:\{l_i:T_i,i\in1..n\}$$

  此为广度子类型化。

  $$\frac{foreach\;i\quad S_i<:T_i}{\{l_i:S_i,i\in1..n\}<:\{l_i:T_1,i\in1..n\}}$$

  此为深度子类型化。

  $$\frac{\{k_j:S_j,j\in1..n\}是\{l_i:T_i,i\in1..n\}的一个置换}{\{k_j:S_j,j\in1..n\}<:\{l_i:T_i,i\in1..n\}}$$

  此为置换子类型化。

  $$\frac{T_1<:S_1\quad S_2<:T_2}{S_1\rightarrow S_2<:T_1\rightarrow T_2}$$

  此为高阶语言（允许函数作为参数传递）的子类型化。这个规则比较奇怪，首先考虑一个函数$f:S_1\rightarrow S_2$，它可以接受$S_1$ 的子类型$T_1$ 作为传入参数，它输出的$S_2$ 也可以作为$T_2$ 类型安全地使用。所以函数 f 可以替换$T_1\rightarrow T_2$ 类型的函数安全使用。

  $$S<:Top$$

  引入 Top 为超类型。$T::=...|Top$

# 子类型化和类型化的性质

• 引理 [逆转定理]

  若$S<:T_1\rightarrow T_2$，那么 S 一定为$S_1\rightarrow S_2$ 类型，其中$T_1<:S_1,S_2<:T_2$。

  若$S<:\{l_i:T_i,i\in1..n\}$，那么 S 一定为$\{k_j:S_j,j\in1..m\}$ 类型，且标签$\{l_i\}\subseteq\{k_i\}$，且公共部分$l_i:T_i,l_i:S_i$ 一定有$S_i<:T_i$

• 引理

  如果$\Gamma\vdash\lambda x:S_1.s_2:T_1\rightarrow T_2$，那么$T_1<:S_1$ 且$\Gamma,x:S_1\vdash s_2:T_2$。

  如果$\Gamma\vdash \{k_a=s_a,a\in1..m\}:\{l_i:T_i,i\in1..n\}$，那么$\{l_i\}\subseteq\{k_a\}$ 且对公共部分$\Gamma\vdash s_a:T_i$。

• 引理 [代换]

  如果$\Gamma,x:S\vdash t:T$ 且$\Gamma\vdash s:S$，那么$\Gamma\vdash[x\mapsto s]\;t:T$。

• 定理 [保持]

  如果$\Gamma\vdash t:T$ 且$t\rightarrow t'$，那么$\Gamma\vdash t':T$。

# Top 类型和 Bottom 类型

$$Bot<:T\\ error:Bot$$

显然把 error 设置成 Bot 就不错，它可以在任何上下文出现。但这样的类型很流氓，需要慎重。

# 子类型化及其他特征

# 归属（Ascription）和强制转型（Casting）

• 之前介绍过归属算子$t\;as\;T$。像 Java 和 C++ 这样具有子类型化的语言，强制转型往往有向上转型和向下转型。前者是直接进行的，而后者需要进一步扩展。

# 变式类型 & 列表类型

• 变式类型的子类型化规则完全类似于记录类型。

• List 的构造子是协变式，也就是：

  $$\frac{S<:T}{List\;S<:List\;T}$$

  其中$List\;T$ 表示一个有限长的，都是 T 类型的元素构成的列表。具体行为和规则可以谷歌。

# 引用

$$\frac{S<:T\quad T<:S}{Ref\;S<:Ref\;T}$$

由于引用类型需要同时支持读$!$ 和写$:=$ 的操作，它的子类型化将及其严格。因为需要读，所以需要$S<:T$，即读出来的都能当 T 用；因为需要写，所以要求$T<:S$。因此有：

$$\frac{S<:T\quad T<:S}{Array\;S<:Array\;T}$$

但是 Java 中却允许协变子类型化规则：

$$\frac{S<:T}{Array\;S<:Array\;T}$$

最初是出于多态的目的引入的规则，但由于它严重地影响了数组的性能（因为每次赋值都需要动态检查类型），被认为是语言设计的一个缺陷。

---

然而，我们可以引入类型构造子$Source\;T,Sink\;T$ 分别表示 “有能力被读出 T 类型数据的类型” 和 “有能力存储 T 类型数据的类型”。那么有：

$$\frac{\Gamma|\Sigma\vdash t_1:Source\;T_1}{\Gamma|\Sigma\vdash !t_1:T_1}\\ \frac{\Gamma|\Sigma\vdash t_1:Sink\;T_1\quad \Gamma|\Sigma\vdash t_2:T_1}{\Gamma|\Sigma\vdash t_1:=t_2:Unit}$$

而这两个构造子都是协变的：

$$\frac{S<:T}{Source\;S<:Source\;T}\\ \frac{S<:T}{Sink\;S<:Sink\;T}$$

且

$$Ref\;T<:Source\;T\\ Ref\;T<:Sink\;T$$

# 子类型化的强制语义

• 考虑下面这个问题。首先，Integer 应该为 Double 的一个子类型，因为所有用 double 的运算都可以替换为 integer。数学上讲，这就意味着整数集合是实数集合的子集，但是在计算机存储中，整型和浮点数的存储方式完全不一样。那就不能直接简单地将 double 替换为 integer。

• 我们可以采用子类型化的强制语义来解决这个问题。这种语义可以表示为一个函数，它将项从该语言的形式转化为一个更低级的不含子类型化规则的语言形式。我们选择含记录和 Unit 类型的纯简单类型 lambda 演算作为目标低级语言。

• 通常，编译过程包含了三个翻译函数：一个作用于类型，一个用来子类型化，一个用来类型化。用$[[-]]$ 表示类型翻译函数（空心中括号）：

  $$\begin{aligned} & [[Top]]=Unit\\ & [[T_1 \rightarrow T_2]]=[[T_1]]\rightarrow [[T_2]] \\ & [[\{l_i:T_1,i\in 1..n\}]]=\{l_i:[[T_i]],i\in 1..n\} \end{aligned}$$

  定义符号$C::S<:T$ 表示推导树 C 推导出 S 是 T 的子类型。那么有：

  $$[[\frac{}{T<:T}]]=\lambda x:[[T]].x\\ [[\frac{}{S<:Top}]]=\lambda x:[[S]].unit\\ [[\frac{C_1::S<:U\quad C_2::U<:T}{S<:T}]]=\lambda x:[[S]].[[C_2]]([[C_1]]x)\\ [[\frac{C_1::T_1<:S_1\quad C_2::S_2<:T_2}{S_1\rightarrow S_2<:T_1\rightarrow T_2}]]=\lambda f:[[S_1\rightarrow S_2]].\lambda x:[[T_1]].[[C_2]](f[[C_1]]x)\\ [[\frac{}{\{l_i:T_i,i\in1..n+k\}<:\{l_i:T_i,i\in1..n\}}]]=\lambda r:\{l_i:[[T_i]],i\in1..n+k\}.\{l_i=r.l_i,i\in1..n\}\\ [[\frac{foreach\;i\quad C_i::S_i<:T_i}{\{l_i:S_i\}<:\{l_i<:T_i\}}]]=\lambda r:\{l_i:[[S_i]]\}.\{l_i=[[C_i]](r.l_i)\}\\ [[\frac{\{k_j:S_j\}是\{l_i:T_i\}的置换}{\{k_j:S_j\}<:\{l_i:T_i\}}]]=\lambda r:\{k_j:[[S_j]]\}.\{l_i=r.l_i\}$$

  这翻译其实就是把所有的子类型化规则用 lambda 演算替换掉。从而得到不含有子类型化的类型。譬如

  $$[[Int<:Double]]=\lambda x.f(x):Int\rightarrow Double$$

• 引理，如果$C::S<:T$，则$\vdash [[C]]:[[S]]\rightarrow [[T]]$。

  也就是说，这个翻译函数对子类型化$S<:T$ 的翻译结果就是一个$[[S]]\rightarrow [[T]]$ 的 lambda 抽象函数。

# 吻合性

• 我们需要对子类型的翻译函数给出语义解释（可以理解为，给出上面推导规则配套的公理），例如：

  $$[[Bool<:Int]]=\lambda b:Bool.if\;b\;then\;1\;else\;0\\ [[Bool<:Float]]=\lambda b:Bool.if\;b\;then\;1.0\;else\;0.0$$

  这是一种强制类型转换的语义。但是会有歧义，譬如在求值：

  $$(\lambda x:String.x)\;true$$

  时，我们可以把 true 转为 Int 再转为 String，得到求值结果 “1”，或者把 true 转为 Float 再转为 String，得到求值结果为 “1.0”。

• 解决这个问题是在类型翻译函数的定义中附加一个要求，即吻合性：

  • 对结论都为$\Gamma\vdash t:T$ 的类型推导$D_1,D_2$，若产生的翻译$[[D_1]],[[D_2]]$ 为目标 语言中行为等价的项，则称从一个语言中的类型推导转换为目标语言项的翻译是吻合的。

  例如为了解决上面那个例子问题，就可以改变$[[Float<:String]]$ 函数的定义，使得$[[Float<:String]]\;1.0="1"$。

# 交叉类型和联合类型

• 交叉算子：

  $$\frac{S<:T_1\quad S<:T_2}{S<:T_1\wedge T_2}\\ T_1\wedge T_2<:T_1\\ T_1\wedge T_2<:T_2\\ S\rightarrow T_1\wedge S\rightarrow T_2<:S\rightarrow(T_1\wedge T_2)$$

  这告诉我们，类型$T_1\wedge T_2$ 即可一当作$T_1$ 来用，也可以当作$T_2$ 来用。

  例如我们可以给加算子赋予类型$(Nat\rightarrow Nat\rightarrow Nat)\wedge(Float\rightarrow Float\rightarrow Float)$，使其可以作用于两个自然数或两个浮点数。

  然而交叉类型的规则会给语言设计者带来难题，更多时候使用一种证明更为容易的 “精炼类型”。

• 联合算子$T_1\vee T_2$ 不做介绍 ==

# 子类型的元理论

• 我们增加一个规则，把之前深度、广度、置换子类型化规则合一：

  $$\frac{\{l_i,i\in1..n\}\subseteq\{k_j,j\in1..m\}\quad l_i=k_j\Rightarrow S_j<:T_i}{\{k_j:S_j,j\in1..m\}<:\{l_i:T_i,i\in1..n\}}$$

  有了这个规则，我们便无需再声明$S<:S$ 和$\frac{S<:T\quad T<:U}{S<:U}$ 这两条了。（因为都是上面规则的特例）

• 于是我们可以写一个小的程序来判断项的类型：

  $subtype::T\rightarrow T\rightarrow Bool$

  subtype S T = if T == Top then true

  else if $S=S_1\rightarrow S_2$ and $T=T_1\rightarrow T_2$

  then subtype $T_1\;S_1\wedge$ subtype $S_2\;T_2$

  else if S 和 T 满足上面那个规则 then True else False

# 算法类型化

• 根据我们之前给出的类型推导规则，共一个结论会有很多的推导式。譬如：

  $$\frac{\frac{\frac{...}{\Gamma\vdash s:S}\quad \frac{...}{S<:U}}{\Gamma\vdash s:U}\quad\frac{...}{U<:T}}{\Gamma\vdash s:T}$$

  可以改写为：

  $$\frac{\frac{...}{\Gamma\vdash s:S}\quad\frac{\frac{...}{S<:U}\quad\frac{...}{U<:T}}{S<:T}}{\Gamma\vdash s:T}$$

  这不是很好便于写程序生成推导。于是，类似之前的子类型，我们需要在保持推导能力的前提下，对推导规则进行压缩。于是就有了算法类型化：

• 算法类型化：

  $$\frac{x:T\in\Gamma}{\Gamma\vdash x:T}\\ \frac{\Gamma,x:T_1\vdash t_2:T_2}{\Gamma\vdash\lambda x:T_1.t_2:T_1\rightarrow T_2}\\ \frac{\Gamma\vdash t_1:T_1\rightarrow T_2'\quad \Gamma\vdash t_2:T_2\quad\Gamma\vdash T_2<:T_1}{\Gamma\vdash t_1\;t_2:T_2'}\\ \frac{foreach\;i\quad\Gamma\vdash t_i:T_i}{\Gamma\vdash\{l_i=t_i,i\in1..n\}:\{l_i:T_i,i\in1..n\}}\\ \frac{\Gamma\vdash t_1:\{l_i:T_i,i\in1..n\}}{\Gamma\vdash t_i.l_i:T_i}$$

  这套系统其实等价于之前声明的一大堆子类型规则，它可靠且完备。

  算法类型化种，也可以引入 Top 合 Bot。

# 合类型和交类型

• [定义] 对类型 J 和类型 S，T，如果有$S<:J,T<:J$，且对所有满足$S<:U,T<:U$ 的类型 U，都有$J<:U$，则称 J 为 S 和 T 的合类型。记为$S\vee T=J$。同理对类型 M，如果$M<:S,M<:T$，且对所有类型满足$L<:S,L<:T$ 的类型 L 都有$L<:T$，那么$L<:M$，则称 M 为 S 合 T 的交类型，记为$S\wedge T=M$。

• 这有啥用呢，其实之前有要求：

  $$\frac{\Gamma\vdash t_1:Bool\quad\Gamma \vdash t_2:T\quad\Gamma\vdash t_3:T}{\Gamma\vdash if\;t_1\;then\;t_2\;else\;t_3:T}$$

  if 的 then 和 else 必须类型相同。但是考虑下面这个情况：

  $$if\;t\;then\;\{x=true,y=1\}\;else\;\{x=false,z="c"\}$$

  虽然 then 和 else 后类型不同，但是它们有个合类型$\{x:Bool\}$。即 if 的结果总是能当$\{x:Bool\}$ 类型来用的。

# 递归类型

# 递归类型简介

# 实例

# 整型列表

• 整型列表的递归定义（变式类型）：

  $$NatList=<nil:Unit,cons:\{Nat,NatList\}>$$

  对类型引入一个明确的递归操作符$\mu$：

  $$NatList=\mu X.<nil:Unit,cons:\{Nat,X\}>$$

  读作 “将$NatList$ 定义为满足$X=<nil:Unit,cons:\{Nat,X\}$ 的无穷的类型”。

• 相关算子：

$$nil=<nil=unit>\;as\;NatList\\ cons=\lambda n:Nat.\lambda l:NatList.<cons=\{n,l\}>\;as\;NatList$$

$nil$ 表示空列表，而$cons:Nat\rightarrow NatList\rightarrow NatList$ 表示在给定列表头再加一个元素。

$$isnil=\lambda l:NatList.case\;l\;of\\ <nil=u>\Rightarrow true\\ |<cons=p>\Rightarrow false\\ hd=\lambda l:NatList.case\;l\;of\\ <nil=u>\Rightarrow 0\\ |<cons=p>\Rightarrow p.1\\ tl=\lambda l:NatList.case\;l\;of\\ <nil=u>\Rightarrow l\\ |<cons=p>\Rightarrow p.2$$

$isnil:NatList\Rightarrow Bool$可以判列表是否为空。

$hd:NatList\Rightarrow Nat$表示返回列表的头元素

$tl:NatList\Rightarrow NatList$表示删除列表的头元素。

# 饥饿函数

• 定义类型：

  $$type\;Hungry=\mu A.Nat\rightarrow A\\ Hungry=Nat\rightarrow Nat\rightarrow Nat\rightarrow...$$

# 流

• 一个有用的饥饿函数的变形就是流类型：

  $$Stream=\mu A.Unit\rightarrow\{Nat,A\}$$

  它接受一个 Unit 类型，然后返回一个数字和一个新的流的序对。

• 有用的算子：

  $$hd=\lambda s:Stream.(s\;unit).1\\ tl=\lambda s:Stream.(s\;unit).2$$

  显然一个是返回读的值，一个是返回新的流。

• 利用不动点算子定义流：

  $$upfrom0=fix\;(\lambda f:Nat\rightarrow Stream.\lambda n:Nat.\lambda\_:Unit.\{n,f\;(succ\;n)\})\;0$$

  解释下，中间括号里：

  $$c=\lambda f:Nat\rightarrow Stream.\lambda n:Nat.\lambda\_:Unit.\{n,f\;(succ\;n)\}\\ c:Nat\rightarrow Stream\rightarrow Nat\rightarrow Unit\rightarrow \{Nat,Stream\}\\ =(Nat\rightarrow Stream)\rightarrow Nat\rightarrow Stream$$

  于是$fix\;c:Nat\rightarrow Stream$ 实际上就是一个读入整型，然后返回以其开头递增的一个流。就是解了一个递归函数：

  $$c=\lambda f.\lambda n.(c':Stream)\\ c'=\lambda\_:Unit.\{n,f\;(succ\;n)\}:Stream$$

  于是有：

  $$hd\;(tl\;(tl\;(tl\;upfrom0)))=3:Nat$$

---

• 流的一个变型：

  $$Process=\mu A.Nat\rightarrow\{Nat,A\}$$

  这是进程类型，譬如：

  $$p=fix\;(\lambda f:Nat\rightarrow Process.\lambda acc:Nat.\lambda n:Nat.\\ let\;newacc\;=\;plus\;acc\;n\;in\{newacc,f\;newacc\}\\ 0 ):Process$$

  于是有：

  $$(p\;1).1\rightarrow 1\\ (p\;1\;2).1\rightarrow3\\ (p\;1\;2\;3).1\rightarrow6\;\\ ....$$

  是个累加器。

# 对象

• 一个计数器对象：

  $$Counter=\mu C.\{get:Nat,inc:Unit\rightarrow C\}$$

  构造对象：

  $$c=fix\;(\lambda f:\{x:Nat\}\rightarrow Counter.\lambda s:\{x:Nat\}.\\ \{get=s.x,\\ inc=\lambda\_:Unit.f\;\{x=succ(s.x)\}\\ \})\;\{x=0\}$$

  于是有：

  $$c1=c.inc\;unit\\ c2=c.inc\;unit\\ c2.get\rightarrow 2:Nat$$

# 递归类型的递归值

• 在之前无类型 lambda 演算时，解递归的不动点算子我就有疑问，它不是可类型化的。但现在，我们可以利用递归类型定义它：

  $$fix=\lambda f:T\rightarrow T.(\lambda x:(\mu A.A\rightarrow T).f\;(x\;x))(\lambda x:(\mu A\rightarrow T).f\;(x\;x))\\ fix:(T\rightarrow T)\rightarrow T$$

  即$x:\mu A.A\rightarrow T,x\;x:T$。

# 递归类型将无类型 λ 演算以一种良类型的方式嵌入含递归类型的静态类型化语言

• 考虑类型：$D=\mu X.X\rightarrow X$。$D=D\rightarrow D$。然后定义个将 D 到 D 的函数映射为 D 的投射函数：

  $$lam=\lambda f:D\rightarrow D.f\;as\;D\\ lam:(D\rightarrow D)\rightarrow D=D\rightarrow D=D$$

  定义函数：$ap=\lambda f:D.\lambda a:D.f\;a$。

• 于是我们可以把无类型 lambda 演算都整成 D 类型，以最简单的只含变量，抽象，作用的 lambda 演算为例：

  $$x^*=x\\ (\lambda x.M)^*=lam\;(\lambda x:D.M^*)\\ (M\;N)^*=ap\;M^*\;N^*$$

  我们可以认为，无类型 lambda 演算中任意一项$M$ 都可以用上面三条规则类型化$M^*:D$。

• 特别地，对于无类型 lambda 演算的不动点算子：

  $$fix=\lambda f.(\lambda x.f\;(\lambda y.x\;x\;y))(\lambda x.f\;(\lambda y.x\;x\;y))\\ \Rightarrow\\ fix^*=lam\;(\lambda f:D\\ ap\;(lam\;(\lambda x:D.ap\;f\;(ap\;x\;x)))\\ (lam\;(\lambda x:D.ap\;f\;(ap\;x\;x)))\\ );\\ fix^*:D$$

• 纯 λ 演算的嵌入可扩展为含一些特征（如数字）。此时我们可以重写 D：

  $$D=\mu X.<nat:Nat,fn:X\rightarrow X>\\ lam=\lambda f:D\rightarrow D.<fn=f>\;as\;D;\\ ap=\lambda f:D.\lambda a:D.\\ case\;f\;of\\ <nat=n>\Rightarrow diverge_D\;unit\\ |<fn=f>\Rightarrow f\;a;$$

  其中$diverge_D=\lambda\_:Unit.fix_D\;(\lambda x:D.x):Unit\rightarrow D$。$diverge_D\;unit$ 表示直接发散掉。

  $$suc=\lambda f:D.case\;f\;of\\ <nat=n>\Rightarrow(<nat=succ\;n>\;as\;D)\\ |<fn=f>\Rightarrow diverge_D\;unit\\ suc:D\rightarrow D\\ zro=<nat=0>\;as\;D$$

# 递归类型的形式

• 牵扯到无穷递归的问题总是很麻烦。我们需要考虑究竟怎样考虑$NatList$ 和其递归展开式$\{nil:Unit,cons:\{Nat,NatList\}\}$ 间的关系究竟是什么？

1、相等递归。这就是我自然的理解，类似于$N=map\;(+1)\;N$。无穷加一还是无穷。但显然这样的类型检查算法将会很痛苦，因为它检查不了无穷多层的类型。

2、同构递归（iso-recursive）将类型和其展开式视为不同，但同构。使用标准的代换符号。譬如递归类型$\mu X.T$（T 中含 X），有：

$$unfold[\mu X.T]=\mu X.T\rightarrow[X\mapsto\mu X.T]T\\ fold[\mu X.T]=unfold^{-1}[\mu X.T]$$

这里我的理解还不是很到位。我的理解是，当实例化类型时，譬如我就想声明一个数组时，可以 fold 成一个$x:NatList$。但当我需要求值时，求到第几个就需要 unfold 几下。这样不要把递归类型看成一个无穷的类型，而把它看作 “另一个类型的衍生类型”。而 “另一个类型” 我们并不需要知道它是啥，只需要知道需要访问时可以 unfold 就好了。

# 递归元理论

# 归纳和共归纳

• 声明$\mathcal{U}$ 是全集，是 “世界上所有事物的集合”。

• [定义]：若$X\subseteq Y\Rightarrow F(X)\subseteq F(Y)$，那么函数$F\in\mathcal{P}(\mathcal{U})\rightarrow\mathcal{P}(\mathcal{U})$ 就是单调的。我们接下来的讨论都假设了$F$ 是个单调函数，而且通常把它当作一个产生函数。

• [定义]：对于一个$X\subseteq\mathcal{U}$：

  • 若$F(X)\subseteq X$，则称 X 是 F 封闭的。
  • 若$X\subseteq F(X)$，则称 X 是 F 一致的。
  • 若$X=F(X)$，则称 X 是 F 的不动点。

• [Knaster-Tarski 定理]：

  • 所有对 F 封闭集的交集是最小的 F 不动点。
  • 所有对 F 一致集的并集是最大的 F 不动点。

• [定义]：F 的最小不动点记为$\mu F$，最大不动点记为$\nu F$。

• [说明]：产生函数往往可以用一组规则实例表示，譬如：

  $$F(\emptyset)=\{a\}\\ F(\{a\})=\{a,b\}\\ F(\{b\})=\{a\}\\ F(\{a,b\})=\{a,b\}$$

  F 就可以压缩为：$\frac{}{a},\frac{a}{b}$ 表示。（在另一篇博客《不动点和循环》中讨论了这种记法）

• [推论]：

  • 归纳原则：如果 X 是 F 封闭的，则$\mu F\subseteq X$
  • 共归纳原则：如果 X 是 F 一致的，则$X\subseteq \nu F$。

• 说点自己的理解。实际上定义的这些东西，其实表达了我们推理的过程。集合 X 用于表示：目前通过公理和推导规则得到的定理的集合。它是单调的，因为一次推导并不会使我们得到的定理减少。这也在我不动点和循环那篇得到了讨论。

# 有限类型和无穷类型

• 考虑三种类型构造子$\rightarrow,\times,Top$。我们将类型表示为树的形式，节点用三种构造子中的一种作为标签。

  把 1 和 2 的序列集合记为$\{1,2\}^*$，空序列记为$\bullet$，而$i^k$ 就表示 i 的 k 次方。如果$\pi,\sigma$ 都是序列，那么$\pi,\sigma$ 就表示把两个序列的串联。

• [定义]：一个树类型是一个局部函数$T\in\{1,2\}^*\rightharpoonup \{\rightarrow,\times,Top\}$，它满足：

  • $T(\bullet)$ 有定义
  • 若$T(\pi,\sigma)$ 有定义，则$T(\pi)$ 也有定义。
  • 若$T(\pi)=\rightarrow$ 或$\times$，则$T(\pi,1),T(\pi,2)$ 也都有意义。
  • 若$T(\pi)=Top$，则$T(\pi,1),T(\pi,2)$ 都没意义。

  若$dom(T)$ 是有限的，那么树类型 T 也是有限的。所有树类型的集合可记为$\mathcal{T}$，所有有限树类型构成的子集记为$\mathcal{T}_f$。

• 为了方便，将满足$T(\bullet)=Top$ 的树写为$Top$。若$T_1,T_2$ 都是树，把满足$(T_1\times T_2)(\bullet)=\times$ 和$(T_1\times T_2)(i,\pi)=T_i(\pi)$ 的树记为$T_1\times T_2$，把$(T_1\rightarrow T_2)(\bullet)=\rightarrow$ 和$(T_1\rightarrow T_2)(i,\pi)=T_i(\pi)$ 的树记为$T_1\rightarrow T_2$。于是给出两个例子：

• 可以根据语法给出有限树类型的更加简洁的定义形式：

  $$T::=Top|T\times T|T\rightarrow T$$

# 子类型

• [定义]：对两个有限树类型$S,T$，若有$(S,T)\in \mu S_f$，其中单调部分函数定义为：

  $$S_f\in\mathcal{P}(\mathcal{T}_f\times\mathcal{T}_f)\rightarrow\mathcal{P}(\mathcal{T}_f\times\mathcal{T}_f)\\ S_f(R)=\{(T,Top)|T\in\mathcal{T}_f\}\cup\\ \{(S_1\times S_2,T_1\times T_2)|(S_1,T_1),(S_2,T_2)\in R\}\cup\\ \{(S_1\rightarrow S_2,T_1\rightarrow T_2)|(T_1,S_1),(S_2,T_2)\in R\}$$

  那么$S$ 是$T$ 的一个子类型。其实$S_f$ 用规则可以压缩地写成：

  $$\frac{}{T<:Top}\quad\frac{S_1<:T_1\quad S_2<:T_2}{S_1\times S_2<:T_1\times T_2}\quad\frac{T_1<:S_1\quad S_2<:T_2}{S_1\rightarrow S_2<:T_1\rightarrow T_2}$$

  其中应该把横线上的$S_1<:T_1$ 理解为$(S_1,T_1)$ 是$S_f$ 的输入，横线下理解为是输出。这也就是子类型的递归定义。

• [定义]：扩展到无穷，有如果$(S,T)\in\nu S$，其中：

  $$S\in\mathcal{P}(\mathcal{T}\times\mathcal{T})\rightarrow\mathcal{P}(\mathcal{T}\times\mathcal{T})\\ S(R)=\{(T,Top)|T\in\mathcal{T}\}\cup\\ \{(S_1\times S_2,T_1\times T_2)|(S_1,T_1),(S_2,T_2)\in R\}\cup\\ \{(S_1\rightarrow S_2,T_1\rightarrow T_2)|(T_1,S_1),(S_2,T_2)\in R\}$$

  那么 S 是 T 的一个子类型。注意，这里用的是最大不动点了，需要考虑的是一个更大的类型全集。

• [定义]：如果关系 R 在单调函数$TR(R)=\{(x,y)|\exists z\in\mathcal{U},(x,z),(z,y)\in R\}$ 下是封闭的。即$TR(R)\subseteq R$，那么关系$R\subseteq\mathcal{U}\times\mathcal{U}$ 具有传递性。

• [引理]：设$F\in\mathcal{P}(\mathcal{U}\times\mathcal{U})\rightarrow\mathcal{P}(\mathcal{U}\times\mathcal{U})$ 为一个单调函数。如果对任意$R\subseteq\mathcal{U}\times\mathcal{U}$ 都有$TR(F(R))\subseteq F(TR(R))$，那么$\nu F$ 是有传递性的。

• [定理]：$\nu S$ 具有传递性。S 为定义无穷子类型的单调函数。

• [定理]：设 F 和 G 为单调函数，且$H(X)=F(X)\cup G(X)$，则$\mu H$ 为满足对 F 封闭和对 G 封闭的最小集合。

# 成员检查

• 本章中心内容：给定某全集$\mathcal{U}$ 上的产生函数 F 和元素$x\in\mathcal{U}$，怎么判断 x 是否在$\nu F$ 中？

• 通常一个元素$x\in\mathcal{U}$ 可以通过很多方法由 F 产生。也就是说，不止一个集合$X\subseteq\mathcal{U}$，满足$x\in F(X)$。称这种集合 X 为 x 的一个产生集。由于 F 的单调性，任何 x 的产生集的超集也是 x 的一个产生集。

• [定义]：如果对所有的$x\in\mathcal{U}$，簇集：

  $$G_x=\{X\subseteq\mathcal{U}|x\in F(X)\}$$

  要么为空，要么簇集中存在唯一一个集合是所有其他集合的子集，则说产生函数 F 是可逆的。

  当 F 可逆时，部分函数$support_F\in\mathcal{U}\rightarrow\mathcal{P}(\mathcal{U})$ 定义如下：

  $$support_F(x)=\begin{cases}X&if\;X\in G_x\;and\;\forall X'\in G_x,X\subseteq X'\\ \uparrow&if\;G_x=\emptyset \end{cases}$$

  扩展定义到集合形式：

  $$support_F(X)=\begin{cases}\bigcup_{x\in X}support_F(x)&if\;\forall x\in X,support_F(x)\downarrow\\\uparrow&otherwise\end{cases}$$

---

• 我们的目标时提出一个检查产生函数 F 的最大和最小不动点中成员的算法。

• [定义]：假如$support_F(x)\downarrow$，那么元素$x$ 是$F$ 支持的，否则就是 F 不支持的。一个 F 支持的元素 x，若$support_F(x)=\emptyset$，那么称其为 F 的基。

  对每个 X，基 x 都在$F(X)$ 中。而 F 不支持的元素 x 不会出现在$F(X)$ 中。

• [例]：考虑$\mathcal{U}=\{a,b,c,d,e,f,g,h,i\}$ 上的一个单调可逆生成函数$E$，它的推导规则为：

  $$\frac{i\quad a}{h}\quad\frac{b\quad c}{a}\quad\frac{b}{d}\quad\frac{d}{e}\quad\frac{e}{b}\quad\frac{f\quad g}{c}\quad\frac{g}{f}\quad\frac{}{g}$$

  则很显然，以元素 h 为例，$G_h$ 就为所有含$i,a$ 的集合。而$support_E(h)=\{i,a\}$。因为只有 i 没有生成规则，所以 i 是唯一不被支持的元素。下图就说明了 support 关系，元素 x 指向的元素构成的集合就是$support_E(x)$。（其实就是把推导规则从结果到前提连线）

---

• [定义]：假设 F 是一个可逆的产生函数，定义布尔函数$gfp_F$ 如下：

  $$gfp_F(X)=if\;support(X)\uparrow\;then\;false\\ else\;if\;support(X)\subseteq X\;then\;true\\ else\;gfp_F(support(X)\cup X)$$

  直观地解释，就是从 X 开始不断扩展他，直到他变成一致的，或包含一个不支持元素。

• [引理 1]：当且仅当$support_F(X)\downarrow$，且$support_F(X)\subseteq Y$，有$X\subseteq F(Y)$ 成立。

  证明：原命题等价于证明$x\in F(Y)\quad iff\quad support_F(x)\downarrow\& support_F(x)\subseteq Y$。

  首先假设$x\in F(Y)$。于是$Y\in G_x$，即$G_x\neq\emptyset$。因为 F 是可逆的，所以$G_x$ 中一定有个最小集合$support_F(x)$。所以有

  $support_F(x)\subseteq Y$。

  反之，根据单调性，若$support_F(x)\subseteq Y$，则有$F(support_F(x))\subseteq F(Y)$。由 support，$G_x$ 的定义，

  有$x\in F(support_F(x))$，所以$x\in F(Y)$。

• [引理 2]：假设 P 是 F 的一个不动点。那么$X\subseteq P$ 当且仅当$support_F(X)\downarrow$ 且$support_F(X)\subseteq P$。

  证明：根据$F(P)=P$，直接转换成$X\subseteq F(P)$ 当且仅当$support_F(X)\downarrow$ 且$support_F(X)\subseteq P$。即刚证完的引理 1。

• [定理 1]：如果$gfp_F(X)=true$，那么$X\subseteq \nu F$，反之$gfp_F(X)=false$ 的话，就有$X\not\subseteq \nu F$。

  证明：

  • 使$gfp(X)=true$ 只有两种情况：
    • $support(X)\subseteq X$ 且$suppoert(X)\downarrow$。此时根据引理 1，有$X\subseteq F(X)$，根据共归纳原则，有$X\subseteq \nu F$。
    • $gfp(support(X)\cup X)=true$。由归纳假设，有$support(X)\cup X\subseteq\nu F$。所以有$X\subseteq\nu F$。
  • 使$gfp(X)=false$ 也有两种情况，类似证明。需用引理 2。

• [定义]：给定可逆产生函数 F 和元素$x\in\mathcal{U}$，x 的直接前驱集合$pred_F(x)$ 为：

  $$pred_F(x)=\begin{cases}\emptyset&support_F(x)\uparrow\\support_F(x)&support_F(x)\downarrow\end{cases}$$

  可以把它扩展到集合上：$pred_F(X)=\bigcup_{x\in X}support_F(x)$

  定义所有可达元素：

  $$reachable_F(X)=\bigcup_{n\geq 0}pred^n(X)$$

  扩展到$reachable_F(x)=reachable_F(\{x\})$。如果$y\in reachable_F(x)$，则 y 是 x 出发可到达的。

• [定义]：如果对任一$x\in\mathcal{U}$，$reachable_F(x)$ 都是有限的，那么可逆产生函数$F$ 也说是有限状态的。

• [定理 2]：如果$reachable_F(X)$ 是有限的，那么$gfp_F(X)$ 就可以定义。因此，如果 F 是有限状态的，那么对任一有限集$X\subseteq \mathcal{U}$，$gfp_F(X)$ 都可以终止。

[总结]：根据定理 1，用$gfp_F$ 函数就可以判断元素是否在最大不动点中，再根据定理 2，这个算法对有限状态可逆函数总是正确的，可停止的。

• 此外，可定义布尔函数：

  $$lfp(X)=if\;support(X)\uparrow\;then\;false\\ else\;if\;X=\emptyset\;then\;true\\ else\;lfp(support_F(X))$$

  $X\subseteq\mu F\Leftrightarrow lfp(X)=true$。它是对有限状态可逆函数检验最小不动点成员的方法。但它只对部分产生函数是正确的。