目录
新浪博客：Lambda Calculus —— 叙述通俗朴素
你好，类型（十）：Parametric polymorphism
你好，类型（六）：Simply typed lambda calculus
Hilbert-style和Gentzen-style演绎系统
《类型和程序设计语言》
百科
λ演算
λ演算，λ(Lambda（大写Λ，小写λ）读音：lan b（m） da（兰亩达）['læ;mdə])演算是一套用于研究函数定义、函数应用和递归的形式系统。它由 Alonzo Church 和 Stephen Cole Kleene 在 20 世纪三十年代引入，Church 运用 lambda 演算在 1936 年给出 判定性问题 (Entscheidungsproblem) 的一个否定的答案。这种演算可以用来清晰地定义什么是一个可计算函数。关于两个 lambda 演算表达式是否等价的命题无法通过一个通用的算法来解决，这是不可判定性能够证明的头一个问题，甚至还在停机问题之先。
λ 演算可以被称为最小的通用程序设计语言。它包括一条变换规则 (变量替换) 和一条函数定义方式，λ演算之通用在于，任何一个可计算函数都能用这种形式来表达和求值。因而，它是等价于图灵机的。尽管如此，λ演算强调的是变换规则的运用，而非实现它们的具体机器。可以认为这是一种更接近软件而非硬件的方式。它一个数理逻辑形式系统，使用变量代入和置换来研究基于函数定义和应用的计算。希腊字母λ被用来在λ演算模型中表示将一个变量绑定在一个函数中。
λ演算可以是有类型的也可以是无类型的，仅仅当输入的的数据类型对于有类型的λ演算函数来说是可以接受的时，有类型的λ演算函数才能被使用。λ演算模型在数学，物理学，语言学和计算机科学等不同领域有着广泛的应用。它在编程语言的理论发展上起到了很重要的作用，并对函数式编程起到了很大的影响，甚至可以说函数式编程就是对λ演算模型的一种实现。同时，它也是范畴论的当前研究对象之一。
λ演算模型最初的形式系统在1935年被 Stephen Kleene 和 J. B. Rosser提出的Kleene–Rosser悖论证明为是前后矛盾的，接着，在1936年，Church单独出版了λ演算模型中的和纯计算有关的部分，也就是如今被称为的无类型λ演算。在1940年，他提出了一个弱化计算，但是逻辑自洽的形式系统，如今被称之为简单类型λ演算。
在20世纪60年代之前，λ演算和编程语言之间的关系被厘清之前，λ演算模型一直都仅仅是一个理论上的形式系统，多亏了Montague和其他的几位语言学家在自然语言的语义方面的研究，λ演算开始在语言学和计算机科学的研究中占有一席之地。
归约策略
在编程语言的理论研究中，求值策略(Evaluation strategy)是一组用来确定程序设计语言中的表达式求值的规则。求值策略主要规定了在什么时候和用什么样的顺序给函数的实际参数求值，何时把参数代换入函数内，和用怎样的形式来进行代换。通常，人们使用λ演算模型中的归约策略来建模求值策略。
无论一个表达式是否为标准状态，将这个这个表达式化为标准型所需要的工作量很大程度上依赖于归约策略的使用。而归约策略的不同又和函数式编程中的及早求值还有惰性求值之间的不同有关。
1.完全β-归约 (Full β-reduction)
任何参数在任何时候都可以被归约，其实就是没有任何的归约策略，天知道会发生什么。
2.应用次序 (Applicative order)
最右边，最内部的表达式总是首先被归约，直观上可以知道，这意味着函数的参数总是在函数调用之前就被归约了。应用次序总是企图用标准形式去调用函数，即便在很多时候这是不可能的。 大多数的程序设计语言(包括Lisp,ML和命令式语言C和Java等)都被描述为严格类型语言，意思是使用了不正确形式参数的函数是形式不正确的。它们在实际上就是使用了应用次序和传值调用归约，但通常被成为及早求值策略。
3.正常次序 (Normal order) 最左边，最外部的表达式总是首先被归约，这也就意味着无论什么时候，参数都是再被归约之前就被替换进了抽象的函数体里面了。
4.传名调用 (Call by name) 和正常次序一样，但是不会在抽象的函数体中再进行归约，比如说，λx.(λx.x)x在这个策略中是正常形式, 虽然它包含了可归约的表达式(λx.x)x
5.传值调用 只有最外部的表达式被归约:一个表达式仅仅当它的右边已经被规约为一个值了才会被归约
6.传需求调用 “传需求调用”和传名调用类似，如果函数的实参被求值了，这个值就会被存储起来已备未来使用。它产生的结果和传名调用一样；但是如果函数的这个实参被调用了多次，那么传需求调用可以提高程序运行效率。它在现实语境中也被叫做惰性求值。
并行与并发
函数式编程在一开始就是面向并发处理的，这也得益于lambda的性质，lambda演算的Church-Rosser性质意味着归约(β归约)可以以任何顺序进行，甚至是并行来进行。这意味着各种不同的非确定性归约策略都是相近的。然而，lambda演算并不提供任何直接的并行结构。一个人可以添加像Futures结构体这样的并发结构体到lambda演算中去。相关的进程代数已经为了进程通信和并发而被研究了出来。
在λ-演算的基础上，发展起来的π-演算、χ-演算，成为近年来的并发程序的理论工具之一，许多经典的并发程序模型就是以π-演算为框架的。
图灵机
图灵机 (Turing machine, TM) 是由图灵在1936年提出的，它是一种精确的通用计算机模型，能模拟实际计算机的所有计算行为。 [1]
所谓的图灵机就是指一个抽象的机器，它有一条无限长的纸带，纸带分成了一个一个的小方格，每个方格有不同的颜色。有一个机器头在纸带上移来移去。机器头有一组内部状态，还有一些固定的程序。在每个时刻，机器头都要从当前纸带上读入一个方格信息，然后结合自己的内部状态查找程序表，根据程序输出信息到纸带方格上，并转换自己的内部状态，然后进行移动。
停机问题
停机问题（英语：halting problem）是逻辑数学中可计算性理论的一个问题。通俗地说，停机问题就是判断任意一个程序是否能在有限的时间之内结束运行的问题。该问题等价于如下的判定问题：是否存在一个程序P，对于任意输入的程序w，能够判断w会在有限时间内结束或者死循环。
通俗的说，停机问题就是判断任意一个程序是否会在有限的时间之内结束运行的问题。如果这个问题可以在有限的时间之内解决，则有一个程序判断其本身是否会停机并做出相反的行为，这时候显然不管停机问题的结果是什么都不会符合要求。所以这是一个不可解的问题。
停机问题本质是一高阶逻辑的不自恰性和不完备性。类似的命题有理发师悖论、全能悖论等。
非确定图灵机
定理：对于任意一个非确定型图灵机M，存在一个确定型图灵机M'，使得它们的语言相等，即 。
定理2：如果语言L被非确定型图灵机 M在多项式时间内接受，则一定存在多项式P使得语言L被时间复杂度为 的确定型图灵机程序所接受。
定理2说明了为什么在证明P=NP之前，所有的NPC问题都只有指数时间复杂度算法。 [1]
新浪博客：Lambda Calculus —— 叙述通俗朴素
http://blog.sina.com.cn/s/blog_68ffc7a4010169rl.html
在互联网行业中，每个人都希望自己的系统是能够水平扩展的，系统的计算能力也是如此。随着实践的深入，大家发现函数式编程能够天然得实现计算的并行化，实际上Map-reduce这样的并行框架本质上都是函数式编程思想下的产物。于是近些年来，Scala，Erlang这样的函数式编程语言越来越受到追捧，搞得程序员不会上个一两门函数式语言都不好意思出门打招呼。博主也不能免俗，准备也花点时间研究一下函数式编程，就从scala入手吧。在触及到具体的语言之前，我觉得还是很有必要先做一些理论储备，每一门计算机语言其实背后都蕴含着某一种思想的光芒。如果能够对这些基本的理论有一点体会或者理解，那么对于程序员提高自己的境界还是很有帮助的，至少在看到网上的大牛们讨论的时候不会一头雾水，经验上可能跟不上这些大牛，但思想一定要跟得上。函数式编程背后的理论基础就是Lambda calculus。作者花了点时间翻阅了一下维基百科http://en.wikipedia.org/wiki/Lambda_calculus，觉得有点体会，这里做个翻译点评。实际上维基百科中文也对该词条进行了翻译，但感觉中文只是英文词条的一个直译，很多东西含混不清，博主在这里对其进行一个评注，便于像我这样数学功底比较差的同仁们理解。
首先解释一下什么是Lambda caculus，Lambda 演算实际上是一套形式化系统，它的主要目的就是通过变量绑定以及代入的方法来表达计算，也就是说它能够从本质上来分析计算。正是因为如此，它在计算机理论界被广泛采用，成为设计函数式编程语言的理论工具。了解一点lamda演算，有助于你从本质上理解函数编程语言考虑问题和看待世界的方式。如果你能够理解到这个层次，也许你也能够在函数式编程思想的启迪下提出actor model这样的并行模型，成为万人膜拜的一代大牛。（憧憬一下....）
Lamda演算的概念十分重要，实际上Lambda 演算系统也不只一个，有uptyped Lambda calculus和typed Lambda calculus的区别，这两个演算系统实际上是不同的变种，至于到底有什么区别，我也不是很清楚，大概的意思是untyped Lambda calculus中的函数没有什么限制，而typed lamada calculus 中的函数所能接受的数据类型是有限制的。具体的区别，得靠理论界的专业人士来普及了，我也就不班门弄斧了。
Lambda演算的开山鼻祖是Alonzo Church，上个世纪30年代的大师。让我们记住他的名字吧。（好吧，只是记住他的名字，其实我也不知道他到底有多牛）
动机
首先来谈谈动机，Lambda演算到底想干什么。关键词就是函数function。我们知道在计算机语言中有一个很基本的概念就是递归函数，这个递归函数很烦人。记得在本科时学习C语言时，如果掌握了递归函数的写法，那C语言就算是基本入门了。而Lambda演算则为各式各样复杂的计算（包括递归计算）提供了一个统一的，简单的语义，从而使得我们能够正式得分析计算的各种特性。否则，计算只是一个口头上笼统的概念，有了Lambda演算，我们就有一个形式化系统来完整的分析到底什么是计算，它到底干了些什么，有什么特性。
首先让我们来看一个函数，identity function：
Id(x) = x
这个函数很简单，输入一个x，马上就返回这个输入值x。接下来再看另外一个函数，平方和函数：
Sqsum(x,y) = x*x + y*y
这个函数输入x,y，返回值是x和y的平方和x*x + y*y。
这是两个很简单的函数，通过观察这两个函数，我们可以观察到一些有用的东西，而这些观察正是Lambda演算主要思想的灵感来源。
首先第一个观察是，函数是不需要一个显式的名字的，比如函数
Sqsum(x,y) = x*x + y*y
其实可以写成一个匿名函数
(x,y) -> x*x +y*y
用专业一点的说法，这个函数可以表述成：
X，y对被映射成x*x + y*y。同样，类似的
Id(x) = x
也可以被写成一个匿名函数 x->x：输入被简单得映射成了自身。
第二个观察就是函数的参数（自变量）的名字是无关紧要的，这也就说
x->x
和
y->y
实际上表达的是同样的函数：identity function
类似的
(x,y) ->x*x + y*y 和
(u,v)->u*u + v*v
实际上表达的也是同一个函数。
最后一个观察就是，任何有两个自变量的函数，比如前面提到的sqsum函数，可以被重新写成另外一种形式的函数，这种新形式的函数只有一个输入变量，但输出返回的却是另外一个函数，而这个返回的函数同样也具有一个输入变量，输出返回另外一个函数，依次类推，直至终结。这有点和递归类似。举个例子吧，
(x,y) -> x*x + y*y
可以被写成
x->(y->x*x+y*y)
这种变化被称之为柯里化。有了柯里化，一个普通的具有多个输入自变量的函数都可以被转化成一系列的，只具有一个输入自变量的函数，这一系列的函数推导也被称之为partial application（片面应用）。
以上面的sqsum的例子而言，如果我们的输出参数是（5，2）我们可以进行如下推导：
((x,y) ->x*x + y*y)(5,2) = 5*5 + 2*2 = 29
如果使用了柯里化，则有
((x->(y->x*x+y*y))(5))(2)
=(y->5*5 + y*y)(2)
=5*5 + 2*2 = 29
我们看到柯里化和之前的函数都得到了一致的结果。需要注意的是，在函数链的第一个函数完成参数代入（x）之后，x*x就变成了一个常量。
Lambda演算
Lamda演算的描述是通过一种专门的Lambda词汇，这套词汇实际上定义了一种语法，以及基于该语法的一系列变换规则，这套规则可以操作Lambda词汇。这种变换规则可以被看作一种等价理论。正如上面所描述的，Lambda演算中的所有函数都是匿名函数，这些函数只有一个输入自变量，因为柯里化可以把多输入自变量的函数变换成只含有一个输入自变量的函数。
Lambda词汇
Lambda演算的语法定义了哪些表达式是有效的Lambda演算声明，同时也定义了哪些表达式不是有效的Lambda演算声明。就像C语言定义了哪些字符串是有效的C语言程序语法，哪些不是。一个有效的Lamda变化表达式被称之为一个Lambda词汇（Lambdaterm）。
下面的三条规则给出了一套归纳定义（递归定义），所有语法有效的Lambda词汇从根本上都源于这套归纳定义：
l 一个变量x，本身就是一个有效的Lambda词汇
l 如果t是一个Lambda词汇，x是一个变量，那么也是一个有效的Lambda词汇（也称之为Lambda抽象）
l 如果t和s都是Lambda词汇，那么ts也是一个有效的Lambda词汇（称之为application，中文叫应用）
任何其它的表达式都不是一个有效的Lambda词汇。如果一条表达式能够通过上述三条原则进行分解，那么这个表达式也可以称之为有效的Lambda词汇。
一个Lamda抽象实际上是一个匿名函数的定义，该函数接受一个输入自变量x，然后将x代入到表达式t中。举个例子，
就是一个函数
的Lamda抽象，表达式
实际上就是t。Lamda抽象只不过建立了一个函数，但并没有调用这个函数，相当于函数声明。
而一个application ts表达的就是一种调用动作，就是把s作为输入代入到函数t中，从而产生t(s)，相当于函数调用。
在Lambda演算中没有变量声明的概念。比如一个函数声明，Lambda演算就把y当作一个还没有定义的变量。Lambda抽象
在语法上是有效的，它代表一个函数，这个函数的行为就是把输入变量x和一个暂时还未知的变量y相加。
Lambda词汇也利用括号来区分词条。比如和
表示的就是不同的词条。
函数
在Lambda演算中，函数是所谓的一等公民，也就说它和值本质上是一样的，函数可以作为输入，函数也可以作为其它函数的返回值出现。
还是举例子吧，代表着identical 函数
。而
表示的是把identical函数应用到y上。另外一个例子，
代表的是constant函数
（函数永远返回y，不管输入x是什么）。
在Lambda演算中，函数的application是左优先的，也就说实际上意味着
.
在Lambda演算中，有所谓的“等价”和“推导”的概念，这两个概念可以把某个Lambda词汇通过“推导”变成“等价”的Lambda词汇。
Alpha等价
Alpha等价是Lambda词汇中定义的一个基本的等价形式。这个思路很简单，在Lambda抽象中变量名的选择实际上是无关紧要的。比如，λx.x和λy.y是alpha等价的Lambda词汇，它们实际上表示的都是一个函数。但Lambda词汇x和y则不是alpha等价的，因为他们并未绑定到一个Lambda抽象中。
接下来一个重要的概念就是beta推导，要理解beta推导则需要首先理解下面这几个概念。
自由变量
Lambda词汇的自由变量指的是还没有被绑定到某一个Lambda抽象中的这些变量。某一个表达式的自由变量集可以定义如下
- x的自由变量就是x
- λx.t的自由变量集就是t的自由变量集（x被排除在外）
- ts的自由变量集就是t的自由变量集和s的自由变量集的union。
例如， λx.x没有任何自由变量，而 λx.x+y的自由变量就是y。
Capture-avoiding替换
Capture-avoiding这个名词可能有点难于理解，简单解释一下。在Lamda演算中，正如前面提到的，变量名实际上是无关紧要的，比如(λx.(λy.yx))实际上和 (λa.(λb.ba))本质上是一样的函数。但这并不意味着这种变量名字的替换是没有约束的。看(λx.(λy.yx))的里面那个Lamda抽象：
(λy.yx)
从这个表达式来看，x是自由变量（未绑定任何Lamda抽象），如果按照上述原则（变量名无关），把y换成x，那么它可以被替换成：
(λx.xx)
但显然这么做是不可以的，这种替换下，最后一个x（原来的自由变量）被capture了，它此时被绑定到某一个Lamda抽象中去了。
因此替换一定要避免自由变量被capture，这就是所谓的Capture-avoided的由来。
假如t，s和r都是lamda词汇，而x，y都是变量，那么 表示的就是以capture-avoiding的方式将t中的x替换成r，给予这个定义，则有：
-
-
如果
-
如果x不等於y并且y不是r的自由变量
那么基于第5条的定义，
是一个成功的capture-avoiding替换，
也是一个capture-avoiding的很好的例子。
在定义5中，y不是r的自由变量，因此也被称之为y对于r来讲是fresh的，这个条件非常关键，这就确保了替换式capture-avoiding的，不会改变函数的含义。如果没有这个条件，则有，这就把一个常量函数
变成了一个identical函数
。
通常来讲，如果你发现fresh条件无法满足时，你可能需要进行一些重命名工作来获得。比如可以利用一个第三者自由变量z来重新命名，就可以得到
Beta推导
有了前面的准备我们就可以来定义beta推导了。Beta推导规则可以让一个(λx.t)s 形式的应用推导成词汇t[x := s]. 那么 (λx.t)s → t[x := s]就用来表示(λx.t)s beta推导成t[x := s]。举个例子，对于每个s，则有(λx.x)s → x[x := s] = s。这就意味着λx.x 真的是一个将x映射x的一个函数。类似的则有(λx.y)s → y[x := s] = y，这也揭示了常量函数λx.y的特性。因此beta推导可以用来揭示函数的特性。
Lambda演算可以看作一个理想的函数式编程语言，就像Haskell。基于这种视角，beta推导对应着一个计算步骤。这个计算步骤不断得被重复，直到没有更多的application可以进一步beta推导。
在untyped Lambda演算中（就是我们目前讨论的Lambda演算），推导过程未必可以终止（也就说满足没有更多的application可以进一步beta推导这个条件）。举例而言，(λx.xx)(λx.xx)，我们对这个Lambda词汇应用beta推导，就可以得到(λx.xx)(λx.xx) → (xx)[x := λx.xx] = (x[x := λx.xx])(x[x := λx.xx]) = (λx.xx)(λx.xx). 这就意味着，这个词条通过一步beta推导又变成了自身，因此这个词条永远没有终止条件。Untyped Lambda演算的另外一个方面就是演算不区分不同种类的数据，例如，你也许写了一个函数只用来操作数字，但是在untyped Lambda演算中，这个函数也可以用来处理真假值（true/false），string或者非数字的对象，这个函数可以处理任何类型的数据。
Formal定义
对于上面的概念，Lamda演算有一套完备严谨的书面定义，这就是通常说的formal definition。这就过于理论化了，这里就不多说了，反正说的就是上面的那么个意思，作为一般非学界的码农，也就没有必要纠结于这些形式化定义了。
推导
Lamda演算的关键就是推导，存在3种推导形式：
- Alpha变换
- Beta推导
- Eta变换
通常我们也会把上面的三种推导说成等价，比如如果两个表达式可以通过beta推导变成相同的表达式，我们就可以称之为这两个表达式是beta等价的，同理alpha等价，eta等价也是类似的定义。
关于推导，有一个专有名词redex，它是reducible expression的缩写。指的是那些可以利用上述3种规则进行推导的表达式，例如，(λx.M) N就是一个beta-redex，而如果x不是M的自由变量，λx.M x 就是eta-redex（这个会再后边解释）。Redex推导之后变成的表达式被称之为reduct。以前面刚刚提到的两个例子而言，各自对应的reduct就分别是 M[x:=N] 和M。
Alpha变换
这个概念前面已经提到过，就是说函数与具体的变量名称无关。两个函数如果是alpha等价的，那这两个函数本质上你可以认为是完全等价的。
实际上alpha变化还是有些需要注意的地方在里面。比如，当你对某一个Lambda抽象进行alpha变换时，发生重命名的变量一定是被绑定到同一个Lambda抽象中的。比如，λx.λx.x 的alpha变化可以是λy.λx.x，但不能是λy.λx.y，因为第一个x和第三个x没有被绑定到同一个Lambda抽象中去。
第二个需要注意的是capture avoiding的原则，这个在前面提到过，也不赘述。
在函数式编程语言中，alpha变化可以避免命名解析的一些问题。比如我们知道在编程语言中一般都有隐藏的概念（java，隐藏），通过alpha变化就可以把函数的变量换成各自不同的，这就避免了编程语言为了实现隐藏带来的复杂性，不会发生某一个变量名屏蔽了另外的变量名，这对具体编程语言的实现是很有意义的。
代入
代入被写作E[V := R]，就是将E中所有变量v出现的地方都用R代替。Lambda演算中的词汇的代入通过递归定义的方式来定义的：
x[x := N] ≡ N
y[x := N] ≡ y, if x ≠ y
(M1 M2)[x := N] ≡ (M1[x := N]) (M2[x := N])
(λx.M)[x := N] ≡ λx.M
(λy.M)[x := N] ≡ λy.(M[x := N]), if x ≠ y, provided y 不属于 FV(N)
为了代入Lamda抽象，有时候还必须得对表达式进行一下alpha变换。举个例子来说吧，代入(λx.y)[y := x]得到(λx.x)就是不对的，因为代入的x本来是个自由变量，结果一代入就被绑定了。正确的代入结果应该是(λz.x)，有点像是对Lambda抽象进行了一个alpha变化，但需要注意的是alpha变化和代入的定义是完全不同的。
Beta推导
Beta推导其实前面也讲过，它是为了揭示函数application的特性。Beta推导的定义是通过代入来定义的：
((λV.E) E′)的beta推导就是E[V := E′].
举例，有一个2，7，x的编码函数((λn.n×2) 7)，其beta推导就有((λn.n×2) 7) → 7×2.
Eta变换
Eta变换是为了揭示扩展性，它是说当且仅当两个函数对所有的参数都能产生相同的结果的时候，我们才认为这两个函数是相同的。 如果x是f中的变量且不是自由变量，λx.(f x)可以Eta变换成f。
Notation:
为了保证Lambda表示式的简洁明快，会有如下的约定：
- 不保留最外层的括号：MN实际上就是(MN)
- Application是左优先的：MNP实际上就是(MN)P
- Lambda抽象的函数体是尽可能向右衍生的：λx.M N实际上是λx.(M N) 而并不是(λx.M) N
- 多个连续的Lambda抽象是可以缩减的：λx.λy.λz.N可以缩减为λxyz.N
Lambda演算的应用
有了上面这些定义，我们就可以利用Lambda演算来做一些推导，来看看函数式编程语言的一些特性如何来用Lambda演算来进行表达。
自然数
比如自然数0，1，2，3可以如下定义：
0 := λf.λx.x
1 := λf.λx.f x
2 := λf.λx.f (f x)
3 := λf.λx.f (f (f x))
怎么理解呢？先看0：
λf.λx.x := f -> (x->x)
也就说变量f在Lambda抽象中没有起到任何作用，这就是0。
再看1：
λf.λx.f x := f->(x->f(x))
fx是一个函数调用，表示的是把x应用到f得到f(x)。那整个表达式的意思就是描述这么一个函数，输入变量f，x（f，x可能是表达式，是合法的Lambda词汇）得到f（x）这样的效果，f进行了一次递归运算。
接着就是2：
λf.λx.f (f x) ：= f->(x->f(f(x)))
这里输入f，x得到f(f(x))，f进行了两次递归运算。
这个定义很晦涩，f的参与递归运算次数（阶数）就是自然数，这其实某种程度上反映了自然数的本质，2实际上就是1的二阶。
操作符
接下来，看看自增（++）函数的操作定义：
SUCC := λn.λf.λx.f (n f x)
自增函数以n作为输入，返回n+1. 这个定义看起来也很是晦涩，但实际上基于前面的定义，SUCC的推导是很完备的。首先看nfx, 基于前面的定义，其中f总共出现了n次。将n代入nfx则有：
将nfx代入SUCC的定义，则有:
这下f总共出现n+1次，根据上面的定义，这不就是n+1嘛。
PLUS的定义也很简单：
PLUS := λm.λn.λf.λx.m f (n f x)
首先看nfx，前面推导过了，有
再看mf(nfx)，则有：
将前面得到的nfx代入mf(nfx)，则有：
这样f就一共出现了m+n次，那最终则有：
这就是m+n。呵呵，很完美吧。
逻辑判断
接下来看看逻辑判断的例子：
TRUE := λx.λy.x
FALSE := λx.λy.y
AND := λp.λq.p q p
上面这三个定义是正确的，为什么是正确的呢？下面的推导可以帮助你理解它的正确性：
AND TRUE FALSE
≡ (λp.λq.p q p) TRUE FALSE →β TRUE FALSE TRUE
≡ (λx.λy.x) FALSE TRUE →β FALSE
递归函数
最后来看看递归函数的例子，递归函数也可以归结为Lambda演算。根据递归的概念，递归函数需要使用递归函数自身。如果用Lambda演算表示这种概念，一个直接的想法是递归函数也许可以表示成这种形式：(λx.x x) y 。xx表示的是把自身作为输入又传递给自身，由于两个x都指向的是y，那么y一定有一个特殊的能力：将Lambda表达式自身作为参数传递给自己。
举个阶乘的例子吧，阶乘的递归定义大家都很清楚，可以写成这样：
F(n) = 1, if n = 0; else n × F(n − 1).
为了描述这个函数，需要引入一个中间Lambda词汇r：
G := λr. λn.(1, if n = 0; else n × (r (n−1)))
其中r能将自身作为输入传递给自身。什么样的Lambda词汇这么神奇，能够具有这样的特性呢？答案就是Fix-Point combinator。怎么理解这个东西呢？大家可能知道函数的fix-point，所谓函数的fix-point指的是函数f的某一个或几个值点x，使得f(x) = x。比如x^2的fix-point就是0和1，因为0^2 = 0，1 ^2 =1。这是值域空间的fix-point，如果x可以是函数的话，这就是所谓的Fix-point combinator，它的特性就是Yg = g（其中Y就是Fix-Point combinator）。找到了Y（Fix-point comibnator），把Y作为r代入到G中，就可以得到阶乘函数的最终定义。因此基于上面的定义，就可以得到阶乘函数F的Lambda演算定义:
F(n) =(YG)n
其中G := λr. λn.(1, if n = 0; else n × (r (n−1)))
至于Y，实际上有很多可能的定义满足这样Fix-point combinator的特性，最简单的就是
Y := λg.(λx.g (x x)) (λx.g (x x))
通过上面的描述，我们可以得出，任何递归函数都可以归结为一个Lambda application （YG），其中G和具体的函数相关，而Y则是统一的，和具体的函数无关。通过分析递归函数的Lambda演算形式，可以帮助我们分析递归函数的本质特性，同时也有助于我们在设计函数式语言时考虑递归的实现。
Lambda演算与函数式语言的关系
讲了这么多，有人可能会问？Lambda演算和函数式编程语言到底有什么关系?
实际上你可以认为任何面向过程的编程语言（包括函数式编程语言）都是某种形式的Lambda演算，只不过这些语言同时又提供了一些额外的过程抽象。
Lambda演算重新精炼了函数的概念，并且使得函数像值一样成为“一等公民”，但这也大大增加了函数式编程语言实现的复杂性。
匿名函数
在古老的Lisp语言中，平方函数可以被表示成如下的一个Lambda表达式：
(lambda (x) (*xx))
上面的例子是一个表达式用来演算一个函数。符号Lambda创建了一个匿名函数，这个函数的参数是x，而表达式（*xx）是函数体。其它的函数式语言比如Haskell的匿名函数创建也采用了同样的语法，因此，匿名函数有时候也被称之为Lamda表达式。
像Pascal这样的命令式语言很早就支持通过函数指针把子程序当作参数传递给其他的子程序。但是仅仅有函数指针还不够，要想让函数成为编程语言的“一等公民”，必须要让函数的新的实例在runtime时可以被动态创建。函数的动态创建在C++，Scala，C#等语言中已经得以支持。
推导策略
对于函数式编程语言而言，其实质都是Lamda演算，函数式语言的语法都对应着相应的Lambda词汇。根据前面的定义，这些Lamda词汇在编译执行的时候往往都需要进行推导，比如beta推导，eta推导，alpha推导等等，这些推导什么时候进行，这就是各个函数式语言需要考虑的问题，有的函数式语言是eager evaluation的策略，而有的函数式语言采用的则是lazy evaluation的策略。这些具体的策略有什么不同，这里就不赘述了，作为码农大概了解一下即可。
关于复杂度
Beta推导的思想看起来很简单，但它并不是一个原子的过程，那么这就意味着在估计计算复杂度时它的代价是颇为可观的，并不能忽略不计。为了精确估计复杂度，编译器需要找出绑定变量V在表达式E中出现的所有位置，这就意味着时间开销，编译器同时又必须用某种方法来存放这些绑定变量的位置，这就意味着空间开销。如果简单的搜索表达式E中V出现的位置，这是一个o(n)的复杂度（其中n为E的长度）。Lambda演算采用了一些特殊的方法来搜索并保存这些绑定变量的出现位置，比如explicit substitution和director strings等等，这里就不再赘述。
并发
Lambda演算的特性决定了演算（beta推导）可以以任何顺序被执行，甚至是并行。这就意味着各种推导策略之间实际上相互之间是有关联的。Lambda演算没有为并行提供一种显式的支持，函数式语言可以为Lambda演算添加类似Future之类的支持，实际上还有其他的并发机制被开发出来并添加到Lambda演算。
语义
最后的问题是，Lambda词汇的语义到底是什么？你可以理解为寻找集合D，该集合D和将函数自身作为输入参数的函数的空间D->D是同构的。（好吧，原谅无知的我，我终究没看懂这一段。。。但其大概意思就是说Lambda词汇的目的就是寻找一个集合D，而且70年代又有大牛理论证明这个集合是存在的，从而使得Lambda演算的理论模型得以成立）
总结下，通过Lambda演算，你可以理解函数式语言的实现，理解函数式语言为什么能够并发。当然，对于一般码农来讲，理解这个似乎也不能帮助你的工作，但多一点深入的理解总没有什么坏处。
我的最爱Lambda演算——开篇
这篇通过 例子 把 alpha - 归约 和 beta 归约讲清楚了
（在这个帖子的原始版本里，我试图用一个JavaScript工具来生成MathML。但不太顺利：有几个浏览器没法正确的渲染，在RSS feed里也显示的不好。所以我只好从头开始，用简单的文本格式重新写一遍。）
计算机科学，尤其是编程语言，经常倾向于使用一种特定的演算：Lambda演算（Lambda Calculus）。这种演算也广泛地被逻辑学家用于学习计算和离散数学的结构的本质。Lambda演算伟大的的原因有很多，其中包括：
- 非常简单。
- 图灵完备。
- 容易读写。
- 语义足够强大，可以从它开始做（任意）推理。
- 它有一个很好的实体模型。
- 容易创建变种，以便我们探索各种构建计算或语义方式的属性。
Lambda演算易于读写，这一点很重要。它导致人们开发了很多极为优秀的编程语言，他们在不同程度上都基于Lambda演算：LISP，ML和Haskell语言都极度依赖于Lambda演算。
Lambda演算建立在函数的概念的基础上。纯粹的Lambda演算中，一切都是函数，连值的概念都没有。但是，我们可以用函数构建任何我们需要的东西。还记得在这个博客的初期，我谈了一些关于如何建立数学的方法么？我们可以从无到有地用Lambda演算建立数学的整个结构。
闲话少说，让我们深入的看一看LC（Lambda Calculus）。对于一个演算，需要定义两个东西：语法，它描述了如何在演算中写出合法的表达式；一组规则，让你符号化地操纵表达式。
Lambda演算的语法
Lambda演算只有三类表达式：
- 函数定义：Lambda演算中的函数是一个表达式，写成：lambda x . body，表示“一个参数参数为x的函数，它的返回值为body的计算结果。” 这时我们说：Lambda表达式绑定了参数x。
- 标识符引用（Identifier reference）：标识符引用就是一个名字，这个名字用于匹配函数表达式中的某个参数名。
- 函数应用（Function application）：函数应用写成把函数值放到它的参数前面的形式，如(lambda x . plus x x) y。
柯里化
在Lambda演算中有一个技巧：如果你看一下上面的定义，你会发现一个函数（Lambda表达式）只接受一个参数。这似乎是一个很大的局限—— 你怎么能在只有一个参数的情况下实现加法？
这一点问题都没有，因为函数就是值。你可以写只有一个参数的函数，而这个函数返回一个带一个参数的函数，这样就可以实现写两个参数的函数了——本质上两者是一样的。这就是所谓的柯里化（Currying），以伟大的逻辑学家Haskell Curry命名。
例如我们想写一个函数来实现x + y。我们比较习惯写成类似：lambda x y . plus x y之类的东西。而采用单个参数函数的写法是：我们写一个只有一个参数的函数，让它返回另一个只有一个参数的函数。于是x + y就变成一个单参数x的函数，它返回另一个函数，这个函数将x加到它自己的参数上：
lambdax. ( lambday. plus x y )
现在我们知道，添加多个参数的函数并没有真正添加任何东西，只不过简化了语法，所以下面继续介绍的时候，我会在方便的时候用到多参数函数。
自由标识符vs. 绑定标识符
有一个重要的语法问题我还没有提到：闭包（closure）或者叫完全绑定（complete binding）。在对一个Lambda演算表达式进行求值的时候，不能引用任何未绑定的标识符。如果一个标识符是一个闭合Lambda表达式的参数，我们则称这个标识符是（被）绑定的；如果一个标识符在任何封闭上下文中都没有绑定，那么它被称为自由变量。
- lambda x . plus x y：在这个表达式中，y和plus是自由的，因为他们不是任何闭合的Lambda表达式的参数；而x是绑定的，因为它是函数定义的闭合表达式plus x y的参数。
- lambda x y . y x ：在这个表达式中x和y都是被绑定的，因为它们都是函数定义中的参数。
- lambda y . (lambda x . plus x y)：在内层演算lambda x . plus x y中，y和plus是自由的，x是绑定的。在完整表达中，x和y是绑定的：x受内层绑定，而y由剩下的演算绑定。plus仍然是自由的。
我们会经常使用free(x)来表示在表达式x中自由的标识符。
一个Lambda演算表达式只有在其所有变量都是绑定的时候才完全合法。但是，当我们脱开上下文，关注于一个复杂表达式的子表达式时，自由变量是允许存在的——这时候搞清楚子表达式中的哪些变量是自由的就显得非常重要了。
Lambda演算运算法则
Lambda演算只有两条真正的法则：称为Alpha和Beta。Alpha也被称为「转换」，Beta也被称为「规约」。
Alpha转换
Alpha是一个重命名操作; 基本上就是说，变量的名称是不重要的：给定Lambda演算中的任意表达式，我们可以修改函数参数的名称，只要我们同时修改函数体内所有对它的自由引用。
所以—— 例如，如果有这样一个表达式：
lambda x . if(= x 0) then1elsex ^ 2
我们可以用Alpha转换，将x变成y（写作alpha[x / y]），于是我们有：
lambda y . if(= y 0) then1elsey ^ 2
这样丝毫不会改变表达式的含义。但是，正如我们将在后面看到的，这一点很重要，因为它使得我们可以实现比如递归之类的事情。
Beta规约
Beta规约才是精彩的地方：这条规则使得Lambda演算能够执行任何可以由机器来完成的计算。
Beta基本上是说，如果你有一个函数应用，你可以对这个函数体中和对应函数标识符相关的部分做替换，替换方法是把标识符用参数值替换。这听起来很费解，但是它用起来却很容易。
假设我们有一个函数应用表达式：“ (lambda x . x + 1) 3 “。所谓Beta规约就是，我们可以通过替换函数体（即“x + 1”）来实现函数应用，用数值“3”取代引用的参数“x”。于是Beta规约的结果就是“3 + 1”。
一个稍微复杂的例子：(lambda y . (lambda x . x + y)) q。这是一个挺有意思的表达式，因为应用这个Lambda表达式的结果是另一个Lambda表达式：也就是说，它是一个创建函数的函数。这时候的Beta规约，需要用标识符“q”替换所有的引用参数“y”。所以，其结果是“ lambda x . x + q “。
再给一个让你更不爽的例子：“ (lambda x y. x y) (lambda z . z * z) 3 “。这是一个有两个参数的函数，它(的功能是)把第一个参数应用到第二个参数上。当我们运算时，我们替换第一个函数体中的参数“x”为“lambda z . z * z “；然后我们用“3”替换参数“y”，得到：“ (lambda z . z * z) 3 “。再执行Beta规约，有“3 * 3”。
Beta规则的形式化写法为：
lambda x . B e = B[x := e] iffree(e) subset free(B[x := e])
最后的条件“if free(e) subset free(B[x := e])”说明了为什么我们需要Alpha转换：我们只有在不引起绑定标识符和自由标识符之间的任何冲突的情况下，才可以做Beta规约：如果标识符“z”在“e”中是自由的，那么我们就需要确保，Beta规约不会导致“z”变成绑定的。如果在“B”中绑定的变量和“e”中的自由变量产生命名冲突，我们就需要用Alpha转换来更改标识符名称，使之不同。
例子更能明确这一点：假设我们有一个函数表达式，“ lambda z . (lambda x . x + z) “，现在，假设我们要应用它：
(lambdaz . (lambdax . x + z)) (x+2)
参数“(x + 2)”中，x是自由的。现在，假设我们不遵守规则直接做Beta规约。我们会得到：
lambdax . x + x + 2
原先在“x + 2”中自由的的变量现在被绑定了。再假设我们应用该函数：
(lambdax . x + x + 2) 3
通过Beta规约，我们会得到“3 + 3 + 2”。
如果我们按照应有的方式先采用Alpha转换，又该如何？
- 由 alpha[x/y] 有: (lambda z . (lambda y . y + z)) (x + 2)
- 由Beta规约： (lambda y . y + x + 2) 3
- 再由Beta规约： 3 + x + 2 。
“3 + x + 2”和“3 + 3 + 2”是非常不同的结果！
规则差不多就是这些。还有另外一个规则，你可以选择性地加一条被称为Eta-规约的规则，不过我们将跳过它。我在这里描述了一个图灵完备—— 完整有效的计算系统。要让它变得有用，或看它如何用来做些有实际意义的事情，我们还需要定义一堆能让我们做数学计算的基本函数，条件测试，递归等，我将在下一篇文章讨论这些。
我们也还没有定义Lambda-演算的模型呢。（原作者在这里和这里讨论了模型的概念。）模型实际上是非常重要的！逻辑学家们在摆弄了LC好几年之后，才为其想出一个完整的模型，这是件非常重要的事情，因为虽然LC看起来是正确的，但在早期为它定义一个模型的尝试，却是失败的。毕竟，请记住，如果没有一个有效的模型，这意味着该系统的结果是毫无意义的！
http://cgnail.github.io/academic/lambda-1/
Alpha转换
Alpha是一个重命名操作; 基本上就是说，变量的名称是不重要的：给定Lambda演算中的任意表达式，我们可以修改函数参数的名称，只要我们同时修改函数体内所有对它的自由引用。
Beta规约
Beta规约才是精彩的地方：这条规则使得Lambda演算能够执行任何可以由机器来完成的计算。
Beta基本上是说，如果你有一个函数应用，你可以对这个函数体中和对应函数标识符相关的部分做替换，替换方法是把标识符用参数值替换。这听起来很费解，但是它用起来却很容易。
见上一篇文章的 capture-avoiding：替换一定要避免自由变量被 capture
http://blog.sina.com.cn/s/blog_68ffc7a4010169rl.html
[x/y]：中括号表示把x 替换成 y （ alpha-归约）
Good Math/Bad Math，原英文博客来一发：
原文来自Good Math/Bad Math的系列连载，全文分7章，本篇是第1章。中文博客负暄琐话对这个系列的前6章做过翻译，强迫症表示忍受不了「下面没有了」，于是自己动手做了全套。这里只对原文做了翻译，而“负暄琐话”的版本则加上了很多掌故，使得阅读起来更有趣味性。
| Good Math, Bad Math | Lambda演算系列之七 |
老外写了系列文章，cgnail做了中文翻译，非常棒，每篇翻译都有原文的链接。
- 我的最爱Lambda演算——开篇 · cgnail's weblog
- 阿隆佐.丘奇的天才之作——lambda演算中的数字 · cgnail's weblog
- Lambda演算中的布尔值和选择 · cgnail's weblog
- 为什么是Y？ · cgnail's weblog
- 从Lambda演算到组合子演算 · cgnail's weblog
- Lambda演算的类型 · cgnail's weblog
- 终章，Lambda演算建模——程序即证明！ · cgnail's weblog
https://imonce.github.io/2019/04/24/Lambda演算精简教程/
14 Apr 2017 计算机中的内存
14 Apr 2017 C语言中常见的内存错误
14 Apr 2017 系统的启动和引导
20 Sep 2014 Good Math/Bad Math的Lambda演算系列的中文翻译
16 Sep 2014 终章，Lambda演算建模——程序即证明！
16 Sep 2014 Lambda演算的类型
15 Sep 2014 从Lambda演算到组合子演算
15 Sep 2014 为什么是Y？
15 Sep 2014 Lambda演算中的布尔值和选择
15 Sep 2014 阿隆佐.丘奇的天才之作——lambda演算中的数字
15 Sep 2014 我的最爱Lambda演算——开篇
再来看 知乎专栏《你好，类型》：
https://thzt.github.io/categories/Logic/
Gradual Typing05-31 你好，类型（十）：Parametric polymorphism10-21 你好，类型（九）：Let polymorphism10-14 你好，类型（八）：Subtype10-13 你好，类型（七）：Recursive type09-23 你好，类型（六）：Simply typed lambda calculus09-19 你好，类型（五）：Predicate logic09-16 Hilbert-style和Gentzen-style演绎系统09-15 你好，类型（四）：Propositional logic09-10 你好，类型（三）：Combinatory logic09-07 你好，类型（二）：Lambda calculus09-06 你好，类型（一）：开篇09-05 类型理论之拙见05-19 形式证明与逻辑推理03-01 数理逻辑定义汇总11-23 模型观 |
当前标签: 简单易懂的程序语言入门小册子
https://www.cnblogs.com/skabyy/tag/简单易懂的程序语言入门小册子/
古霜卡比2014-05-16 05:46 阅读:780 评论:2
简单易懂的程序语言入门小册子（8）：基于文本替换的解释器，小结
古霜卡比2014-05-08 08:55 阅读:877 评论:5
简单易懂的程序语言入门小册子（7）：基于文本替换的解释器，加入continuation，重构解释器
古霜卡比2014-05-03 10:27 阅读:638 评论:0
简单易懂的程序语言入门小册子（1.5）：基于文本替换的解释器，递归定义与lambda演算的一些额外说明
古霜卡比2014-05-02 11:41 阅读:751 评论:0
简单易懂的程序语言入门小册子（6）：基于文本替换的解释器，引入continuation
古霜卡比2014-04-28 11:18 阅读:923 评论:2
简单易懂的程序语言入门小册子（5）：基于文本替换的解释器，递归，不动点，fix表达式，letrec表达式
古霜卡比2014-04-23 09:52 阅读:869 评论:4
简单易懂的程序语言入门小册子（4）：基于文本替换的解释器，递归，如何构造递归函数，Y组合子
古霜卡比2014-04-21 10:24 阅读:1148 评论:7
简单易懂的程序语言入门小册子（3）：基于文本替换的解释器，let表达式，布尔类型，if表达式
古霜卡比2014-04-19 10:10 阅读:916 评论:0
简单易懂的程序语言入门小册子（2）：基于文本替换的解释器，加入整数类型
古霜卡比2014-04-18 09:44 阅读:1040 评论:2
简单易懂的程序语言入门小册子（1）：基于文本替换的解释器，lambda演算
古霜卡比2014-04-17 11:29 阅读:2490 评论:5
Functor 的作用就是应用一个函数到一个上下文中的值：
而 Applicative 的作用则是应用一个上下文中的函数到一个上下文中的值：
Monad 的作用跟 Functor 类似，也是应用一个函数到一个上下文中的值。不同之处在于，Functor 应用的是一个接收一个普通值并且返回一个普通值的函数，而 Monad 应用的是一个接收一个普通值但是返回一个在上下文中的值的函数：
http://blog.leichunfeng.com/blog/2015/11/08/functor-applicative-and-monad/