λ演算
概述
λ演算是由丘奇在1930年代发明的一种函数抽象与应用的形式系统，与图灵机等价，是函数式编程语言的理论基础。
关键内容
- 基本概念：
- 一种用于表达计算的数学逻辑系统
- 通过函数抽象和函数应用来进行计算
-
基本元素包括变量、函数抽象（λx.M）和函数应用((MN))
-
语法结构：
- 变量：x, y, z...
- 抽象：λx.M（定义以x为参数的函数M）
-
应用：(MN)（将函数M应用于参数N）
-
计算规则：
- β归约：(λx.M)N →β M[x:=N]（函数应用的计算）
- α变换：变量改名以避免冲突
-
η变换：函数的外延性
-
与图灵机的关系：
- 图灵证明了λ演算与图灵机在可计算性上等价
- 一个函数是λ可定义的当且仅当它是图灵可计算的
-
这一等价性为Church-Turing论题提供了经验支持
-
历史意义：
- 丘奇在1936年率先使用λ演算解决了判定问题
- 为函数式编程语言（如Lisp、Haskell）提供了理论基础
-
相比图灵机，λ演算更抽象，但直观性较差
-
现代应用：
- 函数式编程语言的理论基础
- 类型理论和程序语言设计
- 计算机辅助证明系统
来源
- 01-turing-on-computable-numbers — 图灵对λ演算的讨论
- 论可计算数及其在判定问题上的应用 — 等价性证明
相关
- 丘奇 — 发明者
- 图灵机 — 等价计算模型
- Church-Turing论题 — 等价性支持
- 函数式编程 — 实际应用
- 阿兰·麦席森·图灵 — 证明等价性