lambda演算

lambda calculus

一种符号表述的演算形式系统。由阿隆佐·邱奇 在 1930s 提出。

lambda 演算被用来证明判定问题是没有答案的。也明确定义了可计算理论中的可计算性。也是现代编程语言中函数式编程的重要理论基础。

理论上和图灵机等效，也就是说，图灵机可计算的，lambda演算一定可以计算。

$$\lambda x.M$$

上述公式含义：“x 作为参数，代入到函数 M 中，最终得到的值”

ref: Lambda演算学习笔记 - MDA之路 - BlogJava

基本定义

演算系统中的合法字符：

• x1, x2, x3 以及各种变元
• → 表示规约
• = 表示等价
• $\lambda$ ( ) 三个符号

对上述字符的理解：

• 变量：x，表示参数或者值
• 抽象：$\lambda x.e$ 表示输入参数 x 返回表达式 e 的函数。
• 应用：e0 e1 ，将函数 e0 作用与函数 e1

关于 $\lambda$ 项的抽象：

• 函数的应用（代入）：用括号 (M N) 表示。
  • 例如，$(\lambda x.x+2)2$ 是将 2 代入到前面的表达式中计算。因为未定义 +，所以以上表述是非法的，仅用来表达这个意思
• 函数的抽象：$\lambda x.M$ ，表示参数为 x，函数体为 M 的米名函数

左结合性：所有的 lambda 演算为从做往右结合。

自由出现法则

出现在 lambda 演算中的变量有两种表示方式：

• 自由变量：变量独立出现在表达式中
• 绑定变量：变量被绑定出现，例如 $\lambda x$ 即为被绑定的 x

规约规则：简化方法

• $\alpha$ 变换：变量名称可以随意替换，λx.x ≡ λy.y
• $\beta$ 规约：函数应用（代入），将 $\lambda$ 后面的项代入到之前绑定的项目中。(λx.x) y → y
• $\eta$ 规约：若x不在e中自由出现，则λx.e x → e ，就是将函数消除，成为单一的变量。

合流性：不论顺序如何，最终结果唯一。

特殊的表达式

• Omega 组合子（无限循环）：$\Omega =(\lambda x.xx)(\lambda x.xx)$
• Y组合子（递归）：$Y=\lambda f.(\lambda x.f(xx))(\lambda x.f(xx))$
  • 第一个 f 表示要代入一个函数，当函数传入后，公式就会变为函数的嵌套形式，递归完成。

计算例子

lambda 演算中，TRUE 运算符定义为 λx.λy.x

举个例子： ((TRUE a) b) 的计算。

即为 ((λx.λy.x a) b)，然后开始规约：

1. 应用第一个参数 a，得到 (λy.a b)
2. 应用第二个参数 b，因为返回值 a 与 b 无关，所以最终返回为 a

因此，TRUE 的行为是：总返回第一个参数，忽略第二个参数。