形式语义03 Lambda

\(\lambda\)-calculus讲了一点点，后面的下次再补...

Background

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

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

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

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\)
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. (\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\}\)
2. \(FV(\lambda x.M)=FV(M)-\left\{\;x\;\right\}\)
3. \(FV(M N)=FV(M)\cup FV(N)\)

也就是通过表达式的结构来递归求值

Substitution

这里的substitution和直接替换是有区别的

我们用 \(M[x/y]\) 或者 \(M\left\{x/y\right\}\) 来表示用 \(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}}=x\)
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的情况了

\(\beta\)-reduction

这个主要用于application求值的时候，递归定义如下：

1. \((\lambda x. M)N\rightarrow M[N/x]\)，意思是一个application就是一个substitution
2. 如果 \(M\rightarrow M'\)，那么 \(\lambda x.M\rightarrow\lambda x.M'\)
3. 如果 \(M\rightarrow M'\)，那么 \(M N\rightarrow M' N\)
4. 同理若 \(N\rightarrow N'\)，那么 \(MN\rightarrow MN'\)