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

---

对于函数的抽象，有两个构造方法和一个计算规则：

抽象（Abstraction）

由一个表达式$M$和一个变量$x$ 可以构造表达式$\lambda x.M$，称为$M$上$x$的抽象（abstraction of x over M）

应用（Application）

由表达式$M$和$N$可以构造表达式$M\ N$，称为$M$对$N$的应用（application of M to N）

Beta化简（β-reduction）

形如$(\lambda x.M)N$的表达式可以被改写成$M[x:=N]$，意思是表达式中的$M$中的每个$x$换成$N$，这一过程称为由$(\lambda x.M)N$到$M[x:=N]$的Beta化简（β-reduction）.

注意“应用”仅是构造另一个lambda项的过程，而真正得到结果的过程则是“Beta化简”.

以下是严格定义

Lambda项（Lambda-term）

设$\Lambda$为所有Lambda项的集合，我们有一个变量的无限集 $V$，$V=\lbrace x,y,z,…\rbrace$

1. （变量Variable）若$u \in V$，则$u \in \Lambda$
2. （应用Application）若$M,N \in \Lambda$，则$(M\ N)\in \Lambda$
3. （抽象Abstraction）若$u \in V$且$M \in \Lambda$，则$(\lambda u.\ M)\in \Lambda$

我们使用小写字母表示$V$中的变量，用大写的字母表示$\Lambda$中的项.

如果两个lambda项$M$和$N$相同（syntactical identity），记为$M \equiv N$.

子项（Subterm）

设lambda项$M$的子项Multiset为${\rm Sub}(M)$

1. （Basis）$\forall x \in V, {\rm Sub}(x)=\lbrace x\rbrace $
2. （应用）${\rm Sub}((M\ N))={\rm Sub}(M)\cup{\rm Sub}(N)\cup\lbrace (M\ N)\rbrace $
3. （抽象）${\rm Sub}((\lambda x.M))={\rm Sub}(M)\cup\lbrace \lambda x.M\rbrace $

若$L \in {\rm Sub}(M)$，我们称$L$为$M$的子项.

子项关系有：

1. （自反性）对所有lambda项$M$，有$M \in {\rm Sub}(M)$
2. （传递性）若$L \in {\rm Sub}(M)$且$M \in {\rm Sub}(N)$，则$L \in {\rm Sub}(N)$

若将lambda项写成它的树形表示，我们可以直观的发现子项就是对应的子树.

若$L$是$M$的子项，且$L \not \equiv M$，称$L$是$M$的真子项（proper subterm）.

另外为了减少括号的使用，定义结合性和优先级：

1. 应用是左结合的，$M\ N\ L$为$(M(N\ L))$
2. 应用的优先级比抽象高，$\lambda x.M\ N$为$\lambda x.(M\ N)$
3. 连续的抽象$\lambda x.(\lambda y.M)$可以简写为，$\lambda xy.M$

这些定义都与Haskell中的一致，所以挺符合直觉（？）

自由和绑定变量

lambda项中出现的变量可以分为三类：自由的（free）、被绑定的（bound）和绑定的（binding）.

其中，紧接着在$\lambda$后出现的，为绑定的变量；在项$\lambda x.M$中，$M$中的$x$即被绑定的变量；自由变量定义为：

设$FV$为一个lambda项中自由变量的集合，则

1. （变量）$FV(x)=\lbrace x\rbrace $
2. （应用）$FV(M\ N)=FV(M)\cup FV(N)$
3. （抽象）$FV(\lambda x.M)=FV(M)-\lbrace x\rbrace $

如果$FV(M)=\emptyset$，则称$M$为闭lambda项（Closed λ-term），也称组合子（combinator）. 所有闭lambda项的集合记为$\Lambda^0$.

Alpha替换（Alpha conversion）

记$M^{x \rightarrow y}$为把$M$中所有自由变量$x$换成$y$.

1. 重命名关系（renaming），符号为$=_\alpha$，定义为：$\lambda x.M =_\alpha \lambda y.M^{x \rightarrow y}$，其中满足$y \notin FV(M)$且$y$不是$M$中的binding变量.
2. 若$M =_\alpha N$则$M\ L=_\alpha N\ L$，$L\ M=_\alpha L\ N$
3. 有自反性、对称性、传递性. Alpha替换/重命名关系是一个等价关系.

若$M =_\alpha N$，则称 $M$与$N$Alpha可替换（α-convertible）或Alpha等价（α-equivalent）. $M$为$N$的Alpha变形（α-variant）.

代换（Substitution）

将$M$中所有自由变量$x$ 代换为$N$，记为$M[x:=N]$，定义为：

1. a) $x[x:=N] \equiv N$ b) $y[x:=N] \equiv y$ ，若$x \not \equiv y$
2. $(PQ)[x:=N] \equiv (P[x:=N])(Q[x:=N])$
3. $(\lambda y.P)[x:=N] \equiv \lambda z.(P^{y \rightarrow z}[x:=N])$，若$\lambda z.P^{y \rightarrow z}$是$\lambda y.P$的Alpha变形，即$z \notin FV(N)$.

注意含$[x:=N]$的项并不在lambda项的构造方法中，因此并不是lambda项，而是作为一种lambda项的“元表记”. 只有将所有$[x:=N]$全部消解了才能得到一个真的lambda项.

(1)就是对于$x$字面意义的代换. (2)普通地将替换推到应用的两边.

(3)的目的是为了防止变量名的冲突，如果$N$中有$y$的自由变量会被原本不应该的$(\lambda y.P)$的$y$绑定。因此需要引入一个不属于$N$的自由变量的$z$，替换原来的$y$. 如果$y \notin FV(N)$，则可以取$z \equiv y$，此时$(\lambda y.P[x:=N]) \equiv \lambda y.(P[x:=N])$.

引入顺序代换（sequential substitution），$M[x:=N][y:=L]$.

引理：

令$x \not \equiv y$，设$x \notin FV(L)$，则$M[x:=N][y:=L]\equiv M[y:=L][x:=N[y:=L]]$

Lambda项模Alpha等价（Lambda-terms modulo α-equivalence）

引理：

令$M_1 =_\alpha M_2$且$N_1 =_\alpha N_2$（？原文为$M_1=_\alpha N_1 \ and\ M_2 =_\alpha N_2 $），则：

1. $M_1N_1 =_\alpha M_2N_2$
2. $\lambda x.M_1 =_\alpha \lambda x.M_2$
3. $M_1[x:=N_1] =_\alpha M_2[x:=N_2]$

即lambda项构造上保持Alpha等价. 因此，我们将一个Alpha等价的等价类看作同一个抽象lambda项，将Alpha等价也视为相同，记$=_\alpha$为$\equiv$，称lambda项上模Alpha等价（λ-terms modulo α-equivalence）.

Barendregt convention：我们选取绑定的变量时应使每个都不一样.

Beta化简（Beta reduction）

单步Beta化简（One-stepβ-reduction， $\rightarrow_\beta$）

1. (Basis) $(\lambda x.M)N \rightarrow_\beta M[x:=N]$
2. (Compatibility)若$M \rightarrow_\beta N$，则$ML\rightarrow_\beta NL,LM\rightarrow_\beta LN$且$\lambda x.M \rightarrow_\beta \lambda x.N$

其中左侧的称可化简式redex（reducible expression），右侧称（redex的）合同（contractum）.

Beta化简（零步或多步，$\twoheadrightarrow_\beta$）

$M \twoheadrightarrow_\beta N$如果存在$n \geq 0$且存在项$M_0$到$M_n$使得$M_0 \equiv M,M_n \equiv N$，且任取$0 \leq i \lt n$有$M_i \rightarrow_\beta M_{i+1}$

即若$M \twoheadrightarrow_\beta N$，则存在一个从$M$开始到$N$的单步Beta化简的链：
$M \equiv M_0 \rightarrow_\beta M_1 \rightarrow_\beta M_2 \rightarrow_\beta … \rightarrow_\beta M_{n-1} \rightarrow_\beta M_n \equiv N $
引理：

1. $\twoheadrightarrow_\beta$是$\rightarrow_\beta$的推广，若$M \rightarrow_\beta N$则$M \twoheadrightarrow_\beta N$
2. $\twoheadrightarrow_\beta$有自反性和传递性

这个零步或多步的Beta化简的推广称为Beta替换（β-conversion），记作$=_\beta$.

$M =_\beta N$

（读作“ $M与N$ Beta可替换（β-convertible）”或“Beta相等（β-equal）”）若存在$n \geq 0$且存在项$M_0$到$M_n$，使得$M_0 \equiv M,M_n \equiv N$且任取$0 \leq i \lt n$有$M_i \rightarrow_\beta M_{i+1}或M_{i+1} \rightarrow_\beta M_i$.

注意每一对$M_i$与$M_{i+1}$应该具有单步关系$\rightarrow_\beta$，但不一定要是从左到右的.

引理：

1. $=_\beta$是$\twoheadrightarrow_\beta$在两个方向上的推广，若$M \twoheadrightarrow_\beta N$或$N \twoheadrightarrow_\beta M$，则$M =_\beta N$
2. $=_\beta$是等价关系，有自反、对称、传递性

范式与汇合（Normal forms and confluence）

Beta范式;可Beta标准化（β-normal form;β-nf;β-normalising）

1. $M$是Beta范式，若$M$没有任何redex
2. $M$有Beta范式，或可Beta标准化，若存在$N$是Beta范式使得$M =_\beta N$. 这样的$N$称为$M$的Beta范式.

一个lambda项的Beta范式可以看做它的输出（计算结果）.

引理：当$M$是Beta范式，则$M \twoheadrightarrow_\beta N$蕴含$M \equiv N$.

化简路径（Reduction path）

一个从$M$开始的有穷化简路径是一个项的有穷序列$N_0,N_1,…,N_n$，使得$N_0 \equiv M$且对任取$0 \leq i \lt n$有$N_i \rightarrow_\beta N_{i+1}$.

一个从$M$开始的无穷化简路径是一个项的无穷序列$N_0,N_1,…$，使得$N_0 \equiv M$且对任取$i \in \mathbb{N}$有$N_i \rightarrow_\beta N_{i+1}$.

弱标准化，强标准化（Weak normalisation, strong normalisation）

1. $M$可弱标准化，若存在Beta范式$N$使得$M \twoheadrightarrow_\beta N$.
2. $M$可强标准化，若不存在从$M$开始的无穷化简路径.

如果$M$可强标准化，则任意化简路径都可以扩展到一个Beta范式为止；因此，可强标准化的也是可弱标准化.

Church–Rosser定理;CR定理;汇合定理（Church–Rosser; CR; Confluence）

设对于lambda项$M$，有$M \twoheadrightarrow_\beta N_1$且$M \twoheadrightarrow_\beta N_2$，则存在lambda项$N_3$使得$N_1 \twoheadrightarrow_\beta N_3$且$N_2 \twoheadrightarrow_\beta N_3$.

这意味着一个演算结果（如果存在）与演算过程的顺序无关.

推论：设$M =_\beta N$则存在$L$使得$M \twoheadrightarrow_\beta L$且$N \twoheadrightarrow_\beta L$.

1. 若$M$有Beta范式$N$，则$M \twoheadrightarrow_\beta N$
2. 一个lambda项最多只有一个Beta范式

不动点定理（Fixed Point Theorem）

定理： $\forall L \in \Lambda$存在$M \in \Lambda$使得$LM =_\beta M$.

证：取$M:=(\lambda x.L(xx))(\lambda x.L(xx))$，有
$$
M \equiv (\lambda x.L(xx))(\lambda x.L(xx)) \
\rightarrow_\beta L(,(\lambda x.L(xx))(\lambda x.L(xx)),) \
\equiv LM
$$

即$LM =_\beta M$.

我们定义不动点组合子（fixed point combinator）：

$Y \equiv \lambda y.(\lambda x.y(xx))(\lambda x.y(xx))$.

对于任意的lambda项$L$，都有$YL$是$L$的一个不动点，因为$L(YL)=_\beta YL$.