λ演算
维基百科,自由的 encyclopedia
λ演算(英语:lambda calculus,λ-calculus)是一套从数学逻辑中发展,以变数绑定和替换的规则,来研究函式如何抽象化定义、函式如何被应用以及递回的形式系统。它由数学家阿隆佐·邱奇在20世纪30年代首次发表。lambda演算作为一种广泛用途的计算模型,可以清晰地定义什么是一个可计算函式,而任何可计算函式都能以这种形式表达和求值,它能模拟单一磁带图灵机的计算过程;尽管如此,lambda演算强调的是变换规则的运用,而非实现它们的具体机器。
此条目包含过多行话或专业术语,可能需要简化或提出进一步解释。 |
lambda演算可比拟是最根本的编程语言,它包括了一条变换规则(变数替换)和一条将函式抽象化定义的方式。因此普遍公认是一种更接近软体而非硬体的方式。对函数式编程语言造成很大影响,比如Lisp、ML语言和Haskell语言。在1936年邱奇利用λ演算给出了对于判定性问题(Entscheidungsproblem)的否定:关于两个lambda运算式是否等价的命题,无法由一个“通用的演算法”判断,这是不可判定效能够证明的头一个问题,甚至还在停机问题之先。
lambda演算包括了建构lambda项,和对lambda项执行归约的操作。在最简单的lambda演算中,只使用以下的规则来建构lambda项:
More information 语法, 名称 ...
语法 | 名称 | 描述 |
---|---|---|
x | 变量 | 用字元或字串来表示参数或者数学上的值或者表示逻辑上的值 |
(λx.M) | 抽象化 | 一个完整的函数定义(M是一个 lambda 项),在表达式中的 x 都会绑定为变量 x。 |
(M N) | 应用 | 将函数M作用于参数N。 M 和 N 是 lambda 项。 |
Close
产生了诸如:(λx.λy.(λz.(λx.zx)(λy.zy))(x y))的表达式。如果表达式是明确而没有歧义的,则括号可以省略。对于某些应用,其中可能包括了逻辑和数学的常量以及相关操作。
本文讨论的是邱奇的“无类型lambda演算”,此后,已经研究出来了一些有类型lambda演算。