1. 匿名函数
现在很多种编程语言都支持匿名函数了，
例如，C# 3.0，C++ 11和Java 8中的lambda表达式，
又例如，Python 2.2.2中的lambda，ECMAScript 3的匿名函数，
ECMAScript 2015的箭头函数（arrow function）等等。
更不论，Haskell，Lisp，Standard ML，这些函数式编程语言了。
越来越多的语言拥抱匿名函数，是因为在很多场景中，我们无需给函数事先指定一个名字，
并且结合词法作用域和高阶函数，会使某些问题用更直观的方式得以解决。
从理论上来讲，匿名函数具有和一般函数同样的计算能力，
使用某些技术手段，可以让匿名函数支持递归运算，从而完成任何图灵可计算的任务。
然而，要想理解这一切，我们首先还得静下心来，从基础的演算开始吧。
2. 自然数
演算听起来是一个高大上的概念，实际上它只是一套“符号推导系统”，
人们首先定义某些合法的符号，然后再定义一些符号推导规则，
最后，就可以计算了，从一堆合法的符号得到另一堆，这种推导过程称之为“演算”。
为了让演算更容易被接受，我们暂时先岔开话题，看看自然数是怎么定义的。
2.1 Peano系统
1889年，皮亚诺（Peano）为了给出自然数的集合论定义，
他建立了一个包含5条公设的公理系统，后人称之为Peano系统。
Peano系统是满足以下公设的有序三元组，
其中为一个集合，是到的函数，为首元素，
（1）
（2）在下是封闭的
（3）不在的值域中
（4）是单射
（5）如果的子集满足，，且在下封闭，则。
2.2 后继
设为一个集合，我们称为的后继，记作，
求集合后继的操作，称为后继运算。
例如，
。
2.3 归纳集
设为一个集合，若满足，
（1）
（2），
则称是归纳集。
例如，是一个归纳集。
从归纳集的定义可知，是所有归纳集的元素，
于是，可以将它们定义为自然数，自然数集记为。
设，满足，则称为后继函数，
则可以证明是一个Peano系统。
3. 演算
演算，是1930年由邱奇（Alonzo Church）发明的一套形式系统，
它是从具体的函数定义，函数调用和函数复合中，抽象出来的数学概念。
3.1 语法
形式上，演算由3种语法项（term）组成，
（1）一个变量本身，是一个合法的项，
（2），是一个合法的项，称为从项中抽象出，
（3），是一个合法的项，称为将应用于。
例如，，，，都是合法的项。
为了简化描述，我们通常会省略一些括号，以上三个项可以写成，
，，，
对于形如的项来说，“”后面会向右包含尽量多的内容。
现在我们有了一堆合法的字符串了。
可是，在给定推导规则之前，这些字符串之间都是没有关联的。
而且，我们也还没有为这些符号指定语义，它们到底代表什么也是不清楚的。
很显然给这些符号指定不同的推导规则，会得到不同的公理系统，
在众多演算系统中，最简单的是系统，它指定了和两种变换。
3.2 变换
设项中包含了，
则我们可以把中所有自由出现的，全都换成y，即，
这种更名变换，称为变换。
其中，“自由出现”指的是不被其他抽象所绑定，
例如，中，是自由的，
而就不是自由的，因为它被绑定了。
如果可以经过有限步变换转换为，就写为。
例如，
3.3 变换
形如的项，可以经由变换转换为，
指的是，把中所有自由出现的都换成。
如果可以经过有限步变换转换为，就写为。
例如，
我们发现，某些项，可以无限进行变换。
而那些最终会终止的变换的结果，称为范式（ normal form）。
3.4 邱奇编码
现在我们有公理系统了，就可以依照或变换，对任意合法的项进行变换。
假设我们有一个项，，
还有另外一个项，，记为，
我们来计算，，
可得，，
我们再运用一次，。
我们发现每次应用，都会给中加一个，
最终我们可以得到以下这些项，
如果我们记，，，
，
我们就得到了自然数的另一种表示方式，称之为邱奇编码。
可以看到邱奇编码与归纳集之间有异曲同工之妙。
3.5 语义
到目前为止，我们并未谈及项到底表示什么含义，
虽然看起来像是函数定义，看起来像是函数调用。
我们谨慎的使用公理化方法，从什么是合法的项出发，
定义系统中的公理——合法的项，
然后又指定了该系统中的推导规则——和变换，
最终得到了一个形式化的公理系统（公理+推导规则）。
后文中，我们将谈及项的语义，然后再逐渐给它加上类型。