看到一个关于lambda的非正式描述，记下来

在 lambda 演算中，每个表达式都代表一个只有单独参数的函数，这个函数的参数本身也是一个只有单一参数的函数，同时，函数的值是又一个只有单一参数的函数。函数是通过 lambda 表达式匿名地定义的，这个表达式说明了此函数将对其参数进行什么操作。例如，“加 2”函数 f(x) = x + 2 可以用 lambda 演算表示为 λ x. x + 2 (λ y. y + 2 也是一样的，参数的取名无关紧要) 而 f(3) 的值可以写作 (λ x. x + 2) 3。函数的作用 (application) 是左结合的：f x y = (f x) y。考虑这么一个函数：它把一个函数作为参数，这个函数将被作用在 3 上：λ x. x 3。如果把这个 (用函数作参数的) 函数作用于我们先前的“加 2”函数上：(λ x. x 3) (λ x. x+2)，则明显地，下述三个表达式：

    (λ x. x 3) (λ x. x+2)   与    (λ x. x + 2) 3    与    3 + 2

是等价的。有两个参数的函数可以通过 lambda 演算这么表达：一个单一参数的函数的返回值又是一个单一参数的函数 (参见 Currying)。例如，函数 f(x, y) = x - y 可以写作 λ x. λ y. x - y。下述三个表达式：

    (λ x. λ y. x - y) 7 2    与    (λ y. 7 - y) 2    与    7 - 2

也是等价的。然而这种 lambda 表达式之间的等价性无法找到一个通用的函数来判定。

并非所有的 lambda 表达式都可以规约至上述那样的确定值，考虑

    (λ x. x x) (λ x. x x)

或

    (λ x. x x x) (λ x. x x x)

然后试图把第一个函数作用在它的参数上。 (λ x. x x) 被称为 ω 组合子 (combinator)，((λ x. x x) (λ x. x x)) 被称为 Ω，而 ((λ x. x x x) (λ x. x x x)) 被称为 Ω2，以此类推。

若仅形式化函数作用的注记而不允许 lambda 表达式，就得到了组合子逻辑 (combinatory logic)。

α-变换

Alpha-变换规则表达的是，被绑定变量的名称是不重要的。比如说 λx.x 和 λy.y 是同一个函数。尽管如此，这条规则并非像它看起来这么简单，关于被绑定的变量能否由另一个替换有一系列的限制。

Alpha-变换规则陈述的是，若 V 与 W 均为变元，E 是一个 lambda 表达式，同时 E[V/W] 是指把表达式 E 中的所有的 V 的自由出现都替换为 W，那么在 W 不是 E 中的一个自由出现，且如果 W 替换了 V，W 不会被 E 中的 λ 绑定的情况下，有

    λ V. E == λ W. E[V/W]

这条规则告诉我们，例如 λ x. (λ x. x) x 这样的表达式和 λ y. (λ x. x) y 是一样的。

β-消解

Beta-消解规则表达的是函数作用的概念。它陈述了若所有的 E' 的自由出现在 E [V/E' ] 中仍然是自由的情况下，有

    ((λ V. E ) E' ) == E [V/E' ]

成立。

== 关系被定义为满足上述两条规则的最小等价关系 (即在这个等价关系中减去任何一个映射，它将不再是一个等价关系)。

对上述等价关系的一个更具操作性的定义可以这样获得：只允许从左至右来应用规则。不允许任何 beta 消解的 lambda 表达式被称为范式。并非所有的 lambda 表达式都存在与之等价的范式，若存在，则对于相同的形式参数命名而言是唯一的。此外，有一个算法用户计算范式，不断地把最左边的形式参数替换为实际参数，直到无法再作任何可能的消解为止。这个算法当且仅当 lambda 表达式存在一个范式时才会停止。Church-Rosser 定理 说明了，当且仅当两个表达式等价时，它们会在形式参数换名后得到同一个范式。
[编辑]

η-变换

前两条规则之后，还可以加入第三条规则，eta-变换，来形成一个新的等价关系。Eta-变换表达的是外延性的概念，在这里外延性指的是，两个函数对于所有的参数得到的结果都一致，当且仅当它们是同一个函数。Eta-变换可以令 λ x . f x 和 f 相互转换，只要 x 不是 f 中的自由出现。下面说明了为何这条规则和外延性是等价的：

若 f 与 g 外延地等价，即，f a == g a 对所有的 lambda 表达式 a 成立，则当取 a 为在 f 中不是自由出现的变量 x 时，我们有 f x == g x，因此 λ x . f x == λ x . g x，由 eta-变换 f == g。所以只要 eta-变换是有效的，会得到外延性也是有效的。

相反地，若外延性是有效的，则由 beta-消解，对所有的 y 有 (λ x . f x) y == f y，可得 λ x . f x == f，即 eta-变换也是有效的。

递归是一种以函数自身迭代自身变元的算法，一般是通过函数自身来定义函数的方式实现。表面看来 lambda 演算不允许递归，其实这是一种对递归的误解。考虑阶乘函数 f(n) 一般这样递归地定义：

    f(n) = 1, 若 n = 0; n·f(n-1), 若 n>0.

λ语言：

    FACT = λ n. n (λ u. MULT n (FACT (PRED n))) 1

用 Y-组合子 在 λ语言 中合法地定义：

    FACT = Y (λ g. λ n. n (λ u. MULT n (g (PRED n))) 1)

    Y = λ f. ((λ x. f (x x)) (λ x. f (x x)))