「Learn LambdaCalculus」#0

前言

前段时间，GZTime也跟我聊过一些关于lambda演算的东西
学Haskell的时候也总是能听说这个东西
看起来挺有意思，来学学_(:з」∠)_

那我也引用GZTime引用的知乎同学的一句话：

在介绍λ演算之前，我们需要放空一下我们的大脑，忘掉C语言，忘掉冯·诺伊曼机，忘掉图灵机，甚至要忘掉0和1，加和减。我们来到一个只有符号的世界。在这个新的世界里，只需要几条简单的定义和规则，便可以构造出与图灵机完全等价的计算模型，即它是图灵完全（Turing Complete）的。和图灵机一样，这个计算模型可以解决任何一个可以机械计算的问题；与图灵机倾向于硬件实现不同，它更倾向于逻辑的推理。它就是λ演算（Lambda演算）。

lambda term

一个合法的lambda表达式又被称为lambda项（lambda term），以下三个规律归纳性地定义了一个合法的lambda项：

• Variable：一个变量 x 本身也是一个合法的lambda项
• Abstraction：如果 M 是一个合法的lambda项，x 是一个变量，那么 (λx.M) 也是一个合法的lambda项（这相当于定义了一个 x -> M 的函数）
• Application：如果 M 和 N 都是合法lambda项，那么 (M N) 也是一个合法lambda项

lambda表达式的组成有变量、抽象符号λ和一个点.、括号

所有lambda项构成$\Lambda$空间，通过上述合法lambda项的定义，$\Lambda$空间的正式定义是：

• 如果$x$是一个变量，那么$x\in\Lambda$
• 如果$x$是一个变量且$M\in\Lambda$，那么$(\lambda x.M)\in\Lambda$
• 如果$M, N\in\Lambda$，那么$(M\ N)\in\Lambda$

notation

为了使lambda表达式的记法更清晰，可以有以下简化：

• 一个lambda项最外侧的括号可以省略。比如 (M N) 可以写成 M N
• 应用是左结合的。比如 M N P 表示的实际是 ((M N) P)
  这和Haskell中函数左结合是一样的
• 抽象是尽可能向右延伸的。比如 λx.M N 实际上表示的是 λx.(M N) 而不是 (λ. M) N
  这和Haskell中lambda表达式向右一直延伸是一致的，因此一般要为lambda表达式加上括号
• 嵌套的多个lambda表达式可以缩写成类似多元函数的样子。比如 λx.λy.λz.M 就可以缩写成 λxyz.M

Free & bound variables

在一个lambda表达式中，也有自由变量（free variables）和约束变量（bound variables）的概念。

在lambda项 λx.M 中，λx被称为binder，它将输入的x与M中的变量x绑定在一起，这时x就是约束变量，而其它的所有变量都是自由变量。

 比如在表达式 λx.x+y 中，x就是约束变量，y是自由变量。

对于一个lambda项M的自由变量构成的集合FV(M)，也有一些规律需要满足：

• 如果 x 是一个变量，那么 FV(x) = {x}
• FV(λx.M) = FV(M) \ {x} （M中除去x之外的变量都是自由变量）
• FV(M N) = FV(M) ∪ FV(N) （M应用在N上得到的lambda项的自由变量是MN两个lambda项的自由变量的并集）

Substitution

lambda项也有一种记法叫做替换（substitution），记法 t[x:=r] 表示将lambda项t中的自由变量x都替换成r。它满足以下规律：

• x[x:=r]=r （一个变量就是自由变量，将其替换成r就变为r）
• y[x:=r]=y if x!=y （如果x和y不相等，那么）