函数式编程----lambda演算

怼烎@ 2022-06-16 06:50 318阅读 0赞

转载自：

http://blog.csdn.net/crazyhacking/article/details/8183088

#    一 概念 #

函数式编程（[英语][Link 1]：Functional programming），又称泛函编程，是一种[编程范型][Link 2]，它将电脑运算视为[数学][Link 3]上的[函数][Link 4]计算，并且避免[状态][Link 5]以及[可变][Link 6]数据。函数编程语言最重要的基础是 [λ 演算][Link 7]（lambda calculus）。而且λ演算的函数可以接受函数当作输入（引数）和输出（传出值）。代表语言haskell,erlang，lisp等

特点：

（1）函数式编程经常使用[递归][Link 8]。

（2）纯函数式的程序不可[变量][Link 9]和无[副作用][Link 10]([Side effect][])。因为**纯**函数式程序设计语言没有[变量][Link 9]，函数没有[副作用][Link 10]，编写出的程序可以利用[记忆化][Link 11]、[公共子表达式消除][Link 12]和[并发计算][Link 13]在运行时和编译时得到大量[优化][Link 14]。

（3）惰性求值

(4) 高阶函数

（5）一切皆函数

缺点：速度和空间上的顾虑

函数式编程常被认为严重耗费在CPU和存储器资源。主因有二：

*  早期的函数式编程语言实现时并无考虑过效率问题。
 *  非函数式编程语言为求提升速度，会在某些部分放弃边界检查或垃圾回收等功能。

[惰性求值][Link 15]亦为语言如[Haskell][]增加了额外的管理工作。

# 二  λ演算  #

λ演算（lambda calculus）是一套用于研究[函数][Link 16]定义、函数应用和[递归][Link 8]的[形式系统][Link 17]。  
Lambda演算被称为最小的通用程序设计语言。它包括一条变换规则（变量替换）和一条函数定义方式，Lambda演算之通用在于，任何一个可计算函数都能用这种形式来表达和求值。因而，它是等价于[图灵机][Link 18]的。尽管如此，Lambda演算强调的是变换规则的运用，而非实现它们的具体机器。可以认为这是一种更接近软件而非硬件的方式。

形式化定义

所有的lambda表达式可以通过下述以[BNF][]范式表达的[上下文无关文法][Link 19]描述：

1.  <expr> ::= <identifier>
2.  <expr> ::=(λ<identifier> .<expr>)
3.  <expr> ::=(<expr> <expr>)

例如：λx y.x+y

头两条规则用来生成函数，而第三条描述了函数是如何作用在参数上的。

如下假定保证了不会产生歧义：（1）函数的作用是左结合的，和（2）lambda操作符被绑定到它后面的整个表达式。例如，表达式 (λx.x x)(λy.y) 可以简写成λ(x.x x) λy.y 。

# 三 lambda演算中的算术 #

1   邱奇数

**Church 编码**是把数据和运算符嵌入到 [lambda 演算][lambda]内的一种方式，最常见的形式是 Church 数，它是使用 lambda 符号的自然数的表示法。这种方法得名于 [Alonzo Church][]，他首先以这种方法把数据编码到 lambda 演算中。

在其他符号系统中通常被认定为基本的项(比如整数、布尔值、有序对、列表和 tagged unions)都被映射到使用 Church 编码的[高阶函数][Link 20]；根据[邱奇-图灵论题][-]我们知道任何可计算的运算符(和它的运算数)都可以用 Church 编码表示。

很多学数学的学生熟悉[可计算函数][Link 21]集合的[哥德尔编号][Link 22]；Church 编码是定义在 [lambda 抽象][lambda 1]而不是自然数上的等价运算。

## Church 数 ##

**Church 数**是在 Church 编码下的[自然数][Link 23]的表示法。表示自然数 ![n][] 的[高阶函数][Link 20]是把任何其他函数 ![f][] 映射到它的 *n* 重[函数复合][Link 24] ![f^n = f \\circ f \\circ \\ldots \\circ f][f_n _ f _circ f _circ _ldots _circ f] 的函数。

### 定义 ###

Church 数 **0**, **1**, **2**, ... 在 [lambda 演算][lambda]中被定义如下:

**0** ≡  `λf.λx. x`

**1** ≡  `λf.λx. f x`

**2** ≡  `λf.λx. f (f x)`

**3** ≡  `λf.λx. f (f (f x))`

...

**n** ≡  `λf.λx. fn x`

...

就是说，自然数 ![n][] 被表示为 Church 数 **n**，它对于任何 lambda-项 `F`和 `X` 有着性质：

**n**  `F X`  [=β][Link 25]  `Fn X`。

### 使用 Church 数的计算 ###

在 lambda 演算中，数值函数被表示为在 Church 数上的相应函数。这些函数在大多数函数式语言中可以通过 lambda 项的直接变换来实现(服从于类型约束)。

加法函数 ![plus(m,n)=m+n][plus_m_n_m_n] 利用了恒等式 ![f^\{(m+n)\}(x)=f^m(f^n(x))][f_m_n_x_f_m_f_n_x]。

**plus** ≡  `λm.λn.λf.λx. m f (n f x)`

后继函数 ![succ(n)=n+1][succ_n_n_1] [β-等价][- 1]于 (**plus 1**)。

**succ** ≡  `λn.λf.λx. f (n f x)`

乘法函数 ![times(m,n)=m\*n][times_m_n_m_n] 利用了恒等式 ![f^\{(m\*n)\} = (f^m)^n][f_m_n_ _ _f_m_n]。

**mult** ≡  `λm.λn.λf. n (m f)`

指数函数 ![exp(m,n)=m^n][exp_m_n_m_n] 由 Church 数定义直接给出。

**exp** ≡  `λm.λn. n m`

前驱函数 ![pred(n) = \\begin\{cases\} 0 & \\mbox\{if \}n=0, \\\\ n-1 & \\mbox\{otherwise\}\\end\{cases\}][pred_n_ _ _begin_cases_ 0 _ _mbox_if _n_0_ _ n-1 _ _mbox_otherwise_end_cases] 通过生成每次都应用它们的参数 `g` 于 `f` 的 ![n][] 重函数复合来工作；基础情况丢弃它的 `f` 复本并返回 `x`。

**pred** ≡  `λn.λf.λx. n (λg.λh. h (g f)) (λu. x) (λu. u)`

## Church 布尔值 ##

**Church 布尔值**是布尔值**真**和**假**的 Church 编码。布尔值被表示为两个参数的函数，它得到这两个参数中的一个。

[lambda 演算][lambda]中的形式定义:

**true** ≡  `λa.λb. a`

**false** ≡  `λa.λb. b`

从Church 布尔值推导来的布尔算术的函数:

**and** ≡  `λm.λn.λa.λb. m (n a b) b`

**or** ≡  `λm.λn.λa.λb. m a (n a b)`

**not** ≡  `λm.λa.λb. m b a`

## 有序对 ##

有序对（2-元组）数据类型可以用TRUE、FALSE和IF来定义。

CONS := λx y.λp.IF p x y

CAR := λx.x TRUE

CDR := λx.x FALSE

链表数据类型可以定义为，要么是为空列表保留的值（e.g.FALSE），要么是CONS一个元素和一个更小的列表。

## 递归 ##

[递归][Link 8]是使用函数自身的函数定义；在表面上，lambda演算不允许这样。但是这种印象是误解。考虑个例子，[阶乘][Link 26]函数f(n)递归的定义为

f(n):= if n = 0 then 1 else n·f(n-1)。

在lambda演算中，你不能定义包含自身的函数。要避免这样，你可以开始于定义一个函数，这里叫g，它接受一个函数f作为参数并返回接受n作为参数的另一个函数：

g := λf n.(if n = 0 then 1 else n·f(n-1))。

函数g返回要么常量1，要么函数f对n-1的n次应用。使用ISZERO谓词，和上面描述的布尔和代数定义，函数g可以用lambda演算来定义。

但是，g自身仍然不是递归的；为了使用g来建立递归函数，作为参数传递给g的f函数必须有特殊的性质。也就是说，作为参数传递的f函数必须展开为调用带有一个参数的函数g -- 并且这个参数必须再次f函数!

换句话说，f必须展开为g(f)。这个到g的调用将接着展开为上面的阶乘函数并计算下至另一层递归。在这个展开中函数f将再次出现，并将被再次展开为g(f)并继续递归。这种函数，这里的f = g(f)，叫做g的不动点，并且它可以在lambda演算中使用叫做**悖论算子**或**不动点算子**来实现，它被表示为Y -- [Y组合子][Y]：

Y = λg.(λx.g(x x))(λx.g(x x))

在lambda演算中，Y g是g的不动点，因为它展开为g(Y g)。现在，要完成我们对阶乘函数的递归调用，我们可以简单的调用 g(Y g)n，这里的n是我们要计算它的阶乘的数。

比如假定n = 5，它展开为：

(λn.(if n = 0 then 1 else n·((Y g)(n-1)))) 5

if 5 = 0 then 1 else 5·(g(Y g，5-1))

5·(g(Y g)4)

5·(λn.(if n = 0 then 1 else n·((Y g)(n-1))) 4)

5·(if 4 = 0 then 1 else 4·(g(Y g，4-1)))

5·(4·(g(Y g)3))

5·(4·(λn.(if n = 0 then 1 else n·((Y g)(n-1))) 3))

5·(4·(if 3 = 0 then 1 else 3·(g(Y g，3-1))))

5·(4·(3·(g(Y g)2)))

...

等等，递归的求值算法的结构。所有递归定义的函数都可以看作某个其他适当的函数的不动点，因此，使用Y所有递归定义的函数都可以表达为lambda表达式。特别是，我们现在可以明晰的递归定义自然数的减法、乘法和比较谓词。

# 四 各种数据结构 #

各种数据结构的表示，例如，线性表，树，快排等的实现。请参考byvoid同学的讲稿：[http://www.byvoid.com/blog/apio-fp/\#more-3200][http_www.byvoid.com_blog_apio-fp_more-3200]

本文总结摘抄自：1 函数式编程

[http://zh.wikipedia.org/wiki/%E5%87%BD%E6%95%B8%E7%A8%8B%E5%BC%8F%E8%AA%9E%E8%A8%80][http_zh.wikipedia.org_wiki_E5_87_BD_E6_95_B8_E7_A8_8B_E5_BC_8F_E8_AA_9E_E8_A8_80]

2 lambda演算 [http://zh.wikipedia.org/wiki/%CE%9B%E6%BC%94%E7%AE%97][Link 7]

3邱奇数 [http://zh.wikipedia.org/wiki/%E9%82%B1%E5%A5%87%E6%95%B0][http_zh.wikipedia.org_wiki_E9_82_B1_E5_A5_87_E6_95_B0]

4  byvoid同学的讲稿：[http://www.byvoid.com/blog/apio-fp/\#more-3200][http_www.byvoid.com_blog_apio-fp_more-3200]

5  函数式编程初探 -阮一峰: [http://www.ruanyifeng.com/blog/2012/04/functional\_programming.html][http_www.ruanyifeng.com_blog_2012_04_functional_programming.html]

[Link 1]: http://zh.wikipedia.org/wiki/%E8%8B%B1%E8%AF%AD
[Link 2]: http://zh.wikipedia.org/wiki/%E7%B7%A8%E7%A8%8B%E5%85%B8%E7%AF%84
[Link 3]: http://zh.wikipedia.org/wiki/%E6%95%B8%E5%AD%B8
[Link 4]: http://zh.wikipedia.org/wiki/%E5%87%BD%E6%95%B0_%28%E6%95%B0%E5%AD%A6%29
[Link 5]: http://zh.wikipedia.org/wiki/%E7%8A%B6%E6%80%81
[Link 6]: http://zh.wikipedia.org/wiki/%E4%B8%8D%E5%8F%AF%E8%AE%8A%E7%89%A9%E4%BB%B6
[Link 7]: http://zh.wikipedia.org/wiki/%CE%9B%E6%BC%94%E7%AE%97
[Link 8]: http://zh.wikipedia.org/wiki/%E9%80%92%E5%BD%92
[Link 9]: http://zh.wikipedia.org/wiki/%E8%AE%8A%E6%95%B8
[Link 10]: http://zh.wikipedia.org/wiki/%E5%89%AF%E4%BD%9C%E7%94%A8_%28%E8%A8%88%E7%AE%97%E6%A9%9F%29
[Side effect]: http://en.wikipedia.org/wiki/Side_effect_%28computer_science%29
[Link 11]: http://zh.wikipedia.org/w/index.php?title=%E8%A8%98%E6%86%B6%E5%8C%96&action=edit&redlink=1
[Link 12]: http://zh.wikipedia.org/w/index.php?title=%E5%85%AC%E5%85%B1%E5%AD%90%E8%A1%A8%E9%81%94%E5%BC%8F%E6%B6%88%E9%99%A4&action=edit&redlink=1
[Link 13]: http://zh.wikipedia.org/wiki/%E5%B9%B6%E8%A1%8C%E8%AE%A1%E7%AE%97
[Link 14]: http://zh.wikipedia.org/wiki/%E4%BC%98%E5%8C%96
[Link 15]: http://zh.wikipedia.org/wiki/%E6%83%B0%E6%80%A7%E6%B1%82%E5%80%BC
[Haskell]: http://zh.wikipedia.org/wiki/Haskell
[Link 16]: http://zh.wikipedia.org/wiki/%E5%87%BD%E6%95%B0
[Link 17]: http://zh.wikipedia.org/wiki/%E5%BD%A2%E5%BC%8F%E7%B3%BB%E7%BB%9F
[Link 18]: http://zh.wikipedia.org/wiki/%E5%9B%BE%E7%81%B5%E6%9C%BA
[BNF]: http://zh.wikipedia.org/wiki/%E5%B7%B4%E7%A7%91%E6%96%AF%E8%8C%83%E5%BC%8F
[Link 19]: http://zh.wikipedia.org/wiki/%E4%B8%8A%E4%B8%8B%E6%96%87%E6%97%A0%E5%85%B3%E6%96%87%E6%B3%95
[lambda]: http://zh.wikipedia.org/wiki/Lambda_%E6%BC%94%E7%AE%97
[Alonzo Church]: http://zh.wikipedia.org/wiki/Alonzo_Church
[Link 20]: http://zh.wikipedia.org/wiki/%E9%AB%98%E9%98%B6%E5%87%BD%E6%95%B0
[-]: http://zh.wikipedia.org/wiki/%E9%82%B1%E5%A5%87-%E5%9B%BE%E7%81%B5%E8%AE%BA%E9%A2%98
[Link 21]: http://zh.wikipedia.org/wiki/%E5%8F%AF%E8%AE%A1%E7%AE%97%E5%87%BD%E6%95%B0
[Link 22]: http://zh.wikipedia.org/wiki/%E5%93%A5%E5%BE%B7%E5%B0%94%E7%BC%96%E5%8F%B7
[lambda 1]: http://zh.wikipedia.org/w/index.php?title=Lambda_%E6%8A%BD%E8%B1%A1&action=edit&redlink=1
[Link 23]: http://zh.wikipedia.org/wiki/%E8%87%AA%E7%84%B6%E6%95%B0
[n]: /images/20220616/41dec5663de64dae91f2fa383010dc11.png
[f]: http://upload.wikimedia.org/math/8/f/a/8fa14cdd754f91cc6554c9e71929cce7.png
[Link 24]: http://zh.wikipedia.org/wiki/%E5%87%BD%E6%95%B0%E5%A4%8D%E5%90%88
[f_n _ f _circ f _circ _ldots _circ f]: http://upload.wikimedia.org/math/5/f/b/5fb363e461e5a62de936ee294197fdac.png
[Link 25]: http://zh.wikipedia.org/wiki/Lambda_%E6%BC%94%E7%AE%97#.CE.B2-.E5.BD.92.E7.BA.A6
[plus_m_n_m_n]: http://upload.wikimedia.org/math/5/5/f/55f0315e517bfb43d61bf4e3367079fe.png
[f_m_n_x_f_m_f_n_x]: /images/20220616/b1857e3ac6964fa3adc16ef5c24b93b8.png
[succ_n_n_1]: http://upload.wikimedia.org/math/2/b/8/2b87835a2c2ba7cf86ea0ad9a41064f6.png
[- 1]: http://zh.wikipedia.org/w/index.php?title=Beta_%E5%BD%92%E7%BA%A6&action=edit&redlink=1
[times_m_n_m_n]: http://upload.wikimedia.org/math/3/7/2/372532b5631de718332af96ff5394bf2.png
[f_m_n_ _ _f_m_n]: /images/20220616/992a99b90dda4fac817e79b52390a19b.png
[exp_m_n_m_n]: /images/20220616/6ffb0a070b1e4bc4965b9eb5e588154a.png
[pred_n_ _ _begin_cases_ 0 _ _mbox_if _n_0_ _ n-1 _ _mbox_otherwise_end_cases]: http://upload.wikimedia.org/math/8/5/0/8508747362f9fb9c98ebd6fd564860eb.png
[Link 26]: http://zh.wikipedia.org/wiki/%E9%98%B6%E4%B9%98
[Y]: http://zh.wikipedia.org/wiki/%E4%B8%8D%E5%8A%A8%E7%82%B9%E7%BB%84%E5%90%88%E5%AD%90
[http_www.byvoid.com_blog_apio-fp_more-3200]: http://www.byvoid.com/blog/apio-fp/#more-3200
[http_zh.wikipedia.org_wiki_E5_87_BD_E6_95_B8_E7_A8_8B_E5_BC_8F_E8_AA_9E_E8_A8_80]: http://zh.wikipedia.org/wiki/%E5%87%BD%E6%95%B8%E7%A8%8B%E5%BC%8F%E8%AA%9E%E8%A8%80
[http_zh.wikipedia.org_wiki_E9_82_B1_E5_A5_87_E6_95_B0]: http://zh.wikipedia.org/wiki/%E9%82%B1%E5%A5%87%E6%95%B0
[http_www.ruanyifeng.com_blog_2012_04_functional_programming.html]: http://www.ruanyifeng.com/blog/2012/04/functional_programming.html