Table of contents

• 前言
• 前置知识
  • 元语言和形式语言
  • 相继演算
  • 柯里化
• 简单类型
  • 无类型 $\lambda$ 演算
    • $\alpha$-转换
    • 规约和暨约形式
    • 邱奇编码
  • 简单类型 $\lambda$ 演算
    • 类型论和一个类型论

前言

是个人学习笔记，会有很多自己的理解和想法，可能有不准确甚至错误的地方。如有发现可以来嘲讽笔者！

由于类型论相关的术语翻译混乱或者难以翻译，有些术语会附上英文原文或直接使用英文。

尝试把笔记写成一篇浅显易懂的入门读物，因此可能很多在诸位认为不重要的地方会花很多笔墨详细解释，以帮助新人理解。

前置知识

元语言和形式语言

……

相继演算

……

柯里化

……？

简单类型

无类型 $\lambda$ 演算

为什么会产生类型？

为了回答这个问题，我们现看看没有类型会发生什么。接下来我们会介绍无类型的 $\lambda$ 演算。说它没有类型也不准确，我们也可以看作它所有的东西共用一个类型。

$\lambda$ 演算中一个项（term）定义为 $term := x | t_1t_2 | \lambda x.t$，这是说一个项要么是一个单独的变量 $x$，要么是两个项的拼接 $t_1 t_2$，要么是形如 $\lambda x.t$ 的形式。

拼接两个项被称为应用（application），它是左结合的，也就是说 $t_1\ t_2\ t_3\cdots t_n$ 代表 $(\cdots (t_1\ t_2)t_3 \cdots )t_n$

$\lambda x.t$ 这种形式被称为抽象（abstrcation）,其中 $x$ 是一个变量，$t$ 是一个项。抽象和我们中学时期理解的函数很像，比如我们定义一个函数 $f(x) = x^2$，我们传入一个参数 $y$ 得到的 $f(y) = y^2$ 其实就是把 $f(x)$ 中的所有 $x$ 换成了 $y$；而 $(\lambda x.t) y$，也就是把 $y$ 应用到这个项上，代表把项 $t$ 中所有 $x$ 都替换成 $y$。注意我们一般规定抽象的优先级比应用要高，也就是 $\lambda x.t_1t_2$ 说的是 $\lambda x.(t_1t_2)$ 而不是 $(\lambda x.t_1)t_2$。

我们把 $M$ 中的 $x$ 全部替换成 $y$ 的结果写成 $M[x \mapsto y]$。

$\alpha$-转换

我们刚刚知道了 $\lambda$ 演算的基本规则，那么请思考一个问题：$(\lambda y.\lambda x.y)xz$ 该怎么算？最后得到的是 $x$ 还是 $z$？换言之我们第一步应用得到的 $(\lambda x.x)z$ 中的两个 $x$ 是不是同一个 $x$？

其实如果我们换一个变量名 $(\lambda y.\lambda t.y)xz$ 就很清晰了。这个项毫无疑问等于 $z$，而我们直觉上认为，$\lambda t.y$ 和 $\lambda x.y$ 是等价的东西，就像 $f(x) = \sin x$ 和 $f(y) = \sin y$ 没什么区别一样。事实上在 $\lambda$ 演算中也是这样规定的。我们接下来形式化地描述一下这种”重命名“的过程。

在一个项 $M$ 中，只要不是在 $\lambda x.$ 的位置使用了一个变量 $x$，我们就称这个变量 $x$ 在项 $M$ 中出现（occurence）了。对于一个项 $\lambda x.M$，如果 $M$ 这个项中出现了 $x$，那么这个项中的 $x$ 就是一个绑定变量（bounded variable），否则是一个自由变量（bounded variable）。我们之前说的 $t[x \mapsto y]$ 严格定义是将 $t$ 中所有自由的 $x$ 换成 $y$。

同时，我们认为将 $\lambda x.M$ 中的 $x$ 和 $M$ 共同换成一个 $M$ 中自由的变量，变换后的项和原来是等价的。这就是 $\alpha$-转换（$\alpha$-conversion）。显然地，我们可以把一个项的所有变量都转化为两两不同的变量，这样就不会出现我们上面草歧义。

而之所以我们出现了上面的歧义，是因为我们采用了字符串来代指数学对象，因此我们即使用着同样的名字 $x$，两个 $x$ 想表达的意思却是不一样的，就会造成一些混淆。

规约和暨约形式

归约 (reduction) 主要描述了一个项怎么化简, 或者说计算。而暨约形式（normal form）则是经过化简得到的所谓“最简形式”。在基础的 $\lambda$ 演算中主要有两条规则：

$$\frac{}{(\lambda x.M)y \equiv M[x \mapsto y]} \beta rule$$

这条规则告诉我们如何使用一个函数，正向使用这个规则叫做 $\beta$-规约。

$$\frac{}{(\lambda x.f x) \equiv f} \eta rule$$

正向使用这个规则叫做 $\eta$-展开，反向使用则叫 $\eta$-规约。

这个规则看起来没什么必要，但是它其实向我们展示了函数的外延性：因为 $f$ 和 $\lambda x.f x$ 无论应用上什么参数都是相同的，因此这两个函数也是等价的。

当一个项没法继续使用 $beta$-规约，我们就称这个项是 $\beta$-范式。

当一个项没法使用上述任意一条规则，且被完全应用（也就是每个抽象都有一个对应的应用）我们就称这个项是 $\beta \eta$-既约的, 简称既约的 (normalized)。

这时我们就会发现无类型 $\lambda$ 演算的第一个毒点：不是所有的项都能化成 $\beta$ 范式，或者说 $\lambda$ 演算并不是停机的。比如我们考虑以下的项：

$$\begin{aligned} & (\lambda x.x x) (\lambda x.x x) \\ =& (x x) [x \mapsto \lambda x.x x] \\ =& (\lambda x.x x) (\lambda x.x x) \\ \end{aligned}$$

我们发现无论如何这个函数都没法被完全规约，它最后总会回到最开始的形式。

邱奇编码

邱奇编码使得 $\lambda$ 演算具有了更多实用意义。通过邱奇编码，我们能将很多东西，比如自然数、布尔值、有序对等等，映射到一个 $\lambda$ 中的项。

如邱奇数能让我们用 $\lambda$ 演算编码自然数。邱奇编码将自然数 $n$，表示为任意函数 $f$ 映射到它自身的 $n$ 重函数复合的一个函数，换言之 $n$ 是一个接受一个函数 $f$ 和一个参数 $x$ 的函数，返回的是把 $f$ 应用到 $x$ 上 $n$ 次的结果。直观理解一下： $$\begin{aligned} 0\ f\ x &= x &= \lambda f.\lambda x.x \\ 1\ f\ x &= f\ x &= \lambda f.\lambda x.f\ x \\ 2\ f\ x &= f\ (f\ x) &= \lambda f.\lambda x.f\ (f\ x) \\ &\cdots& \\ n\ f\ x &= f^n\ x &= \lambda f.\lambda x.f^n\ x \end{aligned}$$

类似地我们能定义加法：$plus := λm.λn.λf.λx. m\ f(n\ f\ x)$，这是我们由定义可以得来的。

类似地我们还可以做很多有趣的东西。但是对类型论这不太重要。有时间可能会回来补。

重要的是，我们不得不开始考虑 $plus\ n\ \lambda x.x$ 或者类似东西的意义——它的确是一个合法的 $\lambda$ 项，我们也可以用规则去化简它，但是它和意义很混乱—— $n$ 加上一个函数是什么？我们没法解释。这就是无类型 $\lambda$ 演算的另一个弊端：虽然我们能表示不同“种类”的东西，但是我们没有手段来确保函数或是其它东西按照我们预想的方式使用它——毕竟不论什么含义最终都是 $\lambda$项，无论多么胡闹的用法都是合法的。这就需要我们用类型来规范函数的行为。

简单类型 $\lambda$ 演算

类型论和一个类型论

首先