记录学习lambda calculus。
lambda(λ) calculus
λ 演算是一套从数学逻辑中发展，来研究函数如何进行抽象化定义、如何被应用以及递归的形式系统。定义比较抽象，简而言之是研究函数形成的一套方法，一种语言（有一套自成体系的简洁语法），并作为一种用途广泛的计算模型。
λ 演算包含如下：
语法： 合法表达式（λ 表达式）的形式系统
语义： 变换规则的形式系统
λ Abstraction
λ 演算的基本形式如下所示：
其中λ为固定标记，标示函数，
variable指代函数参数，expr指代函数体。乍一看确实抽象，举个例子，我们在数学中表示的
，λ 抽象表示为：
我们将形似于
为文字表述就是：定义一个函数，
x + 1即为函数体，传参为x。λ Application
继续将
作为例子，将此函数应用于
2上，则被写作：我们可以理解数学中所表示的
。
但我们需要注意：
λ 演算没有“值”的概念，我们应将其理解为标识符。
Currying
考虑一个这样的函数：它把一个函数作为参数，这个函数被应用于
1上，我们可以表示成：。把这个函数再应用于
上，形成函数
。
可以看到：
(这里将
表示等价）
即当一个单一参数的函数，它的返回值又是一个带单个参数的函数，这样的函数称之为柯里化函数，以逻辑学家Haskell Curry命名。
依旧抽象对吧，再来举个例子：
我们写一个函数实现加法习惯写成形似
lambda x, y: x + y多参数函数。但在 λ 演算中，函数有且仅能拥有一个参数。那么多参数函数如何转换为单参数函数？这就需要依靠 λ 演算的特性：λ 演算中一切都是函数。
我们可以据此将其转换为一个等价的单参数函数：
更通俗的来讲，我们可以用JavaScript来表示：
const add = x => y => x + y;
add(1)(2); // 3
Identifier
在 λ 演算中，有两种标识符：
自由标识符（free identifier）
绑定标识符（binding identifier）
举例说明：
在函数
中
x被称为约束标识符，因为它在函数体中且又是形参。在
中
y被称为自由标识符，因为它没有被预先声明。引入一个我们经常提到的
closure（闭包）正是上下文作用域的存在，上述所举例的单参数函数加法可实现。
Algorithm
λ 演算只有两条的法则：α-conversion（转换）和 β-conversion（归约）。
名称 | 描述 |
α-conversion | 重命名函数中的绑定标识符 |
β-conversion | 将函数体中的绑定标识符替换为参数表达式 |
α-conversion
例如有定义：
将绑定标识符名称更改为
z，则表示为：如同编程语言中将变量重命名一般，这个规则看起来很无趣，但正因为这条规则，我们才可以得以实现递归。
β-conversion
例如有定义：
将1代入得到
1 + 2，则有 Logical
Boolean
λ 演算中，将True、False分别定义为
通过规约理解函数：有两个标识符：x 和 y，无论 x 是什么值，第一个表达式总是输出 x，而第二个表达式总是输出 y。
我们也可据此实现IF/ELSE，例如下列JavaScript实现：
// Boolean
const T = x => y => x; // True
const F = x => y => y; // False
// if-then-else
const ifThenElse = b => x => y => b(x)(y);
/*
* like this:
* if (True) {
* return 1;
* } else {
* return 10;
* }
* */
console.log(ifThenElse(T)(1)(10)); // 1
console.log(ifThenElse(F)(1)(10)); // 10
Logical operation
利用 β 规约，我们也能实现逻辑运算。
其推导方式如下：
Church Numerals
邱奇数（Church Numerals）为使用邱奇编码的自然数表示法，而用以表示自然数 n 的高阶函数是个任意函数 f 映射到它自身的n重函数复合之函数，通俗的讲，数的“值”即参数被函数包裹的次数。
邱奇数定义自然数如下：
可以看到，邱奇数采用递归定义法。邱奇数的 1 表示后继函数对自然数 0 的
1次应用。邱奇数的 2 表示后继函数对自然数 0 的2次应用。以此递归，对于自然数邱奇数 n，即后继函数对自然数 0 的n次调用。JavaScript实现：
// successor number.
const succ = x => x + 1;
// church numeral.
const λ0 = x => x;
const λ1 = y => x => y(x);
const λ2 = y => x => y(y(x));
const λ3 = y => x => y(y(y(x)));
// 0
console.log(λ0(0));
// λ1(succ) -> (x) => succ(x) -> x + 1
console.log(λ1(succ)(0));
// λ2(succ) -> (x) => succ(succ(x)) -> (x + 1) + 1
console.log(λ2(succ)(0));
// λ3(succ) -> (x) => succ(succ(succ(x))) -> ((x + 1) + 1) + 1
console.log(λ3(succ)(0));