标签：com http c t tar sp width strong get ble tab
λ演算（Lambda-calculus）是一套用于研究函数定义、应用和递归的形式系统。它由阿兰佐·丘奇（Alonzo Church）和史蒂芬·科尔·克林（Stephen Cole Kleene）在20世纪三十年代引入。
丘奇运用λ演算在1936年给出“判定性问题”（Entscheidungs problem）的一个否定的答案。关于两个λ演算表达式是否等价的命题无法通过一个通用的算法来解决，这是不可判定性能够证明的头一个问题，甚至还在停机问题之先。
λ演算对函数式编程有巨大的影响，特别是Lisp 语言。
λ演算被称为最小的通用编程语言。λ演算可以用来清晰地定义什么是一个可计算函数。它包括一条变换规则（变量替换）和一条函数定义方式。λ演算之通用在于，任何一个可计算函数都能用这种形式来表达和求值。
因而，λ演算是等价于图灵机的。尽管如此，λ演算强调的是变换规则的运用，而非实现它们的具体机器，可以认为这是一种更接近于软件而非硬件的方式。
语法规则
任何λ表达式都可以通过下述三条BNF范式描述：
范式1、＜expr＞ ::= ＜identifier＞
范式2、＜expr＞ ::= (λ ＜identifier＞ . ＜expr＞)
范式3、＜expr＞ ::= (＜expr＞ ＜expr＞)
范式1和范式2描述了“函数定义”，而范式3描述了“函数应用”。
上述BNF范式中的圆括号在不会产生歧义的情况下可以省略。如下假定保证了省略圆括号不会产生歧义：
假定1、函数的应用是左结合的（即从左到右进行计算）
假定2、λ操作符要绑定到它后面的整个表达式上
例如， ((λ x. (x x)) (λ y. y)) 可以简写成 (λ x. x x) λ y. y。
在λ演算中，每个表达式都代表一个只有单一参数的函数，这个函数的参数本身也是一个只有单一参数的函数，同时，函数的值是又一个只有单一参数的函数。
函数定义
在λ演算中，函数是通过λ表达式匿名定义的，这个表达式说明了此函数将对其参数进行什么操作。例如：
f (x) = x + 2 在λ演算中表示为λ x. x + 2
因为λ x. x + 2表示了一个函数，所以我们通常称λ x. x + 2是一个函数。
下面的表格是对这个函数的结构的描述：
|
lambda |
parameter |
dot |
operation |
|
λ |
x |
. |
x + 2 |
从表格可以看出，表达式λ x. x + 2 定义了一个函数，这个函数对其参数x进行了加二操作。
值得注意的是，如果一个λ表达式定义了一个函数，尽管这个函数的参数没有被赋值，这个表达式也是有值的，这个值就是这个表达式本身。
也就是说，在λ演算中，值的概念并不仅仅说一个数字是一个值，一个表达式也可以是一个值。这也是为什么说λ演算对函数式编程语言有有巨大的影响的原因。在函数式编程语言里，函数也可以作为参数传递给其他函数的理念就是来自于此。
函数应用
函数定义表达了函数对其参数进行什么操作。而给函数指定一个实际的参数，将会触发函数对这个参数进行实际的操作，这个过程成为函数应用。
以函数 λ x. x + 2 为例，如果给参数 x 指定一个值3，那么将会得到结果5。这个过程称为：“将函数 λ x. x + 2 应用在参数3上”。
而写法上，就如同“范式3”，像下面这样：
l (λ x. x + 2) 3
上面在描述函数应用的时候，仅仅讨论了将函数应用在数字上的情况，例如，“将函数 λ x. x + 2 应用在参数3上”这种情况：(λ x. x + 2) 3。
如果将函数λ x. x + 2 应用在一个函数（比如 λ y. y + 1）上呢？显然，只要把3 替换成 λ y. y + 1 就可以了：
l （λ x. x + 2） （λ y. y + 1）
这得到的仍旧是一个函数，只不过这个函数的参数也是一个函数。下面讨论把这个新得到的函数再应用到数字3上：
l （λ x. x + 2） （λ y. y + 1） 3
根据λ演算的两条假定，整个表达式的演算顺序是下面这样的：
1) （λ y. y + 1）应用到数字3上，得到4
2) （λ x. x + 2）应用到4上，得到6
注意，虽然λ演算的“假定1”规定函数应用是左结合的，但是“假定2”限制了“λ操作符要绑定到它后面的整个表达式上”。
显然“（λ y. y + 1） 3”是一个整体，所以要先计算出“（λ y. y + 1） 3”的值，再把（λ x. x + 2）应用到计算出的值上。
高阶函数定义和应用
上面对函数的讨论中，只涉及了单一参数函数。
那么，怎样定义一个有多个参数的函数呢？前面讲过，在λ演算体系中，任何函数都只允许有一个参数，有多个参数的函数是不合法的。
例如，f(x, y) = x + y是一个有两个参数的函数，你无法写出一个类似下面这样的λ表达式来表示这个函数：λ x, y. x + y
因为根据“范式1、范式2、范式3”，这种写法是错误的。但是范式允许你写出如下的表达式：
l λ x. λ y. x + y
这条表达式的涵义是：参数为x的函数，对参数x进行了“λ y. x + y”操作。
如果将函数λ x. λ y. x + y应用到数字2和3上时，写法如下：
l （λ x. λ y. x + y） 2 3
这个表达式实际是按照如下顺序进行了一系列计算：
1) 将（λ x. λ y. x + y）应用到2上，得到λ y. 2 + y
2) 将得到的λ y. 2 + y应用到3上，得到5
从上面这两条计算过程来看，λ x. λ y. x + y实际应该写为λ x. (λ y. x + y）,也就是说，在这个表达式应用到两个参数上的过程中，实际上是先应用到第一个参数上，得到一个中间结果，这个中间结果也是一个函数，再把这个新的函数应用到第二个参数上。
函数的值又是一个函数，在数学上，前一个函数被称为高阶函数。而上面的论述，阐明了λ演算体系中，对高阶函数的定义。
（λ x. λ y. x + y） 2 3这个表达式的计算顺序似乎有违λ表达式范式和假定。“2 3”在符合“范式3”，它理应是一个整体。那为什么不是把“（λ x. λ y. x + y）”直接应用到“2 3”上，而是要先应用到2上，再应用到3上呢？
在我能查到的λ演算相关的文献中，其观点基本都是把2和3分开不作为一个整体对待的。我是这样认为的，“2 3”虽然在语法上不违背“范式3”，但是它在语义上是不合理的，没有实际意义，所以要分开为两部分。
BNF对语法的表述较为完备，但是对语义的表述则不够好。所以在理解λ演算的过程中，要从表达式的意义上检查其正确性，而不能硬套范式和假定。
标签：com http c t tar sp width strong get ble tab
原文地址：http://www.cnblogs.com/look4liming/p/3702239.html
