$λ 演算$

简介

λ演算（读作lambda演算）由数学家阿隆佐·邱奇在20世纪30年代首次发表，值得一提的是他也是阿兰·图灵的博士生导师，图灵则是被誉为计算机之父。它从数理逻辑（Mathematical logic）中发展而来，使用变量绑定（binding）和代换规则（substitution）来研究函数如何抽象化定义（define）、函数如何被应用（apply）以及递归（recursion）的形式系统。

λ演算和图灵机等价（图灵完备，作为一种研究语言又很方便）

数学函数 VS λ 演算函数

在数学中，可以用 $f (x)$ 表示一个函数， $x$ 定义为自变量。通常在使用中， $x$ 是一个数值，而在 λ 演算中， $x$ 通常是一个函数，研究的领域也更为广泛。在 λ 演算中没有值的概念，对于数学值 (自然数)的表示，λ 演算也有对应的邱奇数表示。邱奇数也是一个函数。在λ 演算中一切皆函数的理念深入任何地方。

λ 演算做的事

λ 演算只做三样事情：

给个输入变量；
用 λ 表达式来构造函数；
把函数应用于变量上。

上面是 λ 演算唯一能做的三件事。

为什么要学习 λ 演算？

λ 演算可以编码任何计算。你在任何编程语言中编写程序，无论这种语言是否存在，λ 演算总能以某种方式来编码。当然这么做可能效率极其低效，但那不重要，这是一种基本计算观念。我们想知道多少及什么样的程序可以用 λ 表达式来写，而事实是都可以；
λ 演算被认为是函数式编程语言的基石，像 Haskell。最近函数式编程也流行起来，而 Haskell 语言更像是 λ 演算语法的升级版；
λ 演算在大多主流的编程语言都可以用，像 C#、Java 等等语言，他们都支持了 λ 演算。而像 λ 演算中高阶函数、柯里化等相关术语也进入了前端领域，逐步成为一种编程风格

TIP

阿兰·图灵说：“你可以在我的图灵机里写下任何东西。”，而邱奇的 λ 演算也是一样的系统，他们是等价的

语法定义

语法	名称	描述
$x$	变量	用字符或字符串来表示参数或数学上的值或逻辑上的值
$(λ x . M)$	抽象化	表示函数定义 ( $M$ 是一个 $λ$ 项) ，在表达式中的 $x$ 都会绑定为变量 $x$ )
$(M$ $N)$	函数应用(Function Applicationaks)	将函数M 作用于参数N , M, N是 $λ$ 项

所以λ演算式就三个要点：

绑定关系变量任意性，x、y和z都行，它仅仅是具体数据的代称。
递归定义 λ项递归定义，M可以是一个λ项。
替换归约 λ项可应用，空格分隔表示对M应用N，N可以是一个λ项。

λ 项

所有 λ 演算都是通过运算λ 项来完成演算的，所以对于λ 项需要有个清晰的归纳定义：

变量 $x$ 本身就是一个有效的 λ 项；
如果 $t$ 是一个 λ 项，而 $x$ 是一个变量，则 $λ x . t$ 是一个 λ 项 (称为 λ 抽象) ；
如果 $t$ 和 $x$ 是 λ 项，那么 $(t$ $x)$ 是一个 λ 项 (称为应用)

其它的都不是 λ 项。只有重复运用运算法则操作λ 项才是有效的 λ 演算。

λ 抽象

λ 演算的基本形式是： $λ$ <变量>.<表达式> 一个数学函数表达式 $f (x) = x + 2$ , 用 λ 演算的语法表示函数则是 $λ x . x + 2$ (x 可以任意命名) 我们以 λ 演算的 (λx.M) 语法为文字表述就是“定义了一个函数 M (指代 x + 2) ，M 里的 x 都会绑定为变量 x”

JavaScript中的λ表达式：箭头函数

ECMAScript 2015规范引入了箭头函数，它没有this，没有arguments。只能作为一个表达式（expression）而不能作为一个声明式（statement），表达式产生一个箭头函数引用，该箭头函数引用仍然有name和length属性，分别表示箭头函数的名字、形参（parameters）长度。一个箭头函数就是一个单纯的运算式，箭头函数我们也可以称为lambda函数，它在书写形式上就像是一个λ演算式。

柯里化

考虑一个这样的函数：它把一个函数作为参数，这个函数将被应用于 3 上，我们可以表示成: $λ y . y$ 3接下来我们把这个函数再应用于 $λ x . x + 2$ 函数上，于是形成的函数由此可以推导出这三个表达式是等价的：( $λ y . y$ 3) $(λ x . x + 2)$ 等价于( $λ x . x + 2$ ) $3$ 等价于 $3 + 2$ ，这里的等价关系由 λ 演算的运算法则来确立的。这里有了一个新的概念：当一个单一参数的函数，它的返回值又是一个带单个参数的函数，这样的函数称之为柯里化函数，以逻辑学家Haskell Curry命名，柯里化的概念以及三个编程语言Haskell、Brook、Curry都是以他的名字来命名的。用编程语言 Javascript 看一个相加的柯里化函数如下：

function add(x) {
  return function (y) {
    return x + y
  }
}

例如：一个多参函数 $f (x, y) = x - y$ 柯里化后可以写作: $λ x . (λ y . x - y)$ ，去除括号即 $λ x . λ y . x - y$

高阶函数

在数学和计算机科学中，高阶函数是满足下列至少其中一个条件的函数：

接受一个或多个函数作为输入；
输出一个函数。无类型 lambda 演算中所有的函数都是高阶的。除了高阶函数所有其它函数都是一阶函数 (first-order function)

λ 演算对自然数的定义

λ 演算如何来定义自然数的呢？阿隆佐·邱奇发明了以他为命名的邱奇数 (Church Numerals)，也是较为常用的表示法。

邱奇数

邱奇数为使用邱奇编码的自然数表示法，而用以表示自然数 $n$ 的高阶函数是个任意函数 $f$ 映射到它自身的n重函数复合之函数，简言之，数的“值”即等价于参数被函数包裹的次数

$f^{◯ n} = f ◯ f ◯ . . . f$

邱奇数定义自然数如下：

$0 = λ y . λ x . x$

$1 = λ y . λ x . y$ $x$

$2 = λ y . λ x . y$ $(y$ $x)$

...

我们通过 Javascript 语法实现以上的表达式，并分别对 x 和 y 进行声明：x = 0 且 y = x => x + 1 。下面是邱奇数对0、1、2的自然数的定义转为 Javascript 语法的书写方式。定义自然数 0：

let λ0 = y => (x => x)

定义自然数 1：

let λ1 = y => (x => y(x))

定义自然数 2：

let λ2 = y => (x => y(y(x)))

参考资料

https://www.lumin.tech/articles/lambda-calculus/#邱奇数 https://tech.meituan.com/2022/10/13/dive-into-functional-programming-01.html

演算λ演算 ​

简介 ​

数学函数 VS λ 演算函数 ​

λ 演算做的事 ​

为什么要学习 λ 演算？ ​

语法定义 ​

λ 项 ​

λ 抽象 ​

JavaScript中的λ表达式：箭头函数 ​

柯里化 ​

高阶函数 ​

λ 演算对自然数的定义 ​

邱奇数 ​

参考资料 ​