【Lambda演算与STLC类型论基础】 1 简单的λ演算

1 简单的$\lambda$演算

1.1 函数

考虑函数

$$f(x) = M,$$

我们将其使用$\lambda$演算法的方式重写

$$\lambda x.M$$

1.2 相继式演算

一个类型论中，决定哪些类型合法、某一项有什么类型的规则称为类型规则 (Typing Rules)，它们尝尝使用相继式演算 (Sequent Calculus) 的方式如下给出：

$$\frac{\text{Premise}_{1}~\text{Premise}_{2}~\dots~\text{Premise}_{n}}{\text{Conclusion}}(\text{Name})$$

• 该记号的主题是分数线
• 分子位置是若干条件 (Premise)
• 分母位置是结论 (Conclusion)
• 若干含义和结论共同组成判断 (Judgement)

1.3 类型

在类型论中，每一个项都有其对应的类型 (Type)。引入以下判断表示$A$是一个合法类型

$$A\text{ type}.$$

在STLC中，首先需要定义基本类型 (Base Type) 的集合$\mathcal{B}$，然后在此基础上递归定义其他类型。下面是两个基本规则：

$$\frac{A\in\mathcal{B}}{A\text{ type}} \text{Base}$$

Base规则意为：若$A$是一个基本类型，则它也是一个STLC的类型

$$\frac{A\text{ type}~ ~ ~B\text{ type}}{A\rightarrow B\text{ type}} \text{Func}$$

Func规则意为：若$A$和$B$均为STLC的类型，则类型$A$到类型$B$的函数$A\rightarrow B$也是STLC的类型

我们定义映射$\rightarrow$是右结合的，即$A\rightarrow B\rightarrow C = A \rightarrow (B \rightarrow C)$

1.4 语境

语境 (Context) 记录有哪些变量可用的信息。其基本规则有两条。我们使用$\Gamma \text{ ctx}$表示$\Gamma$是一个合法的语境，第一条基本规则说明空语境$\emptyset$是合法的语境：

$$\frac{}{\emptyset\text{ ctx}}$$

第二条基本规则说明，若$\Gamma$是一个语境，则$\Gamma,x:A$是一个语境，这表示在$\Gamma$中添加了类型为$A$的新变量$x$：

$$\frac{\Gamma \text{ ctx}}{\Gamma,x:A\text{ ctx}}$$

语境中的变量可以使用一个反向列表进行表示，其中的元素是项和其所属类型的二元组：

$$\emptyset,x:A,y:B,\dots~,$$

为方便起见，我们常常将上式中的空集忽略，简记为

$$x:A,y:B,\dots$$

1.5 项

一个类型论中的项 (term) 是类型论中最常被讨论到的部分。引入新判断

• $\Gamma \vdash M:A$ 表示在语境 $\Gamma$ 中，$M$ 是一个类型为 $A$ 的合法项

对于STLC，定义常量集合 $\mathcal{C}$ 和映射 $\text{toType}:\mathcal{C}\rightarrow\mathcal{B}$，其中映射 $\text{toType}$ 为每个 $\mathcal{C}$ 中的常量定义其基本类型。

关于项的基本规则有四条
第一条表示任意语境中，常量集合 $\mathcal{C}$ 中的元素具有其对应的基本类型

$$\frac{c\in\mathcal{C}}{ \Gamma \vdash c:\text{toType}(c) }\text{Const}$$

第二条规则表示，若语境中存在变量 $x:A$，则该变量可以被 “使用”，$x:A$ 是该语境下的项

$$\frac{x:A\in \Gamma}{ \Gamma \vdash x:A}\text{Var}$$

第三条规则表示，若 $M:B$ 是语境 $\Gamma,x:A$ 下的项，则 $\lambda(x:A).M:A\rightarrow B$ 也是语境 $\Gamma$ 中的项

$$\frac{\Gamma,x:A \vdash M:B}{ \Gamma \vdash \lambda (x:A).M:A\rightarrow B}\text{Lam}$$

其中 $\lambda(x:A).M$ 表示以 $x$ 为类型 $A$ 的自变量，$M$ 为函数体的函数
若 $\lambda x.M$ 在语境 $\Gamma$ 中，$M$ 就应当在语境 $\Gamma, x:A$ 中，即它可以额外使用变量 $x$

第四条规则为函数应用的类型规则。若在语境 $\Gamma$ 下，$M$ 具有类型 $A\rightarrow B$，$N$ 具有类型 $A$，则 $MN$ 具有类型 $B$

$$\frac{\Gamma \vdash M:A \rightarrow B~ ~ ~ ~ ~ ~\Gamma\vdash N:A} {\Gamma \vdash MN:B} \text{App}$$

1.6 类型检查

1.6.1 考虑空语境下 $\lambda f.\lambda x.f~x:(A\rightarrow B)\rightarrow A\rightarrow B$ 的完整类型检查过程

$$\frac{\displaystyle \frac{\displaystyle \frac{\displaystyle \frac{f:A\rightarrow B\in f:A\rightarrow B,x:A}{ f:A\rightarrow B, x:A \vdash f:A\rightarrow B}\text{Var}~ ~ ~ \frac{x:A \in f:A\rightarrow B,x:A}{ f:A\rightarrow B, x:A \vdash x:A}\text{Var}} {f:A\rightarrow B, x:A \vdash f~x:B}\text{App}} {f:A\rightarrow B \vdash \lambda x.f~x:A\rightarrow B}\text{Lam}} {\emptyset \vdash \lambda f.\lambda x.f~x:(A\rightarrow B) \rightarrow A \rightarrow B}\text{Lam}$$

上面的例子构造了一个返回函数的函数，被返回的函数再接受多余的参数

1.6.2 考虑空语境下 $\lambda f~g~x.f(g~x):(B\rightarrow C) \rightarrow (A\rightarrow B) \rightarrow A \rightarrow C$ 的类型检查过程

• $f:B \rightarrow C$
• $g: A\rightarrow B$

记 $\Gamma = f:B\rightarrow C, g:A\rightarrow B, x:A$
Step 1.

$$\frac{ \frac{\displaystyle g:A \rightarrow B\in \Gamma} {\displaystyle \Gamma \vdash g:A\rightarrow B}\text{Var}~ ~ \frac{\displaystyle x:A\in \Gamma} {\displaystyle \Gamma \vdash x:A}\text{Var} } { \Gamma \vdash g~x:B }\text{App}$$

Step 2.

$$\frac{\displaystyle \frac{\displaystyle \frac{\displaystyle \frac{ \frac{\displaystyle f:B \rightarrow C\in \Gamma} {\displaystyle \Gamma \vdash f:B \rightarrow C}\text{Var}~ ~ \frac{\displaystyle y:B\in f:\Gamma} {\displaystyle \Gamma \vdash g~x:B}\text{Var} } { \Gamma \vdash f(g~x):C }\text{App}} {f:B\rightarrow C, g:A\rightarrow B \vdash \lambda x.f(g~x): A\rightarrow C}\text{Lam}} {f:B\rightarrow C \vdash \lambda g.\lambda x.f(g~x):(A\rightarrow B)\rightarrow A\rightarrow C}\text{Lam}} {\emptyset \vdash \lambda f.\lambda g.\lambda x.f(g~x):(B\rightarrow C) \rightarrow (A\rightarrow B) \rightarrow A \rightarrow C}\text{Lam}$$

1.7 某个 STLC 下的 $\mathcal{B}$、$\mathcal{C}$ 和 $\text{toType}$ 函数

注意，STLC 是一族类型论，对于 $\mathcal{B}$、$\mathcal{C}$ 和 $\text{toType}$ 函数的不同定义都会得到不同的 STLC。我们取

$$\begin{align} \mathcal{B} &= \{\top, \bot, \text{Ans}\}\\ \mathcal{C} &= \{\text{tt}, \text{yes}.\text{no}\}\\ \text{toType}(c) &= \begin{cases} \top, & c=\text{tt}\\ \text{Ans} & \text{otherwise} \end{cases} \end{align}$$

1.8 替换

1.8.1 出现

在形如

$$\lambda x.M$$

的函数中，除了$x$之外的变量使用称为 出现 (Occurance)，若 $x$ 出现在 $M$ 中，则称之为 绑定出现 (Bound Occurance)；不在形如 $\lambda x$ 结构中的变量在 $M$ 中的出现称为 自由出现 (Free Occurance)。下式中彩色为绑定出现，黑色为自由出现

$${\color{red}\lambda x}.{\color{red}x}({\color{green}\lambda y}.{\color{blue}\lambda x}.{\color{blue} x}{\color{green}y})z({\color{red}x}y)$$

1.8.2 $\alpha$ 转换

正如程序设计语言中对函数形参名称的正确改变不影响函数的功能，在 $\lambda$ 演算中给函数的参数进行正确改名是合法的，这样的转换称为 $\alpha$ 转换 ($\alpha$ Conversion)。

定义：$\alpha$转换
将项 $M$ 中的所有自由出现的 $x$ 重命名为 $y$ 后得到新的项 $N$，若这样的代换不将其中的任意自由出现变为绑定出现，则 $\lambda x.M$ 和 $\lambda y.N$ 等价

对于一个或有限任意多的项，总可以通过有限多次的 $\alpha$ 转换，使得其中的变量两两不同名。

定义：替换 (Substitution)
记 $M[x \mapsto N]$ 为将项中 $x$ 的全部自由出现替换为 $N$ 所得的项

1.9 规约

描述类型论中的项如何化简的规则称为规约 (Reduction)。STLC 中有如下两条规约规则

$\beta$ 规则描述将实参代入函数中的形参位置的过程

$$\frac{x:A \vdash M:B~ ~ ~ ~ ~ ~N:A} {(\lambda x.M)N \equiv M[x\mapsto N]:B} \beta\text{ rule}$$

$\eta$ 规则描述了函数的外延性

$$\frac{f:A\rightarrow B} {f \equiv \lambda x.f~x:A\rightarrow B} \eta\text{ rule}$$

正向应用这个等式称为 $\eta$ 展开 ($\eta$ Expansion)，反向应用这个等式称为 $\eta$ 规约

• 若一个 STLC 项不能在做任何的 $\beta$ 规约或 $\eta$ 规约，则称这个项是 $\beta\eta$-既约的，简称既约 (Normalized)或既约形式 (Normalized Form)。空语境中的既约形式称为闭既约形式 (Canonical Form)
• STLC 中的规约前后的类型不变，且拥有相同语境。这种性质称为subject reduction

定理
STLC 中的任何项都可以通过有限步规约达到既约形式

若一个类型论的规约具有上述性质，则称为停机的 (Terminating)，因此它作为编程语言时不是图灵完备的(图灵完备的编程语言可以做到不停机)

定理：Church-Rosser
一个 STLC 项有唯一的既约形式，与规约顺序无关

*1.10 使用 $\lambda$ 演算构造自然数

1.10.1 $\lambda$ 演算中的函数调用

$$\begin{align} (\lambda x.xy) a &= ay\\ (\lambda {\color{blue}x}.{\color{blue}x}y){(\color{blue}\lambda x.x)} &= (\lambda x.x)y = y \end{align}$$

1.10.2 构造自然数

$$\begin{align} 0 &\rightarrow \lambda sz.z = \lambda s.(\lambda z.z)\\ 1 &\rightarrow \lambda sz.s(z)\\ 2 &\rightarrow \lambda sz.s(s(z))\\ 3 &\rightarrow \lambda sz.s(s(s(z)))\\ &~~\,\vdots \end{align}$$

1.10.3 后继

$$\lambda wyx.y(wyx)$$

例如

$$\begin{align} (\lambda wyx.y(wyx))0 &= (\lambda wyx.y(wyx))(\lambda sz.z)\\ &= \lambda yx.y((\lambda sz.z)yx)\\ &= \lambda yx.y(x) \end{align}$$

1.10.4 加法

$$\lambda xysz.xs(ysz)$$

例如

$$\begin{align} \lambda xysz.xs(ysz)(1)(2) &= \lambda xysz.xs(ysz)(\lambda sz.s(z))(\lambda sz.s(s(z)))\\ &= (\lambda sz.s(z))s\Big((\lambda sz.s(s(z)))sz\Big)\\ &= (\lambda sz.s(z))s(s(s(z)))\\ &= s(s(s(z)))\\ \end{align}$$

2 STLC 的模型