\newcommand\norm[1]{\left\lVert#1\right\rVert} \newcommand\abs[1]{\left\lvert#1\right\rvert} $\lambda$-calculus

Background

首先这是一种编程语言，在1930s被Alonzo Church和Stephen Cole Kleene发明（两位都是听说过的明星人物）

还是一种计算模型，在1937年被Alan Turing证明其和图灵机的表达能力等价（这位更是重量级）

$\lambda$ 演算是函数式编程的基础，同时它简单的特点也使得很适合用于研究PL的各个领域（回忆IDFS中的$\lambda$ 表达式作为transfer function）

PL的东西有点乱，大家的说法和记号也都不一样，这里选择了可能算是比较好理解又简洁的一种

Syntax

定义 $\mathcal V$ 是无穷变量集合，$\Sigma=\mathcal V\cup\left{(,),\lambda,.\right}$ 为字符集，那么定义一个term为$\Sigma$上满足的某些约束的有穷串

$\lambda$ calculus term组成的集合 $\Lambda\subseteq \Sigma^*$ 定义为满足如下条件的最小集合：

1. 若 $x\in\mathcal V$，那么 $x\in\Lambda$

2. 若 $M,N\in\Lambda$，那么 $(MN)\in\Lambda$，此时称 $N$ 是parameter

3. 若 $x\in\mathcal V$ 且 $M\in\Lambda$，那么 $(\lambda x.M)\in\Lambda$，此时称 $M$ 为这个term的body

上面三种形式分别叫做variable、application、$\lambda$ abstraction(function)

为了简略（这也太简略了），有一些约定俗成的优先级和结合律：

1. 最外层括号可以省略不写，例如 $(\lambda x.x^2)=\lambda x.x^2$

2. Application形式是左结合的，即 $f\;x\;y\;z=((f\;x)\;y)\;z$

3. 一个$\lambda$的约束范围(scope)向右延伸，body的范围尽可能长。例如 $\lambda x. x+y=\lambda x.(x+y)\neq(\lambda x. x)+y$

4. 多个$\lambda$ 可以写在一起。例如 $\lambda x.\lambda y.\lambda z.=\lambda xyz.$

Semantics

Bound & Free Variables

对于一个形如 $\lambda x.N$ 的term，我们就说 $N$ 中出现的 $x$ 都被绑定(binding)到了 $\lambda x.$ 上，并把 $\lambda x.$ 叫做binder

注意绑定是可以嵌套的，例如 $\lambda x. (\lambda f.\lambda x.f\; x)+x$，最里面的 $x$ 被绑定到了第二个 $\lambda x.$，而最后一个 $x$ 则被绑定到了第一个 $\lambda x.$ 这个规则和C的作用域是很相似的

如果一个变量没有被绑定，就被称为自由变量(free variables)

一个bound variable是可以被换名字而不改变term的含义的，类似于C function中形参的名字其实是任意的（但仍然有限制，后面会说）。而free variable则不能随意换名字。因此我们主要关注一个term $M$ 中具体的free variables有哪些，用 $FV(M)$ 这个记号来表示

容易有如下规则：

1. $FV(x)=\left{\;x\;\right},\; x\in\mathcal V$

2. $FV(\lambda x.M)=FV(M)-\left{\;x\;\right}$

3. $FV(M N)=FV(M)\cup FV(N)$

也就是结构归纳

Substitution

这里的substitution和直接替换是有区别的，注意我们substitute的必须是free variable

我们用 $M[x/y]$ 或者 $M\left{x/y\right}$、$M[y:=x]$ 来表示用 $x$ 替换掉term $M$ 中的 $y$ 的结果，并把一次substitution记作 $M\rightarrow M[x/y]$

考虑如下C代码

int x=1;

int y=2;


int foo(int z) {
return x + y + z;
}

这里第5行中，x,y是free variable，z被绑定到形参int z

前面说到对函数的形参可以任意换名但是有条件。考虑以下三种情况：

1. 作替换$[x/z]$，这时候第5行变为return x + y + x;，且这里的两个x都被绑定到形参int x上（形参也被替换了），含义和原文显然是不同的

2. 作替换$[u/z]$，这时候u从未出现过（称为fresh variable），这个替换就没有任何问题

3. 作替换$[z/x]$，这时候x从free variable变成了bound variable，含义也发生了变化

基于如上考虑，我们给出substitution的递归定义：

1. $x[N/x]\overset{\text{def} } =N$

2. $y[N/x]\overset{\text{def} }=y$

3. $(M N)[P/x]=(M[P/x])(N[P/x])$

4. $\lambda x.M[N/x]=\lambda x.M$

5. 若 $y\not\in FV(N)$，那么 $(\lambda y.M)[N/x]=\lambda y.(M[N/x])$

6. 若 $y\in FV(N)$，那么 $(\lambda y.M)[N/x]=\lambda z.(M[z/y][N/x])$

1234都好理解，主要说说56

5的意思是如果 $[N/x]$ 不会引入新的 与当前形参重名的free variable，那么就直接换

6的意思是如果非要换，那么就得先把 $M$ 中被绑定到当前 $\lambda y.$ 上的 $y$ 都换成一个fresh variable $z$，此时就规约成5的情况了。最开始我以为也可以先换掉 $N$ 中的 $y$，但是注意free variable的含义，如果换掉了的话语义就变了。

$\alpha$-conversion

也叫$\alpha$-renaming，意思是我们把形如 $\lambda x. M$ 这样的term的body中与binder同名的变量连同binder一起改名字（改成一个从未出现过的变量）得到的term和原来等价。这样的等价关系叫做$\alpha$-equivalence、$\alpha$-congruence。

$\beta$-reduction

讲的是如何reduce一个term。递归定义如下：

1. $(\lambda x. M)N\rightarrow M[N/x]$，这就是基本的$\beta$-reduction

2. 如果 $M\rightarrow M’$，那么 $\lambda x.M\rightarrow\lambda x.M’$

3. 如果 $M\rightarrow M’$，那么 $M N\rightarrow M’ N$，$N M\rightarrow N M’$

$\beta$-reduction是满足上述条件的最小二元关系，显然是自反、传递的

再定义 $\overset*\rightarrow$ 是 $\beta$-reduction的自反传递闭包，这个在后面会用来刻画confluence性质

$\beta$-redex 和 $\beta$-normal form

引入这俩的意图是为了判断reduction何时停止

$\beta$-redex=$\beta$-reduction expression，意思是形如 $(\lambda x.M)N$ 这样的term。这样的形式仍然可以根据$\beta$-reduction rule来进一步化简

$\beta$-normal form指的是不含$\beta$-redex的项，注意到所有的reduction都是基于$\beta$-reduction定义的，不含$\beta$-redex意味着不能再reduce。如果我们把reduction看成映射，那么就可以认为是到达了一个reduction操作下的不动点

$\eta$-reduction

这个主要是利用了函数的外延性等价。意思是说，如果两个函数对于相同的输入有相同的输出，那么它们就可以互相替换

一个例子也是从sicp中来的。假如我们要构造有理分数这一数据类型，并打算用pair来构造，那么可以写成如下形式：

(define (make-rat a b) (cons a b))

也可以这么写：

(define make-rat cons)

具体到$\lambda$-calculus就是：

若 $f=g$，那么 $\lambda x. f\; x=\lambda x.g\; x$

Confluence

Church-Rosser Confluence Theorem：

对于任意的term $M$，若存在两个不同的reduction序列使得 $M\overset\rightarrow A$，$M\overset\rightarrow B$，那么就必然存在一个term $N$ 使得 $A\overset\rightarrow N$ 且 $B\overset\rightarrow N$。注意$A$、$B$、$N$都有可能相等

推论：在$\alpha$-equivalence下，每个term如果存在$\beta$-normal form，那么这个形式是唯一的

反证即可，如果存在两个那么就违反了上述定理。

需要注意的是，这里并没有说“任意推导序列都能得到normal form”，只是说

1. 如果从同一个term开始推导，那么两个推导序列中将会存在一个公共项（不一定是normal form）

2. 如果一个term开始推导能得到一个normal form，那么这个形式在$\alpha$-equivalence意义下唯一

Reduction Strategies

回忆scheme求值的正则序和应用序（即先代换形参还是先对实参求值）策略，正好对应了$\lambda$-calculus的不同reduction”路径”，也就是策略。

实际上就是取 $\rightarrow_\beta$ 这个二元关系的一个子集，在牺牲一些推导能力的前提下使每步推导确定下来

之所以会出现策略的不同，是因为一个term可能存在多个$\beta$-redex，每一步的选取就造成了化简序列的差异。而虽然我们知道normal form唯一，但并不是所有的推导序列都能终止，也并不是所有的term都有normal form。

一个比较好玩的例子就是 $(\lambda x.x\; x)(\lambda x.x\; x)$，这就是没有normal form的term

利用上面的例子可以构造出如下式子 $(\lambda u.\lambda v.v)((\lambda x.x\; x)(\lambda x.x\; x))$，它就存在一个无法终止的推导序列

Full $\beta$-reduction

每次从所有可以reduce的项中挑一个。很显然这是单步非确定性的。

Normal-order reduction

每次选择最左、最外的redex

有定理：Normal-order reduction一定能找到normal form（如果存在的话）

Applicative-order reduction

每次选择最左、最内的redex

Call by Name reduction

规则与Normal相同，唯一的额外要求是不能对function body化简

Call by Value reduction

一个abstraction term能被化简，当且仅当它apply到了一个value上。这意味着所有的function在apply之前都要先对argument求值。这是比较熟悉的经典做法。

这两种规约的效率谁更优是不一定的

Evaluation Strategy

好像搜了很多地方都没有找到类似的定义，可能这是村规

Evaluation和Reduction的区别在于

1. Evaluation只要求最后是一个特殊的形式(canonical form)

2. Evaluation会尽可能避免对function body化简

Canonical Form

意思是形如 $\lambda x. M$ 这样的term

一个Closed Normal Form一定是Canonical Form（所有变量都bounded，且不能再规约，意味着最外面是$\lambda x. M$ 的形式），反之则不然（很显然一个CF仍然可能被规约简化）

Normal Order Evaluation Rules

注意到，如果normal order reduction停止了，那么在规约过程中一定存在一个canonical form。因此提出normal order evaluation的求值策略，规则如下

1. $\lambda x. M\Rightarrow \lambda x.M$，意思是在此处停止

2. 如果$M\Rightarrow\lambda x. M’$，且 $M’[N/x]\Rightarrow P$，那么$M\; N\Rightarrow P$，意思是先把function body规约成canonical form(也就是一个标准的function形式)，再带入parameter，最后整体化简

Eager Evaluation Rules

这个考虑的则是applicative order reduction的evaluation，即先把parameter化成CF，再进行形参代换

1. $\lambda x. M\Rightarrow \lambda x. M$

2. 若$M\Rightarrow \lambda x.M’$，$N\Rightarrow N’$，$M’[N’/x]\Rightarrow P$，那么 $M\; N\Rightarrow P$，注意观察与上面的不同

Fun Func

给几个好玩的例子吧，可以在lambda calculus interpreter里面玩一玩

Bool

$True=\lambda x.\lambda y. x$

$False=\lambda x.\lambda y. y $

编码其实是任意的，类比函数等价定义的外延性（在相同输入下有相同输出），数据等价定义为它们在相同操作下有相同的行为

negate就比较取巧了

$negate = \forall b. b\;False\;True$

然后可以写一个mux，可以方便后面的二元函数

即$if(A)then(B)else(C)=(A\;B)\;C$

于是就可以很容易地写出and和or和xor，实际上只需要写出三个中的一个就完备了

$and=\lambda x.\lambda y. if(x)then(y)else(False)$

$or=\lambda x.\lambda y.if(x)then(True)else(y)$

$xor=\lambda x.\lambda y.if(x)then(negate\; y)else(y)$

Natural

如何判断一个自然数是$0$

$isZero=\lambda n.(n\;(\lambda x.False)\;True)$

注意到当$n=0$时得到的是单位函数，否则得到常函数$False$

其他部分都快写烂了，跳

Recursion

这个比较好玩，之前算是没怎么搞懂

还是那个玩烂了的例子，我们要算阶乘

很容易写出 $fact=\lambda n.if (isZero\;n)then(1)else(mult\;n\;(fact\;(pred\; n)))$

问题在于等式两侧都出现了$fact$，在具体语言中就表现为我们必须给递归函数一个名字才能调用递归

接下来就是很神奇的操作了

考虑这个函数 $Func=\lambda f.\lambda n.if (isZero\;n)then(1)else(mult\;n\;(f\;(pred\; n)))$，它接受一个函数 $f$，返回一个$f$的递归调用。那么上面的定义就可以解释为$fact$是函数$Func$的不动点，即$Func\;fact=fact$

也就是说，虽然我们不能给$fact$命名，但是我们可以通过一个不含$fact$的式子把它算出来

算不动点也是很神奇的操作

回忆之前的神奇表达式 $\Omega=(\lambda x.x\; x)\,(\lambda x.x\; x)$，可以构造（怎么想到的？！）一个新的函数

$Y=\lambda F.(\lambda x.F(x\;x))\,(\lambda x.F(x\;x))$

观察 $YF=(\lambda x.F(x\; x))\,(\lambda x.F(x\;x))=F((\lambda x.F(x\;x))\,(\lambda x. F(x\;x)))=F(YF)$

大概的idea就是我们希望每次apply完之后，前面多出一个$F$而后面保持不变，这样就可以得到不动点

那么阶乘就可以写成

$Y\; Func$