本文为Type Theory and Formal Proof : An Introduction 的笔记，纯个人向（

---

简单类型（Simple types）

我们从一个类型变量（type variables）的无限集开始：$\mathbb{V}=\lbrace \alpha,\beta,\gamma,…\rbrace$.

所有简单类型的集合$\mathbb{T}$

1. 类型变量（Type variable）若$\alpha \in \mathbb{V}$，则$\alpha \in \mathbb{T}$
2. 箭头类型（Arrow type）若$\sigma,\tau \in \mathbb{T}$，则$(\sigma \to \tau) \in \mathbb{T}$

即 $\mathbb{T= V\ \mid\ T \to T}$ .

记法：使用字母$\alpha,\beta,…$表示$\mathbb{V}$中的类型变量，$\sigma,\tau,…$（有时也用$A,B,…$）表示一个简单类型. 最外侧的括号可以省略. 箭头是右结合的.

“项$M$有类型$\tau$”，我们引入定型陈述（statements, or typing statements），形式为$M:\tau$.

我们假设对于每个类型都有无穷的变量，且每个变量的类型都是唯一的，即若$x:\sigma$且$x:\tau$，则$\sigma \equiv \tau$.

对于lambda演算的构造方法，有：

1. 应用：若$M:\sigma \to \tau$且$N:\sigma$，则$M\ N:\tau$.
2. 抽象：若$x:\sigma$且$M:\tau$，则$\lambda x.M:\sigma \to \tau$

可定型的项（Typable term）

我们说一个项$M$可定型，如果存在类型$\sigma$使得$M:\sigma$.

Church定型与Curry定型（Church-typing and Curry-typing）

对于定型，有两种方法：

Church定型（Typing à la Church）

假设$x$有类型$\alpha \to \alpha$，且$y$有类型$(\alpha \to \alpha) \to \beta$，则$yx$有类型$\beta$. 然后$z$有类型$\beta$，且$u$有类型$\gamma$，则$\lambda zu.z$有类型$\beta \to \gamma \to \beta$. 所以，如果$(\lambda zu.z)(yx)$是允许的，则有类型$\gamma \to \beta$.

Curry定型（Typing à la Curry）

对于lambda项$M \equiv (\lambda zu.z)(yx)$，假设变量$x,y,z,u$的类型并没有给出. 我们注意到$M$是一个$\lambda zu.z$对$yx$的应用，所以$\lambda zu.z$应该有一个函数类型，比如$A \to B$，且$yx$必须有类型$A$，所以$M$有类型$B$.

$\lambda zu.z:A \to B$表明$z:A$且$\lambda u.z:B$. 对于后一个类型陈述，$B$是一个$\lambda$开头抽象的项，因此$B$具有函数类型$B\equiv (C \to D)$，且$u:C,z:D$.

而$yx$是一个应用，因此一定有$y:E \to F$且$x:E$，则$yx:F$.

我们有：

• $x:E$
• $y:E\to F$
• $z:A 且 z:D，所以A\equiv D$
• $u:C$
• $B\equiv (C \to D)$
• $yx:A 且yz:F，所以A \equiv F$

得到$(*)\ x:E,y:E\to A,z:A,u:C$.

我们可以将变量$x,y,z,u$赋予“真实”的类型，填入$(*)$式的样板，如：

• $x:\beta, y:\beta \to \alpha, z:\alpha,u:\delta, M:\delta \to \alpha$
• $x:\alpha \to \alpha,y:(\alpha \to \alpha)\to \beta,z:\beta,u:\gamma,M:\gamma \to \beta$
• $x:\alpha,y:\alpha\to \alpha \to \beta, z:\alpha \to \beta,u:\alpha \to \alpha$

我们对于绑定的变量直接给出类型，自由变量的类型称为上下文（context）.

对于项$(\lambda zu.z)(yx)$，$z,u$是绑定的，而$x,y$是自由的. 假设$z:\beta$且$u:\gamma$，我们记作$(\lambda z:\beta.\lambda u:\gamma.z)(yx)$.

对于此例的上下文，记作：

$x:\alpha \to \alpha,y:(\alpha \to \alpha) \to \beta \ \vdash\ (\lambda z:\beta.\lambda u:\gamma.z)(yx):\gamma \to \beta$.

Church的$\lambda{\to}$的派生法则

预标注类型的lambda项（Pre-typed λ-terms,$\Lambda_\mathbb{T}$）

$\Lambda_\mathbb{T}=V\mid(\Lambda_\mathbb{T}\Lambda_\mathbb{T})\mid(\lambda V:\mathbb{T}.\Lambda_\mathbb{T})$.

陈述，声明，上下文，推断（Statement, declaration, context, judgement）

1. 陈述（statement）具有形式$M:\sigma$，其中$M \in \Lambda_\mathbb{T}$且$\sigma \in \mathbb{T}$. 在陈述中，称$M$主体（subject），$\sigma$为类型.
2. 声明（declaration）是以变量为主体的陈述.
3. 上下文（context）是一个对于不同主体的声明的列表.
4. 推断（judgement）具有形式$\Gamma \ \vdash \ M:\sigma$，其中$\Gamma$是上下文，而$M:\sigma$是陈述.

我们需要判断一个推断是否是可派生的，引入派生系统（derivation system）.

前提-结论格式（premiss–conclusion format）：

$\dfrac{前提1\ 前提2\ …\ 前提n}{结论}$

由此给出Church的$\lambda{\to}$的三条派生法则，以此建立Church的$\lambda{\to}$的派生系统.

Church的$\lambda{\to}$的派生法则（Derivation rules for $\lambda{\to}$）

$(var)\qquad \Gamma\ \vdash\ x:\sigma 若x:\sigma\in \Gamma$

$(appl)\ \dfrac{\Gamma\ \vdash \ M:\sigma\to\tau\qquad \Gamma\ \vdash\ N:\sigma}{\Gamma\ \vdash\ MN:\tau}$

$(abst)\ \dfrac{\Gamma,x:\sigma\ \vdash\ M:\tau}{\Gamma \ \vdash\ \lambda x:\sigma.M:\sigma\to\tau}$

基于派生系统可标注类型的项称合法的（legal）.

合法的$\lambda{\to}$项（Legal $\lambda{\to}$-terms）

在$\lambda{\to}$中，一个预标注类型的lambda项$M$是合法的，如果存在上下文$\Gamma$和类型$\rho$使得$\Gamma \vdash M:\rho$.

类型论需要解决的几类问题

良类型性/可定型性（Well-typedness/Typability）

形如：

$?\ \vdash\ 项:\ ?$

即判断一个项是否合法，如果合法则找到一个合适的上下文和类型，否则找出它出错的地方.

一个变体是类型赋值（Type Assignment），即给出上下文，只要找出项的类型：

$上下文\ \vdash\ 项\ :\ ?$.

类型检查（Type Checking）

$上下文\ \overset{?}{\vdash}\ 项\ :\ 类型$

给出上下文、项和类型，检查是否这个项（在这个上下文中）有这个类型.

项的寻找（Term Finding/Term Construction/Inhabitation）

$上下文\ \vdash\ ?\ :\ 类型$

给定上下文和类型，寻找是否存在合适的项.

$\lambda{\to}$中的良类型性

例：项$M\equiv \lambda y:\alpha \to \beta .\lambda z:\alpha.yz$是否合法. 即找到上下文$\Gamma$和类型$\rho$，使得$\Gamma \vdash M:\rho$.

首先$\Gamma\equiv\emptyset$就可以，因为$M$中没有自由变量需要定型. 其次就是找到$\rho$：

$(n)\quad \lambda y.\alpha \to \beta.\lambda z:\alpha.yz\ :\ ?$

由三条派生法则中，只有抽象法则$(abst)$可以用，这样就变成了：

$\quad\vdots$

$(m)\quad y:\alpha \to \beta\ \vdash\ \lambda z:\alpha.yz\ :\ ?$

$(n)\quad \lambda y:\alpha\to \beta.\lambda z:\alpha.yz:\dots\qquad 对(m)用(abst)$

这样问题就变成了$(m)$中的$?$. 需要找到$\lambda z:\alpha.yz$的类型，同样是$\lambda$，重复上面的操作：

$\quad\vdots$

$(l)\quad y:\alpha \to \beta,\ z:\alpha \ \vdash\ yz\ :\ ?$

$(m)\quad y:\alpha \to \beta \ \vdash\ \lambda z:\alpha.yz\ :\ \dots \qquad对(l)用(abst)$

$(n)\quad \lambda y:\alpha\to \beta.\lambda z:\alpha.yz:\dots\qquad 对(m)用(abst)$

新的要定型的项是$yz$，是一个应用，所以只能用应用法则$(appl)$. 而$(appl)$有两个前提，所以现在有两个新目标：

$\quad\vdots$

$(k_1)\quad y:\alpha \to \beta,\ z:\alpha \ \vdash\ y\ :\ ?_1$

$\quad \vdots$

$(k_2)\quad y:\alpha \to \beta,\ z:\alpha \ \vdash\ z\ :\ ?_2$

$(l)\quad y:\alpha \to \beta,\ z:\alpha \ \vdash\ yz\ :\ \dots \qquad 对(k_1)和(k_2)用(appl)$

$(m)\quad y:\alpha \to \beta \ \vdash\ \lambda z:\alpha.yz\ :\ \dots \qquad对(l)用(abst)$

$(n)\quad \lambda y:\alpha\to \beta.\lambda z:\alpha.yz:\dots\qquad 对(m)用(abst)$

现在的目标是$y$和$z$，它们是简单的变量，因此用变量法则$(var)$就完了. 接下来对于$(l)$的项$yz$，由于$(appl)$的条件满足了就可以得到它的类型$\beta$. 接下来的项的类型也都可以这样得到.

最终得出的结论是我们找到了一个派生，说明$\lambda y:\alpha \to \beta:\alpha.yz$是合法的.

$\lambda{\to}$中的类型检查

例：$x:\alpha \to \alpha,\ y:(\alpha \to \alpha)\to \beta\ \vdash\ (\lambda z:\beta.\lambda u:\gamma.z)(yx):\gamma \to\beta$.

我们的目标是填入下面的点点点：

$\quad\vdots$

$(n)\quad x:\alpha \to \alpha,\ y:(\alpha \to \alpha)\to \beta\ \vdash\ (\lambda z:\beta.\lambda u:\gamma.z)(yx):\gamma \to\beta$

因为项$(\lambda z:\beta.\lambda u:\gamma.z)(yx):\gamma \to\beta$是一个应用项，我们使用应用法则$(appl)$.

$\quad\vdots$

$(m_1)\ x:\alpha \to \alpha,\ y:(\alpha \to \alpha)\to \beta \ \vdash\ \lambda z:\beta.\lambda u:\gamma.z\ :\ ?_1$

$\quad\vdots$

$(m_2)\ x:\alpha \to \alpha,\ y:(\alpha \to \alpha)\to \beta \ \vdash\ yx\ :\ ?_2$

$(n)\quad x:\alpha \to \alpha,\ y:(\alpha \to \alpha)\to \beta\ \vdash\ (\lambda z:\beta.\lambda u:\gamma.z)(yx):\gamma \to\beta \quad对(m_1)和(m_2)用(appl),(?)$

因为$(appl)$法则只有在对应的类型匹配上了才成立，所以最后一行还留了个$(?)$.

对于$?_2$可以用两次$(var)$法则然后$(appl)$法则解决，并且$y$和$x$的类型也匹配得上. 现在还剩：

$\quad\vdots$

$(m_1)\ x:\alpha \to \alpha,\ y:(\alpha \to \alpha)\to \beta \ \vdash\ \lambda z:\beta.\lambda u:\gamma.z\ :\ ?$

对于两个$\lambda$可以使用两次$(abst)$法则解决，就得到了完整的派生：

$(a) \quad x:\alpha \to \alpha,\ y:(\alpha \to \alpha)\to \beta,\ z:\beta,\ u:\gamma \ \vdash\ x:\alpha$
$(b) \quad x:\alpha \to \alpha,\ y:(\alpha \to \alpha)\to \beta,\ z:\beta,\ u:\gamma \ \vdash\ y:(\alpha \to \alpha)\to \beta$
$(1) \quad x:\alpha \to \alpha,\ y:(\alpha \to \alpha)\to \beta,\ z:\beta,\ u:\gamma \ \vdash\ z:\beta$

$(2)\quad x:\alpha \to \alpha,\ y:(\alpha \to \alpha)\to \beta,\ z:\beta \ \vdash\ \lambda u:\gamma.z:\gamma \to \beta \quad 对(1)用(abst)$

$(m_1)\ x:\alpha \to \alpha,\ y:(\alpha \to \alpha)\to \beta \ \vdash\ \lambda z:\beta.\lambda u:\gamma.z\ :\ \beta \to\gamma\to\beta \quad 对(2)用(abst)$

$(m_2)\ x:\alpha \to \alpha,\ y:(\alpha \to \alpha)\to \beta \ \vdash\ yx\ :\beta \quad 对(b)和(a)用(appl)$

$(n)\quad x:\alpha \to \alpha,\ y:(\alpha \to \alpha)\to \beta\ \vdash\ (\lambda z:\beta.\lambda u:\gamma.z)(yx):\gamma \to\beta \quad对(m_1)和(m_2)用(appl),(?)$

接下来只剩下检查$(n)$ 的$(appl)$ 的条件，显然满足了. 于是我们给出了这个推断的正确派生.

$\lambda{\to}$中项的寻找

在逻辑表达式中，我们有$A \to B \to A$，其中的$\to$读作“蕴含”，这个命题是一个“重言式”. 这很显然，因为：如果A，那么（如果B那么A）.

我们可以用$\lambda{\to}$形式化这个证明，把$A\to B\to A$作为一个类型，尝试找到一个在空上下文中的项：

$(n)\quad ?\ :\ A\to B\to A$

需要一个$\to$类型的项，所以首先用$(abst)$法则：

$(m)\quad x:A \ \vdash\ ?\ :\ B\to A$

$(n)\quad \dots\ :\ A\to B\to A\qquad 对(m)用(abst)$

现在仍然是一个$\to$类型的项，引入新变量$y$重复这个过程：

$(l)\quad x:A,\ y:B\ \vdash\ ?\ :\ A$

$(m)\quad x:A \ \vdash\ ?\ :\ B\to A\qquad 对(l)用(abst)$

$(n)\quad \dots\ :\ A\to B\to A\qquad 对(m)用(abst)$

现在$?$可以被$(var)$法则解决：

$(1)\quad x:A,\ y:B\ \vdash\ x\ :\ A$

$(2)\quad x:A \ \vdash\ \lambda y:B.\ x\ :\ B\to A\qquad 对(1)用(abst)$

$(3)\quad \lambda x:A.\ \lambda y:B.\ x\ :\ A\to B\to A\qquad 对(2)用(abst)$

就完成了.

我们将命题看做类型，把命题的inhabitants作为证明：

$假设x是命题A的证明，y是命题B的证明.$

$(1)\quad 那么x（仍）是A的证明.$

$(2)\quad y到x的函数是一个由B到A的证明，即\lambda y:B.\ x证明了B\to A这个蕴含.$

$(3)\quad 所以，\lambda x:A.\lambda y:B\ x证明了A\to B\to A.$

这一过程称PAT-解释（PAT-interpretation），“PAT”既指“命题作为类型”（propositions-as-types），又指“证明作为项”（proofs-as-term）.

$\lambda{\to}$的性质

定义域，子上下文，置换，投影（Domain, $\rm dom$, subcontext, $\subseteq$, permutation, projection, $\upharpoonright$）

1. 如果$\Gamma \equiv x_1 : \sigma_1,\dots,x_n:\sigma_n$，则$\Gamma$的定义域（domain）或$\rm dom(\Gamma)$为列表$(x_1,\dots,x_n)$.
2. 上下文$\Gamma’$是$\Gamma$ 的子上下文（subcontext），或$\Gamma’ \subseteq \Gamma$，如果$\Gamma’$中所有的声明也在$\Gamma$中以相同次序出现.
3. 上下文$\Gamma’$是上下文$\Gamma$的一个置换（permutation），如果所有在$\Gamma’$中的声明也在$\Gamma$中出现，反之亦然.
4. 如果$\Gamma$是一个上下文，$\Phi$是一个变量的集合，则$\Gamma$在$\Phi$上的投影（projection）或$\Gamma \upharpoonright\Phi$，是$\Gamma$的一个子上下文$\Gamma’$，满足${\rm dom}(\Gamma’) = {\rm dom}(\Gamma)\cap\Phi$.

自由变量引理 (Free Variables Lemma)

若$\Gamma \vdash L:\sigma$，则$FV(L)\subseteq {\rm dom}(\Gamma)$.

这说明，如果$L$有类型，则所有在$L$中出现的自由变量$x$都有类型，且作为一条声明$x:\sigma$记录在上下文$\Gamma$中.

引理 (Thinning, Condensing, Permutation)

1. （Thinning）令$\Gamma’$与$\Gamma’’$是上下文，使得$\Gamma’ \subseteq \Gamma’’$. 若$\Gamma’ \vdash M:\sigma$则$\Gamma’’ \vdash M:\sigma$.
2. （Condensing）若$\Gamma \vdash M:\sigma$，则$\Gamma \upharpoonright FV(M) \vdash M:\sigma$.
3. （Permutation）若$\Gamma \vdash M:\sigma$，且$\Gamma’$是$\Gamma$的一个permutation，则$\Gamma’$也是上下文，且$\Gamma’ \vdash M:\sigma$.

• Thinning指一个上下文加上更多声明的扩展，即与子上下文相反.
• Condensing指仅需要保留$\Gamma$中关于$FV(M)$的部分就可以得到$M$的类型.
• Permutation指上下文的顺序并不重要，上下文中的声明并没有相互依赖关系.

因此在$\lambda{\to}$中，也可以用集合代替列表定义上下文，集合上下文称基（bases）. 我们用列表因为对于更复杂的系统还会有依赖的声明，此时顺序就很重要.

生成引理（Generation Lemma）

1. 若$\Gamma \vdash x:\sigma$，则$x:\sigma \in \Gamma$.
2. 若$\Gamma \vdash MN:\tau$，则存在类型$\sigma$使得$\Gamma \vdash M:\sigma \to \tau$且$\Gamma \vdash N:\sigma$.
3. 若$\Gamma\vdash \lambda x:\sigma.M:\rho$，则存在$\tau$使得$\Gamma,\ x:\sigma\vdash M:\tau$且$\rho \equiv \sigma \to \tau$.

就对应了三条派生法则.

子项引理（Subterm Lemma）

若$M$是合法的，则$M$的所有子项都是合法的.

类型唯一性（Uniqueness of Types）

设$\Gamma \vdash M:\sigma$且$\Gamma \vdash M : \tau$，则$\sigma \equiv \tau$.

可判定性定理

(Decidability of Well-typedness, Type Assignment, TypeChecking and Term Finding)

在$\lambda{\to}$中，以下问题都是可判定的：

1. Well-typedness（1a）Type Assignment
2. Type Checking
3. Term Finding

归约和$\lambda{\to}$

对于$\lambda{\to}$中的beta归约，我们对代换的定义进行以下调整：

3. $(\lambda y:\sigma.P)[x:=N]\equiv \lambda z:\sigma.(P^{y \to z}[x:=N])$，若$\lambda z:\sigma.P^{y \to z}$是$\lambda y:\sigma.P$的alpha变形使得$z \notin FV(N)$.

此时我们有：

代换引理（Substitution Lemma）

设$\Gamma’,\ x:\sigma,\ \Gamma’’ \vdash M:\tau$且$\Gamma’ \vdash N:\sigma$，则$\Gamma’,\Gamma’’ \vdash M[x:=N]:\tau$.

对$\mathbb{\Lambda_T}$的单步beta归约（$\to_\beta$, for $\mathbb{\Lambda_T}$）

1. (Basis) $(\lambda x:\sigma.M)N\to_\beta M[x:=N]$
2. (Compatibility)同第一章定义

Church–Rosser定理

在$\lambda{\to}$上仍成立

主体归约引理（Subject Reduction）

若$\Gamma \vdash L : \rho$且若$L \twoheadrightarrow_\beta L’$，则$\Gamma \vdash L’:\rho$.

即beta归约不影响类型性，且对项进行beta归约不影响项的类型.

强标准定理/终止定理（Strong Normalisation Theorem/Termination Theorem）

所有合法的项$M$都是强标准化的.

结论

1. $\lambda{\to}$中没有自应用（self-application）
2. Beta范式的存在性得以保证
3. 不是所有合法的项都有不动点