关于 lambda 演算

这书最终还是没看下去 w，太啰嗦了实在是。而且感觉关注的重点有些偏离实践。

试图看《Haskell Programming From First Principles》，它居然从 lambda 演算作为起始点，令人感叹。因此进行一些学习。

什么是函数？函数是输入的集合到输出的集合的映射。”Understanding functions in this way——as a mapping of a set of inputs to a set of outputs——is crucial to understanding functional programming.“

演算（calculus）指某种计算或推理的方法。lambda 演算是一种（对特定事物进行）形式化（描述）的方法。比如，它可以对图灵机进行描述，从而能够做到同冯诺依曼姬一样图灵完备。命令式编程语言从冯诺依曼体系出发，函数式编程语言从 lambda 演算出发（当然，底层仍旧是冯诺依曼体系的，硬件基础决定必须如此）。

就如四则运算有数字和运算符两种元素，lambda 演算有三个基本元素——expression，variable，abstraction。

expression 是所有东西的父集。它可以是 variable 的名字，abstraction，或是它们的组合。最简单的 expression 是单个变量，比如x。

variable 没有特定的意义或值 （真正的值，即特定的 lambda 表达式的语义不能从 lambda 演算本身中找到，而要从外界找到），它只是一个名字——对函数的可能输入赋予的名字。

abstraction 是函数。它包括函数头，函数体。它可以应用单个 argument——单个输入。在当前的语境下，大可把 abstraction 当作函数的同义词。

abstraction 的一个实例如下——

𝜆x.x

其中𝜆后的 x 表示 variable（parameter）的名称，.后的东西为函数体。这个 abstraction 用数学语言大可以表述为f(x) = x，或者通过 haskell 表述——(\x -> x)。

显然，lambda 演算中的 abstraction 是比数学中的函数更加抽象，一般化的——它的输入值是没有任何限定的，无论输入值是一个数字，字符串，或是另一个函数，它都能作为入参并进行替换。

绑定（bind），当我们对函数应用一个参数的时候，函数体中的每一个 x 都会被替换成该参数。也可以说，x 绑定在该参数上了。参数的值为何，x 就会被替换为何值。被绑定的 x 变量称为约束变量。

约束变量的名字是可以随意替换的，比如𝜆x.x，可以替换成𝜆y.y，𝜆z.z。这是显然的——x，y，z 只是名字，代号而已，它们会被具体的值替换，因此命名如何无关紧要。这种性质称为** alpha 等价**。

这里的 abstraction 𝜆x.x没有名字 ，因此它是一个匿名函数（anonymous function）。

abstraction 之所以叫 abstraction，是因为它进行了一定的抽象——通过让名字代表具体的值来抽象出特定形式；在应用中以具体的值替换名字——从而让一定的形式能具有更加广泛的意义。如果离开了这种替换，形如x + 1这种形式的表达式是没有任何意义的，因为 x 只是一个奇怪的符号而已。

这里的“应用”也有自己的语法——(M N)，其中 M 为应当为 abstraction，而 N 为一个任意 lambda 元素（项）。比如(𝜆x.(x + 1) 2)就是一个应用，2 将作为参数应用到该 abstraction，将 x 替换为 2，最终得到 (2 + 1) 这个表达式。这称为** Beta 化简**。显然这是将 abstraction 转换成表达式的基础。

parameter 和 argument——定义的语境称作 parameter，应用的语境称为 argument。绑定的是 parameter，接受的是 argument。实践中这两个词通常可以混用，都冠以“参数”为名。但 argument 更倾向于表示传递给函数的值。

这里的 1，2，+应该考虑为某种标识符，或某种变量名，不考虑它的具体语义。

对𝜆x.x，将其应用到入参1和𝜆y.y，能够得到1和𝜆y.y。下面列出了(𝜆𝑦.𝑦)求解过程，其中[𝑥 ∶= (𝜆𝑦.𝑦)]表示 x 将替换为(𝜆𝑦.𝑦)，或者说 x 和这个值绑定了。

(𝜆𝑥.𝑥)(𝜆𝑦.𝑦)
[𝑥 ∶= (𝜆𝑦.𝑦)]
𝜆𝑦.𝑦

又比如对(𝜆𝑥.𝑥)(𝜆𝑦.𝑦)𝑧，能容易看出来其结果为 z。(𝜆𝑥.𝑥)显然为 identity 函数。容易得到 const 函数——(𝜆x.𝜆y.x)。

变量绑定和替换就是 lambda 演算的核心规则。在 lambda 演算里，变量只是名字，函数只是一个等待替换输入参数并返回一个表达式的“模版”。对 lambda 表达式进行化简的过程称为解析（resolve）。解析将在无法再次进行 Beta 化简时停止，即找不到 abstraction，或者找不到参数。无法进行 Beta 化简的表达式称为beta normal form。这种形式是计算完全的表达式。

但是并非所有表达式都能转化为 beta normal form，比如这个——(𝜆x.xx)(𝜆x.xx)，对其进行 Beta 化简会得到它本身，因而能够无限地化简下去。这种表达式是diverge发散的。很好奇这是否涉及到停机问题。

同时出现在函数头和函数体的名字称为约束变量，而未出现在函数头却出现在函数体中的名字称为自由变量。编程中自由变量是常见的——引用的上层作用域或全局作用域的变量。

函数是单参数的，就如 Haskell 的函数定义一样，但也同 haskell 一样允许使用“语法糖”——形如𝜆xy.xy的函数实质上是𝜆x.(𝜆y.xy)。顺便，这里的xy没有任何意义，只是两个名字放在一起罢了，具体语义没有被定义。可以认为类似数学上那种乘法表述，f(x)=2x。但若是 x 被应用到了另一个函数，这将成为一次函数的应用。

𝜆xy.xy (𝜆z.a) 1
(𝜆x(𝜆y.xy)) (𝜆z.a) 1
[x := (𝜆z.a)]
(𝜆y.(𝜆z.a)y) 1
[z := y]
(𝜆y.a) 1
[y := 1]
a 

当然，对于多参数的应用，大可以直接一次性全部替换。只是这种替换对人脑友好，对计算机不友好罢了。

lambda 演算中的计算（evaluation）就是化简。这对一个只有纯函数形式的“语言”来说是显然的。

组合子（Combinator）是没有自由变量的 lambda 项。它代表一类这样的 lambda——它只能对它的 argument 进行组合。

lambda 表达式的计算顺序遵循normal order。”Normal order is a common evaluation strategy in lambda calculi. Normal order means evaluating (ie, applying or beta reducing) the leftmost outermost lambdas first, evaluating terms nested within after you’ve run out of arguments to apply.”

就这样了。将来如果有必要再深化。lambda 演算比我想象的还要简单，看来是之前看的书，文章太过堆砌概念了。