编程语言理论

1. 类型系统

1.1 类型系统分类

1.2 静态类型系统

Hindley-Milner 类型推断：

自动推断表达式的最一般类型：

$\text{算法W}(\Gamma ,e)=(S,\tau )$

其中 $\Gamma$ 为类型环境，$S$ 为替换，$\tau$ 为类型。

多态类型：

$id:\forall \alpha .\alpha \to \alpha$

Let 多态：

let id = λx.x in (id 1, id true)  -- 合法

而：

(λid.(id 1, id true))(λx.x)  -- 不合法（ML中）

1.3 子类型

子类型关系 $S<:T$ 表示 $S$ 类型的值可以用在期望 $T$ 类型的地方。

函数子类型的协变与逆变：

• 参数类型：逆变（contravariant）
• 返回类型：协变（covariant）

$S_1\to S_2<:T_1\to T_2⟺T_1<:S_1\wedge S_2<:T_2$

Liskov 替换原则（LSP）：

若 $S<:T$，则 $T$ 类型的对象可被 $S$ 类型的对象替换，程序行为不变。

1.4 代数数据类型

积类型（Product）：

$A\times B=\{(a,b)\mid a\in A,b\in B\}$

和类型（Sum）：

$A+B=\text{inl}(a)\mid \text{inr}(b)$

类型同构：

2. Lambda 演算

2.1 无类型 Lambda 演算

语法：

$e::=x\mid \lambda x.e\mid e_1{e}_2$

β 归约：

$(\lambda x.e_1)e_2\to e_1[x:=e_2]$

α 转换：

$\lambda x.e{\equiv }_{\alpha }\lambda y.e[x:=y]$

η 归约：

$\lambda x.(fx){\to }_{\eta }f(x\notin FV(f))$

2.2 归约策略

2.3 Church 编码

Church 布尔值：

$\text{true}=\lambda t.\lambda f.t$

$\text{false}=\lambda t.\lambda f.f$

Church 数：

$0=\lambda f.\lambda x.x$

$1=\lambda f.\lambda x.fx$

$2=\lambda f.\lambda x.f(fx)$

$n=\lambda f.\lambda x.f^{n}x$

后继：

$\text{succ}=\lambda n.\lambda f.\lambda x.f(nfx)$

加法：

$\text{plus}=\lambda m.\lambda n.\lambda f.\lambda x.mf(nfx)$

2.4 Y 组合子

实现不动点，允许递归：

$Y=\lambda f.(\lambda x.f(xx))(\lambda x.f(xx))$

$Yf=f(Yf)$

2.5 简单类型 Lambda 演算（STLC）

类型语法：

$\tau ::=B\mid {\tau }_1\to {\tau }_2$

类型规则：

$\frac{x:\tau \in \Gamma }{\Gamma ⊢x:\tau }\text{ (Var)}$

$\frac{\Gamma ,x:{\tau }_1⊢e:{\tau }_2}{\Gamma ⊢\lambda x:{\tau }_1.e:{\tau }_1\to {\tau }_2}\text{ (Abs)}$

$\frac{\Gamma ⊢e_1:{\tau }_1\to {\tau }_2\Gamma ⊢e_2:{\tau }_1}{\Gamma ⊢e_1{e}_2:{\tau }_2}\text{ (App)}$

类型安全 = 进展性 + 保持性：

• 进展性：良类型的闭项要么是值，要么可以归约
• 保持性：归约保持类型不变

3. 操作语义

3.1 小步语义

定义单步归约关系 $\to$：

$\frac{e_1\to e_1^{\prime }}{e_1{e}_2\to e_1^{\prime }{e}_2}$

$\frac{v_1{e}_2\to v_1{e}_2^{\prime }}{e_2\to e_2^{\prime }}$

$\frac{}{(\lambda x.e)v\to e[x:=v]}$

3.2 大步语义

定义求值关系 $\Downarrow$：

$\frac{e_1\Downarrow \lambda x.e{e}_2\Downarrow v_{2}e[x:=v_2]\Downarrow v}{e_1{e}_2\Downarrow v}$

3.3 小步 vs 大步

4. 指称语义

4.1 基本思想

将程序映射到数学对象（域论中的元素）：

$[[e]]:\text{Env}\to \text{Value}$

4.2 语义函数

$[[x]]\rho =\rho (x)$

$[[\lambda x.e]]\rho =\lambda v.[[e]]\rho [x\mapsto v]$

$[[e_1{e}_2]]\rho =([[e_1]]\rho )([[e_2]]\rho )$

4.3 不动点语义

递归定义的语义通过域论中的最小不动点给出：

$[[\text{fix}]]=\text{lfp}(F)={⨆}_{n=0}^{\infty }{F}^n(\perp )$

5. 程序验证

5.1 Hoare 逻辑

Hoare 三元组：

$\{P\}C\{Q\}$

含义：若前置条件 $P$ 成立，执行命令 $C$ 后，后置条件 $Q$ 成立。

推理规则：

$\frac{}{\{P\}\text{skip}\{P\}}$

$\frac{}{\{Q[x:=e]\}x:=e\{Q\}}$

$\frac{\{P\}{C}_1\{R\}\{R\}{C}_2\{Q\}}{\{P\}{C}_1;C_2\{Q\}}$

$\frac{\{P\wedge b\}{C}_1\{Q\}\{P\wedge \neg b\}{C}_2\{Q\}}{\{P\}\text{if }b\text{ then }{C}_1\text{ else }{C}_2\{Q\}}$

$\frac{\{P\wedge b\}C\{P\}}{\{P\}\text{while }b\text{ do }C\{P\wedge \neg b\}}$

5.2 循环不变式

循环不变式 $I$ 必须满足：

1. 初始化：循环开始前 $I$ 成立
2. 保持：每次迭代后 $I$ 仍然成立
3. 终止：循环结束时 $I\wedge \neg b$ 可推出 $Q$

5.3 最弱前置条件

$\text{wp}(x:=e,Q)=Q[x:=e]$

$\text{wp}(C_1;C_2,Q)=\text{wp}(C_1,\text{wp}(C_2,Q))$

$\text{wp}(\text{if }b\text{ then }{C}_1\text{ else }{C}_2,Q)=(b\Rightarrow \text{wp}(C_1,Q))\wedge (\neg b\Rightarrow \text{wp}(C_2,Q))$

5.4 类型系统与验证

类型系统是一种轻量级程序验证：

依赖类型：类型可以依赖于值，允许在类型层面表达更精细的属性。

$\text{Vec}(A,n):\text{Type}$

长度为 $n$ 的 $A$ 类型向量，类型检查器可验证列表操作的正确性。