Lambda Calculus

记录学习lambda calculus。

lambda(λ) calculus

λ 演算是一套从数学逻辑中发展，来研究函数如何进行抽象化定义、如何被应用以及递归的形式系统。定义比较抽象，简而言之是研究函数形成的一套方法，一种语言（有一套自成体系的简洁语法），并作为一种用途广泛的计算模型。

λ 演算包含如下：

• 语法： 合法表达式（λ 表达式）的形式系统
• 语义： 变换规则的形式系统

λ Abstraction

λ 演算的基本形式如下所示：
$$
\lambda<variable>.<expr>
$$
其中λ为固定标记，标示函数，variable指代函数参数，expr指代函数体。

乍一看确实抽象，举个例子，我们在数学中表示的\(f(x) = x + 1\)，λ 抽象表示为：
$$
\lambda x.x + 1
$$
我们将形似于\(\lambda x.x + 1\)为文字表述就是：定义一个函数，x + 1即为函数体，传参为x。

λ Application

继续将\(\lambda x.x + 1\)作为例子，将此函数应用于2上，则被写作：
$$
(\lambda x.x + 1)\ 2
$$
我们可以理解数学中所表示的f(2) = x + 1。

但我们需要注意：

λ 演算没有“值”的概念，我们应将其理解为标识符。

Currying

考虑一个这样的函数：它把一个函数作为参数，这个函数被应用于1上，我们可以表示成：\(\lambda y.y\ 1\)。把这个函数再应用于\(\lambda x.x + 3\)上，形成函数\((\lambda y.y \ 1)(\lambda x.x+3)\)。

可以看到：

$$
(\lambda y.y \ 1)(\lambda x.x+3) \equiv (\lambda x.x+3)\ 1 \equiv 1 + 3
$$

(这里将\(\equiv\)表示等价）

即当一个单一参数的函数，它的返回值又是一个带单个参数的函数，这样的函数称之为柯里化函数，以逻辑学家Haskell Curry命名。

依旧抽象对吧，再来举个例子：

我们写一个函数实现加法习惯写成形似lambda x, y: x + y多参数函数。但在 λ 演算中，函数有且仅能拥有一个参数。

那么多参数函数如何转换为单参数函数？这就需要依靠 λ 演算的特性：λ 演算中一切都是函数。

我们可以据此将其转换为一个等价的单参数函数：

$$
\lambda x, \lambda y \ x + y
$$

更通俗的来讲，我们可以用JavaScript来表示：

const add = x => y => x + y;
add(1)(2); // 3

Identifier

在 λ 演算中，有两种标识符：

• 自由标识符（free identifier）
• 绑定标识符（binding identifier）

举例说明：

• 在函数\(\lambda x.x\)中x被称为约束标识符，因为它在函数体中且又是形参。
• 在\(\lambda x.y\)中y被称为自由标识符，因为它没有被预先声明。

引入一个我们经常提到的closure（闭包）

正是上下文作用域的存在，上述所举例的单参数函数加法可实现。

Algorithm

λ 演算只有两条的法则：α-conversion（转换）和 β-conversion（归约）。

α-conversion

例如有下列定义：
$$
\lambda x.xy
$$
将绑定标识符名称更改为z，表示如下：
$$
\lambda z.zy
$$
如同编程语言中将变量重命名一般，这个规则看起来很无趣，但正因为这条规则，我们才可以得以实现递归。

β-conversion

例如有以下定义：
$$
(\lambda x . x + 2)\ 1
$$
将1代入得到1 + 2，则有

$$
(\lambda x.x+2)\ 1 \equiv 1 + 2
$$

Logical

Boolean

λ 演算中，将True、False分别定义为以下：
$$
\lambda x. \lambda y.x
\\
\lambda x. \lambda y.y
$$
通过规约理解函数：有两个标识符：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

利用 β 规约，我们也能实现逻辑运算。

$$
AND := \lambda p. \lambda q.(p \ q \ p)
\\
OR := \lambda p. \lambda q.(p \ p \ q)
\\
NOT := \lambda p.(p \ FALSE \ FALSE)
\\
IFTHENELSE := \lambda p.\lambda a.\lambda b(p \ a \ b)
$$
其推导方式可参考下图：

Church Numerals

邱奇数（Church Numerals）为使用邱奇编码的自然数表示法，而用以表示自然数 n 的高阶函数是个任意函数 f 映射到它自身的n重函数复合之函数，通俗的讲，数的“值”即参数被函数包裹的次数。

$$
f^{o\ n} = f \circ f \circ f \cdots f
$$

邱奇数定义自然数如下：

$$
0 = \lambda y. \lambda x.x
\\
1 = \lambda y. \lambda x. y\ x
\\
2 = \lambda y. \lambda x. y(y\ x)
\\
3 = \lambda y. \lambda x. y(y(y\ x))
\\
\cdots
\\
n = \lambda y. \lambda x. \cdots y^{n} \ x
$$

可以看到，邱奇数采用递归定义法。邱奇数的 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));

References

• Lambda Calculus – Pandaos’s blog
• 何为 λ 演算（Lambda Calculus）
• 我的最爱Lambda演算
• Lambda calculus – Wikipedia
• Y分钟入门lambda演算