函数式编程从入门到入门 —— 回溯到λ演算

Posted 2021-04-09 多牧FE

函数式编程（又称 函数程序设计 ），它区别于我们通常接触的通过指令编写的 命令式编程 ，是另一种思想的 编程范式 ，它将所有的计算机运算都视为数学上的函数运算，并且避免了程序中状态和可变对象的使用。函数式编程更加重视输出的结果而不是在过程中产生变化，比起在一系列的指令中产生改变，它更倾向于每一步函数变化得出的新结果。总而言之，函数式编程是将巨大复杂的变化，分解成一步一步精巧而可控的函数。

函数式编程从入门到入门是系列文章，这是第一篇。

回溯到λ演算

历史

时间回到十九世纪三十年代，计算机之父 艾伦·图灵 提出了著名的抽象计算模型 —— 图灵模型 ，而在同一时期，美国数学家 阿隆佐·邱奇 也提出了一套计算模型—— λ演算 模型。最开始，邱奇试图创制一套完整的形式系统作为数学的基础，当他发现这个系统易受 罗素悖论 的影响时，就把 λ演算 演算单独分离出来，用于研究可计算性，最终导致了他对 判定性问题 的否定回答。根据 邱奇-图灵论题 ，这两种计算模型是等效的， λ演算 也同样可以被 图灵机 演算。

λ演算 是一套从数学逻辑中发展，以变量绑定和替换的规则，来研究函数如何抽象化定义、函数如何被应用以及递归的形式系统。 λ演算 演算作为一种广泛用途的计算模型，可以清晰地定义什么是一个可计算函数，而任何可计算函数都能以这种形式表达和求值，它能模拟单一磁带 图灵机 的计算过程；尽管如此， λ演算 强调的是变换规则的运用，而非实现它们的具体机器。

Λ 项

λ演算 的语法将一些表达式定义为有效的λ演算式，而某一些表达式无效，就像C语言中有些字符串有效，有些则不是。有效的 λ演算 式称为 λ项 。

以下三个规则给出了语法上有效的 λ项 ，如何建构的归纳定义：

• 变量 x 本身就是一个有效的 λ项 ;

• 如果 x 是一个 λ项 ，而 x 是一个变量，则 λ x.t 是一个 λ项 ；

• 如果 x 和 s 是 λ项 ，那么 (ts) 是一个 λ项 。

其它的都不是 λ项 。因此， λ项 当且仅当可重复应用这三个规则获取时，才是有效的。一些括号根据某些规则可以省略。例如，最外面的括号通常不会写入。

概念

形式	名称	描述
x	变量	一个代表参数、数学值或逻辑值的字符或字符串。
(λx.M)	抽象	定义了函数，x变量被绑定在 λ项上。
(M N)	应用	将参数N传入函数M，M和N都为 λ项 。
(λx.M[x]) → (λy.M[y])	α-等价	在表达式中将参数x用y替换，用来解决重名问题。
((λx.M) E) → (M[x:=E])	β-规约	将参数E绑定到变量x上。

函数是唯一的 “类型”

在 λ演算 中，每一个表达式都被视为一个单参数函数，并且这些函数只会返回一个值。而且对于这些函数，他们的参数和返回值都是一个单参数函数。总而言之， λ演算 中可以认为只有一种类型，单参数函数，这些函数通过 λ表达式 定义，表达式代表了函数将对参数做怎样的操作。

举个例子来说：我们有一个 “喜加一” 函数

f(x) = x + 1
# 我们可以这样来表达
λx.x + 1

Λ演算 中的数据和演算

基本算数

在lambda演算中有许多方式都可以定义自然数，但最常见的还是邱奇数，下面是它们的定义：

0 = λf.λx.x
1 = λf.λx.f x
2 = λf.λx.f (f x)
3 = λf.λx.f (f (f x))

由此类推，我们得到了以下函数：

# 喜加一
PLUS_ONE = λn.λf.λx.f(n f x)
# 加法就是在加一的基础上，重复n次加一
PLUS = λm.λn.λf.λx.m f (n f x)
# 乘法就是在0的基础上重复PLUS n次
MULT = λm.λn.m (PLUS n) 0
# -1s 有些复杂，通过跳过一层参数，达到减一的效果
PRED = λn.λf.λx.n(λg.λh.h(g f))(λu.x)(λu.u)

逻辑与谓词

邱奇布尔值：

TRUE := λx.λy.xFALSE := λx.λy.y

定义逻辑运算为：

AND := λp q.p q FALSEOR := λp q.p TRUE q
NOT := λp.p FALSE TRUEIFTHENELSE := λp x y.p x y